Effective Preprocessing in SAT through Variable and Clause Elimination

Niklas Eén

Cadence Berkeley Laboratories

Berkeley, USA

Armin Biere

Johannes Kepler University
Linz, Austria

for SAT 2005

The Eighth International Conference on

Theory and Applications of Satisfiability Testing

June 20, 2005

Problem Statement: Clausification of Netlists

Typically represented using And-Inverter graphs.

We can write a good clausifier... [JS04,Vel05]

Can we “recover” after we translated to clauses?

Yes, do preprocessing in the SAT solver!

Global view Þ Better results

More general

Saves the user of the SAT solver the trouble of writing a good clausifier (to some extent).

Purpose of Preprocessing

Slim down the CNF to a core without “obvious” redundancies, such as:

“Meaningless” internal variables.

Big conjunctions: a & (b & (c & d))

MUXes: (s & x) | (~s & y)

Equivalent literals.

Binary clauses: (x → y), (y → x)

Unpropagated shallow facts (generalize BCP).
Example. Hyper-unary-resolution:

Clauses: (a | b | c), (a → x), (b → x), (c → x)

The Preprocessor SATELITE

We implement three basic techniques:

Variable elimination by resolution.
Takes care of wasteful internal variables
(and equivalent literals*).

Fast subsumption. C Í C' (backward: Cnew Í Cold)
Removes “trash” produced by the variable
elimination (important!).

Self-subsumption. (x | A) Äx (~x | A | B) = (A | B)
Gives a generalization of BCP (Niklas Sörensson)

{˜x, a}	{x, ˜a, ˜b}

{˜x, b} Ä	{x, d, ˜c, e}

{˜x, c}	{x, a, ˜c, e}

{a, ˜a, ˜b}	{b, a, ˜c, e}

{a, d, ˜c, e}	{c, ˜a, ˜b}

{a, ˜c, e}	{c, d, ˜c, e}

{b, ˜a, ˜b}	{c, a, ˜c, e}

{b, d, ˜c, e}

Outline of Algorithm

Repeat until no more changes:

selfSubsume()

subsume()

eliminateVars()

Backward subsumption and BCP applied eagerly.

Made efficient by tracking clauses that are...

strengthened by selfSubsume() or BCP.

removed by subsumption or BCP.

added or removed by eliminateVars().

A clause may become unit

Þ	top-level unit propagation.

Eliminate “x” if leads

to fewer clauses.

Details on Variable Elimination

Try variable x where #occur(x) ´ #occur(~x) is smallest first.

If both #occur(x) and #occur(~x) are >10, skip.

For pragmatic reasons, detect definitions:

Clauses: (t ® x), (t ® y), (x & y ® t)
mean “t « x & y” Þ eliminate t by inlining.

Natural to do hyper-unary-resolution during this step.

Details on Subsumption

Maintain occurs-lists. [Biere04]

occur(p) is the set of clauses where p occurs.

For each clause, store a 64-bit signature.

Hash each literal to a number 0..63. Take bitwise OR.

subset(Clause C, Clause C')

if (size(C) > size(C'))	return FALSE

if (sig(C) & ~sig(C'))	return FALSE

return result of complete (expensive) subset test

findSubsumed(Clause C)

pick the literal p in C with the shortest occur list

for each C' Î occur(p) do

if (C ¹ C' && subset(C, C' ))

add C' to result

return result

Demo!

module main()

{

num : array 4..0 of boolean;

init	(num) := 6;

next	(num) := (~num[0]) ? (num >> 1) : (num * 3 + 1);

test : assert G (num ~= 1);

}

SMV file

Small BMC problem unrolled 4 time-frames.

Resulting boolean circuit clausified by introducing one variable per binary AND/XOR.

Missing variables in model?

We need to extend the satisfying assignment. This is cheap!

In an incremental SAT solver, we need to “freeze” variables.

Experimental Results

MINISAT solved 376 industrial problems in 1st-stage.
SATELITE + MINISAT solved 402 problems.

We investigate:

size reduction

runtime effect

Size Reductions

Size Reductions

Preprocessing Time

Preprocessing Time (log-scale)

Heads-up Comparison

MiniSat

ZChaff

Heads-up Comparison

Conclusions

Many SAT problems inefficiently encoded.

Big performance gain can be achieved by improving the encoding.

A solution at the SAT level can be efficient and effective.

The presented method is completely resolution based, which facilitates proof-logging.

Other rewrite rules and implementation tricks are of course possible. We show by construction that the general direction is worth looking at.

Future Work

Look-ahead strategy

Scheduling

of application of self-subsumption

of variable elimination

Evaluating the differences and benefits of SAT preprocessing vs. a good clausifier.

Bibliography

[JS04] “Clause Form Conversions for Boolean Circuits”
Paul Jackson and Daniel Sheridan (SAT 2004)

[Vel05] “Efficient Translation of Boolean Formulas to CNF in Formal

Verification of Microprocessors”
Miroslav N. Velev (Tech Report 2005)

[Biere04] “Expand and Resolve”
Armin Biere (SAT 2004)

Niklas Een

2005-05-25T21:13:19