Home
 Papers
 Software
 Licensing
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 realworld 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 SMSPDR implementation of IC3, which runs singlethreaded, and without any
preprocessing. In the paper we combine it with DAGaware rewriting (provided by ABC).
Licensing
ModSAT and SMSPDR are both released under the MIT licence.
Please send any questions,
concerns or comments to Sam
Bayless