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