# MonoSAT

MonoSAT is a SAT Modulo Theory (SMT) solver for monotonic theories over Booleans and bitvectors. It supports reasoning about a wide set of graph properties, including reachability, shortest paths, acyclicity, minimum-weight spanning trees, and maximum s-t flows. It also has some support for geometric predicates, in particular, for detecting intersections of convex-hulls of point sets, and experimental support for reasoning about finite state machines.

The graph properties that MonoSAT supports can be used to generate graphs that have complex properties - for example, to create a graph which is guaranteed to have a path from node A to node B, but not to have a path from node A to node C, unless the maximum flow from node B to node D is within a certain range. These requirements can be combined with arbitrary Boolean logic constraints (in CNF format), allowing graphs with complex characteristics to be created (or just reasoned about) using MonoSAT.

A description of the techniques behind our SAT Modulo Monotonic Theory solver can be in our AAAI 2015 paper. Additional technical details can be found in the 2014 pre-print of the paper, as well as in this thesis.

• MonoSAT [binary | src]
The stable release of MonoSAT, statically compiled for Linux x64 (tested on Ubuntu 14.04).
Read more about MonoSAT, find tutorials, examples, and access the most recent release, at GitHub.
• linedd, a line-oriented delta-debugger [src]
linedd is a portable, format-agnostic, line-oriented Delta Debugger written in Python, which was used extensively for debugging and developing MonoSAT and its associated file format.

### Previous releases of MonoSAT:

• MonoSAT 1.1.2 [binary | source]
Adds bitvector support, and a Python 3 library interface, as well as major performance improvements.
• MonoSAT 1.0.1 [binary | source]
This is the first stable release of MonoSAT.
• AAAI 2015 [binary | source]
This is the version of MonoSAT used for the AAAI 2015 paper’s experiments. Watchout: it has some performance issues, and even a few known bugs!

### Licensing

MonoSAT as a whole is released under the GPL, version 3 or later.
Most of MonoSAT (see the source for details) is also available under the MIT license.