2
$\begingroup$

When doing variable elimination on a formula in cnf form, there is created a lot of new clauses. Is there any efficient way to check if these are subsumed by other, already existing clauses?

$\endgroup$
4
$\begingroup$

There is a preprocessing method called vivification$^1$ that can be used to detect subsumed clauses. It relies on unit propagation to work.

To vivify a clause, make a partial variable assignment such that all the proposed clause's literals are false. E.g. if your proposed clause is $x_1 \lor \lnot{x_2} \lor x_3 \lor \lnot{x_4}$, assign $x_1$ = FALSE, $x_2$ = TRUE, $x_3$ = FALSE, and $x_4$ = TRUE. If while you're doing these assignments unit propagation produces a conflict, or if one of the variables is set by unit propagation and vivification later wants to set it to a different value, then the new clause is implied by the existing formula and can be discarded as redundant.


$^1$"Vivifying Propositional Clausal Formulae" by Cédric PIETTE, Youssef HAMADI and Lakhdar SAÏS

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.