Adding Unsafe Constraints to Improve SAT Solver Performance

John Franco

Abstract:

We examine the structure of CNF representations of common problems,

such as bounded model checking, in Formal Verification. We observe that

this structure arises in a variety of other difficult problems as well. We

show why such structures are difficult for current Satisfiability solvers:

namely, that inferences typically can be discovered only after a large

number of variables have been set. Thus, for example, clause learning

is not as effective on such structures as we would like it to be. We

propose some ideas which may lead to significantly reduced solution times for

these and other problems. These have have to do with guessing

inferences apriori BASED ON SOLUTION STRUCTURE and not formula structure

as is typically done in preprocessing. That is, the structure of solutions

that can be found for smaller versions of a problem are examined for

necessary patterns of variable values - either to support or reject the solutions -

and constraints are added to the original formula to enforce inclusion

or rejection of these patterns. Adding guessed constraints can reduce

search enormously but may eliminate some solution traces, so at some search

depth these guessed constraints are removed and search continues to the end.

The trick is to prevent all solutions from being lost if at least one

exists. For Formal Verification problems this means, at worst, getting

a result with a certain confidence. Some other problems can be solved

more directly. For example, this idea was used to find a van der Waerden

number W(2,6) = 1132 by first getting a bound then using solution patterns to

reduce a full search to something manageable. We are still refining

this technique.