5
$\begingroup$

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?

Improve this question
$\endgroup$
4
  • 6
    $\begingroup$ 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.) $\endgroup$
    – Ryan Williams
    Dec 1, 2012 at 22:31
  • 7
    $\begingroup$ @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. $\endgroup$
    – Kyle Jones
    Dec 2, 2012 at 4:50
  • 2
    $\begingroup$ @Kyle - Your comment sounds like an answer... $\endgroup$
    – Xavier Labouze
    Dec 4, 2012 at 10:14
  • $\begingroup$ @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 $\endgroup$
    – Tayfun Pay
    Dec 8, 2012 at 22:32

1 Answer 1

Reset to default
5
$\begingroup$

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.

Improve this answer
$\endgroup$
0

Your Answer

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

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