There are several powerful solvers for satisfiability (SAT), such as WSAT, Davis-Putnam, and RELSAT. However, in practice, the SAT encodings often have so many clauses that we exceed physical memory resources on attempting to solve them. This excessive size often arises because conversion to SAT, from a more natural encoding using quantifications over domains, requires expanding quantifiers.
This suggests that we should "lift" successful SAT solvers. That is, adapt the solvers to use quantified clauses instead of ground clauses. However, it was generally believed that such lifted solvers would be impractical: Partially, because of the overhead of handling the predicates and quantifiers, and partially because lifting would not allow essential indexing and caching schemes.
Here we show that, to the contrary, it is not only practical to handle quantified clauses directly, but that lifting can give exponential savings. We do this by identifying certain tasks that are central to the implementation of a SAT solver.These tasks involve the extraction of information from the set of clauses (such as finding the set of unsatisfied clauses in the case of WSAT) and consume most of the running time. We demonstrate that these tasks are NP-hard with respect to their relevant size measure. Hence, they are themselves search problems, and so we call them "subsearch problems".
Ground SAT solvers effectively solve these subsearch problems by naive enumeration of the search space. In contrast, a lifted solver can solve them using intelligent search methods. Consequently, lifting a solver will generally allow an exponential reduction in the cost of subsearch and so increase the speed of the search engine itself.
Experimental results are given for a lifted version of WSAT. We only use very simple backtracking for the subsearch, but we still find that cost savings in the su bsearch can more than offset the overheads from lifting. The reduction in size of the formulas also allows us to solve problems that are too large for ground WSAT.
In summary, a lifted SAT solver not only uses far less memory than a ground solver, but it can also run faster.