Modular SAT

ModSAT is "SAT Modulo SAT" solver - that is, like a SAT Modulo Theory solver, but where the `theory' is itself Boolean satisfiability.

There are several reasons why we might want to solve a SAT instance modulo another SAT instance (or, recursively, modulo SAT modulo SAT modulo SAT...). The first is that if we are trying to solve an instance with known, `modular' structure (.i.e., the instance is composed of several CNFs, each of which share relatively few variables with each other), then the theories in this SAT modulo SAT solver are a way of capturing and exploiting that structure (by improving memory locality). One very common example of such `modular' instances is anything produced by unrolling a transition function, such as during bounded model checking. However, since in general most things that human design have some degree of modularity built in, many types of SAT instances produced by translating real-world problems into CNF will also have such structure - for example, software verification instances (even before unrolling loops) will generally produce a CNF with modular structure.

Papers

• Efficient Modular SAT Solving for IC3
  Sam Bayless, Celina G. Val, Thomas Ball, Holger H. Hoos, Alan J. Hu - FMCAD 2013
  This paper both introduces the SAT Modulo SAT solver, and describes its application to the model checker IC3.
  [pdf | bibtex ]

Software

• ModSAT [binary | source]
  This is the current release of the SAT Modulo SAT solver, based on Minisat 2.2. This initial release is a cleaned up, simplified version of the one that I am currently experimenting with; it is packaged with a very simple incremental bounded model checker. This bounded model checker may not be particularly fast - it is just intended to provide an easy source of modular SAT instances with which to test out ModSAT. Also note that this still a beta release; although I have tested it, it most likely has bugs, and it isn't yet as heavily optimized as it could be.
• SMSPDR [binary (version from FMCAD 2013) | source ]
  This is our implementation of IC3 using our SAT Modulo SAT solver. It can solve just one fewer of the 2008 Hardware Model Checking Competition instances than the entire Virtual Best Solver from the 2008 competition - that is, just one fewer than the total set of instances solved by ''any'' the entrants in the original competition. Note that the binary includes only our SMS-PDR implementation of IC3, which runs single-threaded, and without any pre-processing. In the paper we combine it with DAG-aware rewriting (provided by ABC).

Licensing

Please send any questions, concerns or comments to Sam Bayless