bratelefant / mallob

Malleable Load Balancer. Multitasking Agile Logic Blackbox. Award-winning SAT solving for the cloud.

Mallob

Short links: Experimental data of our SAT21 paper · Animallob: Interactive visualization of experiments

---

Overview

Mallob is a platform for massively parallel and distributed on-demand processing of malleable jobs, handling their scheduling and load balancing. Malleability means that the CPU resources allotted to a job may vary during its execution depending on the system's overall load.

Most notably, Mallob features an engine for distributed SAT solving. According to the International SAT Competition 2020🥇 and 2021🥇🥈, Mallob is currently the best approach for SAT solving on a large scale (800 physical cores) and one of the best approaches for SAT solving on a moderate scale (32 physical cores).

More information on the design decisions and techniques of Mallob can be found in our SAT 2021 paper where we also evaluated Mallob on up to 2560 physical cores.

---

Installation

There are two options on how to obtain a functional instance of Mallob: (a) by direct installation on your Linux system, or (b) via Docker.

Build on Linux

Mallob is built with CMake. Note that a valid MPI installation is required (e.g. OpenMPI, Intel MPI, MPICH, ...). In addition, before building Mallob you must first execute cd lib && bash fetch_and_build_sat_solvers.sh which, as the name tells, fetches and builds all supported SAT solving libraries.

To build Mallob, execute the following usual steps:

mkdir -p build
cd build
cmake .. <cmake-options>
make

If you want to make use of Glucose as a SAT solver, use the cmake option -DMALLOB_USE_RESTRICTED=1 (after having read the Licensing section below). Use -DMALLOB_USE_ASAN=1 to build Mallob with Address Sanitizer for debugging purposes.

Docker

Alternatively, you can run Mallob in a Docker container. Run docker build . in the base directory after setting up Docker on your machine. The final line of the output is the ID to run the container, e.g. by running docker run -i -t <id> bash and then executing Mallob interactively inside with the options of your choosing.

---

Usage

Mallob can be used in several modes of operation which are explained in the following.

Launching Mallob

For any multinode computations, Mallob is launched with mpirun, mpiexec or some other MPI application launcher. In addition, Mallob supports spawning SAT solver engines in two ways: As a number of separate threads within the MPI process, or as its individual child process. This can be set with -appmode=thread or -appmode=fork respectively. Forked mode is the default mode and requires that (i) the executable mallob_sat_process (produced during the build) is located in a directory contained in the PATH environment variable and (ii) the environment variable RDMAV_FORK_SAFE=1 must be set.

To sum up, a command to launch Mallob is usually structured like this:

RDMAV_FORK_SAFE=1 PATH=.:$PATH mpirun <mpi-options> ./mallob <options>

Solving a single SAT instance

Call Mallob with the option -mono=<cnf-file>. Mallob will run in single instance solving mode on the provided CNF file: All available MPI processes (if any) are used with full power to resolve the formula in parallel. This option overrides a couple of options concerning balancing and job demands.

For instance, the Mallob-mono configuration for the SC 2020 Cloud Track roughly corresponds to the following parameter combination:

-mono=<input_cnf> -log=<logdir> -T=<timelim_secs> -appmode=thread -cbdf=0.75 -cfhl=300 -mcl=5 -sleep=1000 -t=4 -v=3 -satsolver=l

This runs four solver threads for each MPI process and writes all output to stdout as well as to the specified log directory, with moderate verbosity.

Scheduling and solving many instances

Launch Mallob without any particular options regarding its mode of operation. Mallob then opens up a JSON API which can be used over the file system of any of the client nodes under <base directory>/.api/.

Users

The API distinguishes jobs by the user which introduced them. By default there is a user admin defined in .api/users/admin.json. You can just use this user or create a new one and save it under .api/users/<user-id>.json. The priority must be larger than zero and no larger than one; a higher number gives more importance to the user's jobs.

Job Directories

If multiple clients are used, then the i-th client uses .api/jobs.<i>/ as its API directory. Therefore, if only a single client is employed (which is the default), the directory .api/jobs.0/ is used.

Introducing a Job

To introduce a job to the system, drop a JSON file in .api/jobs.0/new/ structured like this:

{ 
    "user": "admin", 
    "name": "test-job-1", 
    "file": "/path/to/difficult/formula.cnf", 
    "priority": 0.7, 
    "wallclock-limit": "5m", 
    "cpu-limit": "10h",
    "arrival": 10.3,
    "dependencies": ["admin.prereq-job1", "admin.prereq-job2"],
    "incremental": false
}

Here is a brief overview of all required and optional fields in the JSON API:

Field name	Required?	Value type	Description
user	yes	String	A user which is present at .api/users/<user>.json
name	yes	String	A user-unique name for this job (increment)
file	yes*	String	File path of the input formula to solve
priority	yes*	Float (0,1)	Priority of the job (higher is more important)
application	no	String	Which kind of problem is being solved; currently either of "SAT" or "DUMMY" (default: SAT)
wallclock-limit	no	String	Job wallclock limit: combination of a number and a unit (ms/s/m/h/d)
cpu-limit	no	String	Job CPU time limit: combination of a number and a unit (ms/s/m/h/d)
arrival	no	Float >= 0	Job's arrival time (seconds) since program start; ignore job until then
max-demand	no	Int >= 0	Override the max. number of MPI processes this job should receive at any point in time
dependencies	no	String array	User-qualified job names (using "." as a separator) which must exit before this job is introduced
incremental	no	Bool	Whether this job has multiple increments / revisions and should be treated as such
precursor	no	String	(Only for incremental jobs) User-qualified job name (<user>.<jobname>) of this job's previous increment
incremental	no	Bool	(Only for incremental jobs) If true, the incremental job given by "precursor" is finalized and cleaned up.

*) Not needed if done is set to true.

In the above example, a job is introduced with effective priority <user-prio> * <job-prio> = 1.0 * 0.7 = 0.7, with a wallclock limit of five minutes and a CPU limit of 10 CPUh. The formula file must be a valid CNF file. For incremental jobs, Mallob uses the common iCNF extension: The file may contain a single line of the form:

a <lit1> <lit2> ... 0

where <lit1>, <lit2> etc. are assumption literals.

The "arrival" and "dependencies" fields are useful to test a particular preset scenario of jobs: The "arrival" field ensures that the job will be scheduled only after Mallob ran for the specified amount of seconds. The "dependencies" field ensures that the job is scheduled only if all specified other jobs are already processed.

Mallob is notified by the kernel as soon as the file is placed in .api/jobs.0/new/ and will immediately move the job description to .api/jobs/pending/ and schedule the job.

Retrieving a Job Result

Upon completion of a job, Mallob writes a result JSON file under .api/jobs.0/done/<user-name>.<job-name>.json (you can repeatedly query the directory contents or employ a kernel-level mechanism like inotify). Such a file may look like this:

{
    "cpu-limit": "10h",
    "file": "/path/to/difficult/formula.cnf",
    "name": "test-job-1",
    "priority": 0.7,
    "result": {
        "responsetime": 0.02732086181640625,
        "resultcode": 20,
        "resultstring": "UNSAT",
        "revision": 0,
        "solution": []
    },
    "user": "admin",
    "wallclock-limit": "5m"
}

The result code is 0 is unknown, 10 if SAT, and 20 if UNSAT. In case of SAT, the solution field contains the found satisfying assignment; in case of UNSAT, the result for an incremental job contains the set of failed assumptions.

Options Overview

All command-line options of Mallob can be seen by executing Mallob with the -h option. This also works without the mpirun prefix.

---

Programming Interfaces

Mallob can be extended in the following ways:

• New options to the application (or a subsystem thereof) can be added in src/optionslist.hpp.
• To add a new SAT solver to be used in a SAT solver engine, do the following:
  • Add a subclass of PortfolioSolverInterface. (You can use the existing implementation for any of the existing solvers and adapt it to your solver.)
  • Add your solver to the portfolio initialization in src/app/sat/hordesat/horde.cpp.
• To extend Mallob by adding another kind of job solving engine (like combinatorial search, planning, SMT, ...), do the following:
  • Extend the enumeration JobDescription::Application by a corresponding item.
  • In JobReader::read, add a parser for your application.
  • In JobFileAdapter::handleNewJob, add a new case for the application field in JSON files.
  • Create a subclass of Job (see src/app/job.hpp) and implement all pure virtual methods.
  • Add an additional case to JobDatabase::createJob.
• To add a unit test, create a class test_*.cpp in src/test and then add the test case to the bottom of CMakeLists.txt.
• To add a system test, consult the files scripts/systest_commons.sh and/or scripts/systest.sh.

---

Licensing

In its default configuration, the source code of Mallob can be used, changed and redistributed under the terms of the Lesser General Public License (LGPLv3), one notable exception being the source file src/app/sat/hordesat/solvers/glucose.cpp (see below). The used versions of Lingeling and YalSAT are MIT-licensed, as is HordeSat.

The Glucose interface of Mallob, unfortunately, is non-free software due to the non-free license of (parallel-ready) Glucose. Notably, its usage in competitive events is restricted. So when compiling Mallob with MALLOB_USE_RESTRICTED=1 make sure that you have read and understood these restrictions.

---

Remarks

Many thanks to Armin Biere et al. for the SAT solvers Lingeling and YalSAT this system uses by default and to Tomáš Balyo for HordeSat, the portfolio solver this project's solver engine is built upon.

Furthermore, in our implementation we make thankful use of the following projects:

• Compile Time Regular Expressions by Hana Dusíková, for matching particular user inputs
• robin_hood hashing by Martin Ankerl, for efficient unordered maps and sets
• JSON for Modern C++ by Niels Lohmann, for reading and writing JSON files

If you make use of Mallob in an academic setting, please cite this SAT'21 conference paper:

@inproceedings{schreiber2021scalable,
  title={Scalable SAT Solving in the Cloud},
  author={Schreiber, Dominik and Sanders, Peter},
  booktitle={International Conference on Theory and Applications of Satisfiability Testing},
  pages={518--534},
  year={2021},
  organization={Springer},
  doi={10.1007/978-3-030-80223-3_35}
}

If you want to specifically cite Mallob in the scope of an International SAT Competition, please cite:

@article{schreiber2020engineering,
  title={Engineering HordeSat Towards Malleability: mallob-mono in the SAT 2020 Cloud Track},
  author={Schreiber, Dominik},
  journal={SAT Competition 2020},
  pages={45}
}
@article{schreiber2021mallob,
  title={Mallob in the SAT Competition 2021},
  author={Schreiber, Dominik},
  journal={SAT Competition 2021},
  note={To appear.}
}