Modular SAT


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




ModSAT and SMSPDR are both released under the MIT licence.

Please send any questions, concerns or comments to Sam Bayless