<p>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.</p>

CC BY-SA 3.0
2013-03-11T00:41:13.570Z
2013-03-11T00:41:13.570Z
Kyle Jones
<p>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.</p>

<p>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? </p>

CC BY-SA 3.0
2012-12-01T22:31:07.920Z
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
CC BY-SA 3.0
2012-12-02T04:50:18.430Z
@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
CC BY-SA 3.0
2012-12-04T10:14:27.763Z
@Kyle - Your comment sounds like an answer...
Xavier Labouze
CC BY-SA 3.0
2012-12-08T22:32:14.650Z
@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
<cc.complexity-theory>
Eliminating clauses from a CNF formula based on their unsatisfying truth assignments being covered by some other clause
Tayfun Pay
# Eliminating clauses from a CNF formula based on their unsatisfying truth assignments being covered by some other clause

(Asked by: username_0 on 2012-12-01)

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?

**Tags:** cc.complexity-theory

> **Comments:**
> **username_1**: 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.)  
> **username_2**: @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.  
> **username_3**: @Kyle - Your comment sounds like an answer...  
> **username_0**: @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  

---

## 1 answers

### Answer by username_2 on 2013-03-11. Score: 6 | Accepted answer

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.


---

