search

sambayless / monosat

MonoSAT - An SMT solver for Monotonic Theories
MIT License
107 stars 30 forks source link
graph sat smt

readme

MonoSAT

Build Status

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 supports reasoning about graphs that are either directed or undirected (including graphs that may have cycles). Edges may (optionally) have constant or Bitvector weights. MonoSAT also has experimental support for constraints on finite state machines - see FiniteStateMachines for details.

MonoSAT can be used from the command line, or as a Python 3 library. See the 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 and 16.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, with C++ support enabled.

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.

Building on OSX with brew

You will need to first install GMP:

$brew install gmp

MonoSAT will, by default, compile statically linked binaries and dynamically linked libraries. In most cases, you can then continue the cmake installation as above.

However, in some cases brew might not add the GMP libraries to the library path, in which case MonoSAT compilation may fail during linking. You can check where brew installed GMP with:

$brew --prefix gmp

If brew installed GMP to /opt/local/lib/gmp, then you may need to modify the MonoSAT compilation instructions as follows:

$cmake .
$DYLD_LIBRARY_PATH=/opt/local/lib LIBRARY_PATH=/opt/local/lib make
$sudo make install

Building on FreeBSD (Only tested on FreeBSD 12)

You will need to first install GMP, which you can do via pkg or ports:

$pkg install gmp

If you intend to include the Java library (see below), you'll also need a JDK and you'll need to set your JAVA_HOME environment variable:

$pkg install openjdk8
$export JAVA_HOME=/usr/local/openjdk8

Installing the Python library

To install the Python library (system-wide) on your system's default Python version:

$cmake -DPYTHON=ON .
$make
$sudo make install

MonoSAT also has support for Cython bindings, which are about 30% faster but require you to have a wokring installation of cython:

$cmake -DPYTHON=ON -DCYTHON=ON .
$make
$sudo make install

To install MonoSAT in an alternative python version (or in a virtual env or a non-standard location), first build MonoSAT as normal, then cd into 'src/monosat/api/python', and then use setup.py to install the Python library manually, eg:

$cd src/monosat/api/python
$sudo python3.6 setup.py install -f

Above, -f ensures that if you have previously installed a version of the monosat library, it will be overwritten cleanly with the new version.

See the tutorial and tutorial.py for instructions on using the Python library.

Compiling the Java Library

To compile the Java library, you need to build MonoSAT with Java bindings enabled. You will also need an installed JDK, version 1.8 or higher:

$cmake -DJAVA=ON .
$make

This should generate monosat.jar in MonoSAT's root directory. To use MonoSAT from Java, you will need to include the jar in your classpath. You will also need to ensure that Java can find MonoSAT's dynamic library, for example:

java -Djava.library.path=path/to/libmonosat.so -cp path/to/monosat.jar mypacakge.MyMainClass

On OSX, you would instead use path/to/libmonosat.dylib

See Tutorial.java for instructions on using the Java library.

Command-Line Usage

The recommended way to use MonoSAT is as a library, via the Python or Java bindings. However, it is also possible to call MonoSAT from the command line. 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, bitvector, and finite state machine 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.

MonoSAT implements a generalization of the circuit routing heuristics described in Routing Under Constraints; you can activate them using the '-ruc' command line option. Thse can greatly improve performance on instances that use multiple reachability constraints. See examples/python/routing/router.py for an example usage.

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/. 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:

Licensing

The majority of MonoSAT is released under the MIT license (as documented in individual source files). However, by default MonoSAT links some GPLv2 sources (found in src/monosat/dgl/alg/dyncut/). If built with these sources, the resulting binary is licensed as a whole under the GPLv2.

MonoSAT can be built without including any GPL licensed sources, in which case it retains the MIT license. To build MonoSAT without using GPL sources, use: ''' $cmake -DGPL=OFF '''

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, and a Link-Cut Tree implementation by Daniel Sleator.

Publications using MonoSAT

If you would like your publication listed here, please contact Sam Bayless.

If you want to cite MonoSAT, please cite our 2015 AAAI paper:

@article{monosat2015,
  author    = {Sam Bayless and Noah Bayless and Holger H. Hoos and Alan J. Hu},
  title     = {{SAT Modulo Monotonic Theories}},
  booktitle = {Proceedings of the 29th AAAI Conference on Artificial Intelligence},
  year      = {2015}
}

Further References