# MonoSAT

#### Home | Downloads | GitHub | Licensing

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.

• 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
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 1, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.17845375835895538, "perplexity": 3673.0460221890216}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.3, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2017-39/segments/1505818689775.56/warc/CC-MAIN-20170923175524-20170923195524-00038.warc.gz"}