# Eliminating clauses from a CNF formula based on their unsatisfying truth assignments being covered by some other clause

We are given a Boolean formula in Conjunctive Normal Form (CNF) with $n$ variables and $m$ clauses, where we do not allow repetition of clauses in a given formula and we do not allow repetition of variables in a given clause. Then it is well known that we can have up to $3^n-1$ distinct clauses.

What I would like to know is the complexity of eliminating clauses where their unsatisfying assignments are already covered by some other clause. For example, given the following CNF formula $\{ (a,b,c,d), (a,b,c,\bar{d}), (a,\bar{b},c,d), (a,b,c), (a,b,d), (b,c,d), (c,d) \}.$ After we eliminate the clauses where their unsatisfying truth assignments are already covered by some other clause we get following CNF formula $\{ (a,b,c), (a,b,d), (c,d) \}.$ How fast can this be done for an arbitrary formula? Could it be done in polynomial time in terms of the length of the input?

• I presume by "$C'$ is covered by some other clause $C$" you mean this: "$C \Rightarrow C'$ is a tautology." If that's the case, then why doesn't the obvious greedy algorithm work? (For each pair of clauses $C$, $C'$, remove $C'$ if $C$ implies $C'$. Repeat until no such pair exists.) – Ryan Williams Dec 1 '12 at 22:31
• @Tayfun What you're describing is called subsumption; it is a standard CNF simplification technique for SAT solvers. None of the operations involved is worse than quadratic to either the number of variables or number of clauses in the formula. – Kyle Jones Dec 2 '12 at 4:50
• @Kyle - Your comment sounds like an answer... – Xavier Labouze Dec 4 '12 at 10:14
• @RyanWilliam,KyleJones. I waited a week to see if there were any other comments or answers. Anyways, then can we also assume, on top of assuming that there are no repetition of clauses in a given formula and no repetition of variables in a given clause, that "there does not exists any clause whose unsatisfying truth assignments are already covered by some other clause" and then run our SAT algorithm? Such that "subsumption" is not counted in the computation time of our SAT algorithm? Thanks – Tayfun Pay Dec 8 '12 at 22:32