Are there any studies about how effective a limited resolution pre-processor is for DPLL-CDCL type SAT solvers?

By limited resolution pre-processor I mean a pre-processor that generates short (1,2, or 3 variable) resolvent clauses from a SAT instance.

I think such a pre-processor might benefit rapid restart type CDCL solvers.

I can show that connected XSAT instances will always have numerous short resolvent clauses when the XSAT instance is converted to SAT.

This algorithm can be thought of as an inefficient XSAT to SAT conversion.

Two literals are adjacent if they appear together in a clause. A literal is always adjacent to its inverse. If a literal is true in an XSAT instance then all adjacent literals must be false.

A learned clause is created to prevent a clause from creating a conflict during the search process. We can use adjacency tables to create learned SAT clauses. Consider this unsatisfiable X3SAT example:


Compare the adjacency tables for the three literals in $(c,e,g)$:

$Literal | Adjacent$

$c | a, b, \bar c, e, g$

$e | a, c, d, \bar e, g$

$g | a, c, e, f, \bar g$

If one adjacent literal from each row is true then the clause will be empty causing a conflict. We can create a learned clause by choosing one literal from the adjacent column of each row, inverting them, and putting them into a SAT clause. It is best to generate unit and binary clauses first since they will subsume larger clauses. For example, $a$ is adjacent in all three rows. A conflict will occur if $a$ is true. We can create the unit learned clause $(\bar a)$.

These are SAT learned clauses that can be created from the XSAT clause $(c,e,g)$:

$(\bar a)$

$(\bar b \lor \bar c)(\bar c \lor \bar e)(\bar c \lor \bar g)(\bar d \lor \bar e)(\bar e \lor \bar g)(\bar f \lor \bar g)$

$(\bar b \lor \bar d \lor \bar f)(\bar b \lor e \lor \bar f)(\bar b \lor e \lor g)(c \lor \bar d \lor \bar f)(c \lor e \lor g)$

Applying the algorithm to the entire X3SAT instance results in this SAT instance.

$(a \lor b \lor c)(a \lor d \lor e)(a \lor f \lor g)(b \lor d \lor f)(c \lor e \lor g)$

$(\bar a)$

$(\bar b \lor \bar c)( \bar b \lor \bar d)(b \lor \bar e)( \bar b \lor e)( \bar b \lor \bar e)( \bar b \lor \bar f)(b \lor \bar g)( \bar b \lor g)( \bar b \lor \bar g)$

$(c \lor \bar d)( \bar c \lor d)( \bar c \lor \bar d)( \bar c \lor \bar e)(c \lor \bar f)( \bar c \lor f)( \bar c \lor \bar f)( \bar c \lor \bar g)$

$(\bar d \lor \bar e)( \bar d \lor \bar f)(d \lor \bar g)( \bar d \lor g)( \bar d \lor \bar g)$

$(e \lor \bar f)( \bar e \lor f)( \bar e \lor \bar f) (\bar e \lor \bar g)$

$(\bar f \lor \bar g)$

This SAT instance has a short resolution refutation:

$( \bar b \lor e) R ( \bar b \lor \bar e) \rightarrow (\bar b)$

$( \bar c \lor d) R ( \bar c \lor \bar d) \rightarrow (\bar c)$

$(a \lor b \lor c) R (\bar a) R (\bar b) R (\bar c) \rightarrow ()$

I have a more complicated algorithm that creates more learned clauses than this one.

I would also be interested in whether that are any papers about resolution refutations of XSAT instances converted to SAT.



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.