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 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 MonoSAT requires CMake (version 2.7 or higher) From the root directory, build and install MonoSAT with:
$cmake .
$make
$sudo make install
MonoSAT requires C++11 support, zlib, and GMP >= 5.1.3. Tested on Ubuntu 14.04, with G++ 4.8.2 or higher, and with Clang 3.5. The Python library requires Python 3.3+.
If you get compilation 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 cmake/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 build monosat (see above), cd into 'src/monosat/api/python', and then use Python's setuptools to install the Python library (see below).
On Ubuntu (14.04):
$cmake .
$make
$cd src/monosat/api/python
$sudo python3 setup.py install -f
###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, finite state machine, 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 finite state machine theory solvers can be found in graph/ and fsm/, the (not currently maintained) geometry theory is in geom/. 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 variant of Kolmogorov and Boykov's 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:
- Pearce and Kelly's `PK' algorithm for dynamic topological sort in DAGs
- Euler Tree
- Link Cut Tree
- Tarjan's SCC
- 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
- Buriol, Luciana S., Mauricio GC Resende, and Mikkel Thorup. "Speeding up dynamic shortest-path algorithms." INFORMS Journal on Computing 20.2 (2008): 191-204.
- Dijkstra, Edsger W. "A note on two problems in connexion with graphs." Numerische mathematik 1.1 (1959): 269-271
- Dinitz, Y. "Algorithm for solution of a problem of maximum flow in a network with power estimation". Doklady Akademii nauk SSSR 11: 1277–1280 (1970)
- 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
- Kohli, Pushmeet, and Philip HS Torr. "Efficiently solving dynamic markov random fields using graph cuts." Computer Vision, 2005. ICCV 2005. Tenth IEEE International Conference on. Vol. 2. IEEE, 2005
- Korduban, D. "Incremental Maximum Flow in Dynamic graphs." Theoretical Computer Science Stack Exchange. http://cstheory.stackexchange.com/q/10186, 2012
- Kruskal, Joseph B. "On the shortest spanning subtree of a graph and the traveling salesman problem." Proceedings of the American Mathematical society 7.1 (1956): 48-50
- Prim, Robert Clay. "Shortest connection networks and some generalizations." Bell system technical journal 36.6 (1957): 1389-140](http://dx.doi.org/10.1002/j.1538-7305.1957.tb01515.x)
- Ramalingam, Ganesan, and Thomas Reps. "An incremental algorithm for a generalization of the shortest-path problem." Journal of Algorithms 21.2 (1996): 267-305.
- Sleator, Daniel D., and Robert Endre Tarjan. "A data structure for dynamic trees." Proceedings of the thirteenth annual ACM symposium on Theory of computing. ACM, 1981.
- Spira, Philip M., and A. Pan. "On finding and updating spanning trees and shortest paths." SIAM Journal on Computing 4.3 (1975): 375-380.
- Thorup, Mikkel. "Near-optimal fully-dynamic graph connectivity." Proceedings of the thirty-second annual ACM symposium on Theory of computing. ACM, 2000.
- Pearce, David J., and Kelly, Paul H. J. "A Dynamic Topological Sort Algorithm for Directed Acyclic Graphs", 2006