MonoSAT is a SAT Modulo Theory solver for monotonic theories, over Booleans and bitvectors. It supports a wide set of graph predicates (including reachability, shortest paths, maximum s-t flow, minimum spanning tree, and acyclicity constraints). MonoSAT also has limited support for geometric constraints involving convex hulls of point sets, and experimental support for constraints on finite state machines.

MonoSAT now comes with a simplified, Z3-inspired Python 3 interface (see api/python). See installation instructions below; see also the tutorial.

To see further examples of use cases for MonoSAT, and details on the (very simple) input file format that MonoSAT accepts, see FORMAT.

###Building From the root directory, build MonoSAT with:

$cd Release
$make

or

$cd Static
$make

or (to build the shared library, required by the Python interface):

$cd SharedLibrary
$make

MonoSAT requires C++11 support, zlib, and GMP >= 5.1.3. Tested on Ubuntu 14.04, with G++ 4.8.2 and G++ 4.9. The python library requires Python 3.3+.

If you get errors along the lines of "error: could not convert ‘x’ from ‘__gmp_expr<__mpq_struct [1], __mpq_struct [1]>’ to ‘bool’", then you likely need to install a more recent version of GMP.

If you build MonoSAT without using the provided makefiles, it is critically important to compile with NDEBUG set (i.e., -DNDEBUG), as otherwise many very expensive debugging assertions will be enabled.

###Install the Python Library

To install the Python library (system-wide), first install the shared library, and then use Python's setuptools to install the Python library. The Python library has optional support for pseudo-Boolean constraints, using MinisatPB, which is a fork of Minisat+.
In order to use pseudo-Boolean constraints in the Python library, you must separately install MinisatPB on your system path.

On Ubuntu (14.04):

$cd SharedLibrary
$make
$sudo cp libmonosat.so /usr/local/lib/
$cd ../api/python
$sudo python3 setup.py install

###Usage MonoSAT is based on MiniSat 2, and supports many of the same calling conventions:

$monosat [-witness|-witness-file=filename] input_file.gnf

Where input_file.gnf is a file in GNF format (a very simple extension of DIMACS CNF format to support graph and geometry predicates). Use -witness to print the solution (if one exists) to stdout, or -witness-file to save it to file.

MonoSAT includes a very large set of configuration options - most of which you should stay away from unless you know what you are doing or want to explore the internals of MonoSAT (also, some of those configuration options might lead to buggy behaviour). Two options that often have a large impact on performance are -decide-theories and -conflict-min-cut:

$monosat -decide-theories -conflict-min-cut input_file.gnf

The -decide-theories option will cause the solver to make heuristic decisions that try to satisfy the various SMT predicates, which will often lead to improved performance, but can be pathologically bad in some common cases, and so is disabled by default. -conflict-min-cut will cause the solver to use a much slower, but more aggressive, clause learning strategy for reachability predicates; it may be useful for small, dificult instances.

###Source Overview MonoSAT is written in C++. Core SAT solver functionality is in the core/ and simp/ directories; in particular, note core/Config.cpp, which is a central listing of all the configuration options available to MonoSAT.

The graph and geometry theory solvers can be found in geometry/ and graph/. Many of the graph algorithsms used by MonoSAT are collected in dgl/ (for 'Dynamic Graph Library').

dgl/ incldudes C++ implementations of several dynamic graph algorithms (as well as some more common graph algorithms), and is well-optimized for medium sized (<20,000 nodes, < 100,000 edges), sparse graphs. The algorithms in dgl are designed for the case where the set of possible edges (and nodes) is fixed and known in advance (or only changes infrequently), and from that fixed set of possible edges many subsets of edges will subsequently be selected to be included in or excluded from the graph. 'dgl' supports templated edge weights and edge capacities, and has been tested successfully with integers, floats, and GMP arbitrary precision rationals.

######Algirthms implemented in 'dgl/' include:

• Reachability/Shortest Path
  • Ramalingam-Reps dynamic single-source shortest paths algorithm (with improvements described in Buriol et al. 2008)
  • Thorup's dynamic connectivity algorithm (for undirected graphs)
  • Dijkstra's algorithm
  • DFS/BFS
• Minimum Spanning Tree
  • Spira and Pan's dynamic minimum spanning tree algorithm
  • Kruskal's algorithm
  • Prim's algorithm
• Maximum s-t Flow
  • Kohli and Torr's dynamic maximum flow algorithm
  • Edmonds-Karp algorithm (including a dynamic variant)
  • Dinitz's algorithm (including the dynamic tree variant)
• And many supporting algorithms and data structures, including:
  • Euler Tree
  • Link Cut Tree
  • Splay Tree
  • Disjoint Set

###Licensing The majority of MonoSAT is released under the MIT license (as documented in individual source files). However, some of the code, including some important libraries, fall under the GPL, and as a result, MonoSAT as a whole is currently released under the GPL (version 3 or later).

###Acknowledgements

MonoSAT was made possible by the use of several open-source projects, including the afore-mentioned MiniSat, as well as a high-performance dynamic maximum-flow algorithm by Pushmeet Kohli and Philip Torr, Emil Stefanov's implementation of Disjoint Sets, a Link-Cut Tree implementation by Daniel Sleator, and a computational geometry library by Chelton Evans.

###References

Edmonds, Jack, and Richard M. Karp. "Theoretical improvements in algorithmic efficiency for network flow problems." Journal of the ACM (JACM) 19.2 (1972): 248-264

Ramalingam, Ganesan, and Thomas Reps. "An incremental algorithm for a generalization of the shortest-path problem." Journal of Algorithms 21.2 (1996): 267-305.