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