MERGESAT SAT SOLVER

The goal of the development of MergeSat is to re-use and merge proposed SAT solving techniques, and merge them into a single solver, so that they do not get lost. Furthermore, MergeSat should be kept backwards compatible to MiniSat, so that tools using MiniSat or Glucose as SAT backend today could easily switch to MergeSat.

MergeSat also implements interfaces and features to integrate it into other workflow, for example the incremental SAT interface IPASIR. Furthermore, MergeSat can print its parameter specification so that automated parameter tuning can be used to find a better setup for a given benchmark family. Finally, MergeSat can check whether the obtained model actually satisfied the input formula, and can emit unsatisfiability proofs -- as well as check them during run time -- to make sure unsatisfiability results are correct. See the CHANGELOG file for more recent additions and extensions.

QUICK START

To solve a CNF formula input.cnf with MergeSat, you need to first build the solver, and next can solve the formula:

make r
build/release/bin/mergesat input.cnf

DIRECTORY OVERVIEW:

minisat/mtl/            Mini Template Library
minisat/utils/          Generic helper code (I/O, Parsing, CPU-time, etc)
minisat/core/           A core version of the solver
minisat/parallel/       An extended solver with parallel solving, and helpers
minisat/simp/           An extended solver with simplification capabilities
minisat/tests/          Unit tests for the solver and data structures

BUILDING: (release version: without assertions, statically linked, etc)

To build the release variant of the solver, use the below command. Other variants of the tool can be build by using the build target make all.

make r
cp build/release/bin/mergesat <install-dir>/mergesat

Note: MergeSat can also be used via docker. The resulting docker image contains a binary of MergeSat that can be used to solve formulas (see examples below).

The docker file Dockerfile brings build dependencies for MergeSat, and will install the solver in the image, so that CNFs can be solved.

docker build .

To be able to consume the Fedora base image, you might need to pull the Fedora images first, by running:

docker pull fedora

As the release build of MergeSat is a statically linked binary, you can also use the create container to compile the solver in the cloned repository. The major advantage is that by compiling with a recent glibc, transparent huge pages can be used with the statically linked binary.

Note, the binary created with the docker file tries to back allocated memory with transparent huge pages. This typically results in a 10% speedup (average), but also can result in less reproducability of runtime, as transparent huge pages might not be available.

docker run -u=$(id -u) -v $PWD:$PWD -w $PWD $CONTAINER make r -B

Full list of commands to build the solver with the docker file:

CONTAINER=$(docker build -q .)
docker run -u=$(id -u) -v $PWD:$PWD -w $PWD $CONTAINER make r -B
cp build/release/bin/mergesat <install-dir>/mergesat

EXAMPLES:

Solve some CNF file:

./mergesat "input.cnf"

Solve some CNF file and produce an unsatisfiability proof:

./mergesat "input.cnf" -drup-file="$TMPDIR"/proof.out

Display all options of the solver:

./mergesat --help

Generate a parameter model file for parameter tuning (with ParamILS or SMAC):

./mergesat -pcs-file=mergesat.pcs

Solve a CNF in a dockerfile:

docker run -v $PWD:$PWD $CONTAINER_ID \
  /opt/mergesat/uild/release/bin/mergesat $INPUT

PARALLEL SOLVING

This feature is currently considered experimental. Long-term, the sequential solver should be replaced by the parallel solver.

MergeSat implements a deterministic parallel solving approach. This solver allows to produce unsatisfiability proofs as well, and provides the incremental MiniSat interface. When compiling MergeSat as parallel solver, the solver behind the interface will use the parallel implementation.

The number of used cores is set to 1 by default -- making the solver behave like the sequential solver.

Building

When you built the sequential solver before the parallel solver, you need to clean the built files. Otherwise, some definitions will be missing when you try to compile the parallel solver.

make clean
make BUILD_TYPE=parallel r

All other build targets from the sequential build work in the parallel build as well.

Examples

Solve some CNF file with 4 cores:

./mergesat "input.cnf" -cores=4

Solve some CNF file and produce an unsatisfiability proof with 4 cores:

./mergesat "input.cnf"  -cores=4 -drup-file="$TMPDIR"/proof.out

Display all options of the solver:

./mergesat --help

RELATED RESEARCH

When using the solver, please cite the below publication. This paper describes the goal of the solver, as well as a few learnings that have been made while developing the solver.

@inproceedings{DBLP:conf/sat/Manthey21,
  author    = {Norbert Manthey},
  editor    = {Chu{-}Min Li and
               Felip Many{\`{a}}},
  title     = {The MergeSat Solver},
  booktitle = {Theory and Applications of Satisfiability Testing - {SAT} 2021 - 24th
               International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {12831},
  pages     = {387--398},
  publisher = {Springer},
  year      = {2021},
  url       = {https://doi.org/10.1007/978-3-030-80223-3\_27}
}