Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

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?

share|improve this question
6  
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
6  
@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
1  
@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
add comment

1 Answer 1

up vote 4 down vote accepted

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.

share|improve this answer
    
Thanks a lot!!! –  Tayfun Pay Mar 12 '13 at 21:19
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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