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