# 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.

### Downloads

**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.

Please send any questions, concerns or comments to Sam Bayless