Are there any techniques for checking whether a clause is subsumed by another clause when adding it to a cnf formula?

Question

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?

Answer 1

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