<p>The subsumption process I described is called vivification: <a href="https://arxiv.org/abs/1807.11061" rel="nofollow noreferrer">Clause Vivification by Unit Propagation in CDCL SAT Solvers</a></p>
<p>It was used by Glucose which won SAT Competition 2017 and Maple LCM which won Bronze in SAT Competition 2018. It is now used by most SAT Solvers that compete. Some solvers that once used vivification, like Lingeling 271, have removed it.</p>
<p>Vivication is computationally expensive. Most solvers only use it on learned clauses with a small Literal Block Distance (LBD) score: <a href="https://arxiv.org/abs/1904.11106#:%7E:text=A%20state%2Dof%2Dthe%2D,the%20better%20is%20its%20quality" rel="nofollow noreferrer">Characterization of Glue Variables in CDCL SAT Solving</a>. LDB measures the number of distinct decision levels in a given learned clause. The lower the LBD score the better.</p>

CC BY-SA 4.0
2024-10-21T19:09:27.113Z
2024-10-21T19:09:27.113Z
Russell Easterly
<p>I’m interested in finding papers about DPLL+CDCL SAT solvers that try to subsume learned clauses. I found this paper on arxiv: <a href="https://arxiv.org/abs/1906.07508" rel="nofollow noreferrer">Subsumption-driven clause learning with DPLL+restarts</a>.</p>
<p>I’m still studying the paper which seems to search for ways to subsume existing clauses in the SAT instance. My own experience with CDCL solvers is that they often find learned clauses that subsume previously learned clauses. I may have found a way to speed up this subsumption process.</p>
<p>Assume the partial variable assignment where <span class="math-container">$a$</span>, <span class="math-container">$b$</span>, and <span class="math-container">$c$</span> are true causes a contradiction when unit clause propagation is done. A typical CDCL solver would create the learned clause <span class="math-container">$(\bar a \lor \bar b \lor \bar c)$</span>. We can also immediately test if any of the three assignments <span class="math-container">$a b \bar c$</span>, <span class="math-container">$a \bar b c$</span>, or <span class="math-container">$\bar a b c$</span> cause a contradiction. If so, we can subsume the clause <span class="math-container">$(\bar a \lor \bar b \lor \bar c)$</span>. If all three assignments cause a contradiction we can add the learned clauses <span class="math-container">$(\bar a \lor \bar b)$</span>, <span class="math-container">$(\bar a \lor \bar c)$</span>, and <span class="math-container">$(\bar b \lor \bar c)$</span>. All three of these subsume <span class="math-container">$(\bar a \lor \bar b \lor \bar c)$</span>.</p>
<p>I show how this process can speed up a DPLL+CDCL SAT solver on Pigeon Hole problems.</p>
<p>I describe a SAT solver that extends the ideas presented in <a href="https://arxiv.org/abs/1612.05019" rel="nofollow noreferrer">An Early Sign of Satisfiability</a>.</p>
<p>The authors define a “positive clause” as a clause that only has positive literals and a “negative clause” as a clause with only negative literals. All other clauses are called “unipolar”. The basic idea is that a SAT solver only has to find a partial variable assignment the satisfies all of the positive or all of the negative clauses. The remaining clauses can be satisfied by assuming the unassigned variables are all negative if the positive clauses are satisfied or the unassigned variables are all positive if the negative clauses are satisfied. My solver only cares about positive clauses.</p>
<p>Note, clauses can become positive clauses during processing. The clause <span class="math-container">$(a \lor b \lor \bar c)$</span> becomes the positive clause <span class="math-container">$(a \lor b)$</span> if the partial variable assignment sets <span class="math-container">$c$</span> to true.</p>
<p>This is the flow of the positive clause based DPLL-CDCL solver.</p>
<ol>
<li><p>Perform unit clause propagation. If a conflict is found the SAT instance is unsatisfiable.</p>
</li>
<li><p>If there are no non-unit, positive clauses then the SAT instance can be satisfied by assuming all unset variables are false.</p>
</li>
<li><p>Choose the lowest order, unsatisfied, non-unit, positive clause. Set the lowest order, unassigned variable in the clause to true. This is a decision variable.</p>
</li>
<li><p>Perform unit clause propagation. If no conflict is found go to step 2.</p>
</li>
<li><p>Add a learned clause formed by inverting the positive decision variables involved in the conflict.</p>
</li>
<li><p>Try to find subsuming clauses by inverting each decision variable one at a time and performing unit clause propagation. If this causes a conflict then a subsuming clause has been found.</p>
</li>
<li><p>Undo all variable assignments and restart at step 1. Keep all learned clauses.</p>
</li>
</ol>
<p>I will use the 4 pigeons in 3 holes problem as an example.</p>
<p><span class="math-container">$(a1 \lor a2 \lor a3)(b1 \lor b2 \lor b3)(c1 \lor c2 \lor c3)(d1 \lor d2 \lor d3)$</span></p>
<p><span class="math-container">$(\bar {a1} \lor  \bar {b1})(\bar {a1} \lor  \bar {c1})(\bar {a1} \lor  \bar {d1})(\bar {b1} \lor  \bar {c1})(\bar {b1} \lor  \bar {d1})(\bar {c1} \lor  \bar {d1})$</span></p>
<p><span class="math-container">$(\bar {a2} \lor  \bar {b2})(\bar {a2} \lor  \bar {c2})(\bar {a2} \lor  \bar {d2})(\bar {b2} \lor  \bar {c2})(\bar {b2} \lor  \bar {d2})(\bar {c2} \lor  \bar {d2})$</span></p>
<p><span class="math-container">$(\bar {a3} \lor  \bar {b3})(\bar {a3} \lor  \bar {c3})(\bar {a3} \lor  \bar {d3})(\bar {b3} \lor  \bar {c3})(\bar {b3} \lor  \bar {d3})(\bar {c3} \lor  \bar {d3})$</span></p>
<p>There are no unit clauses in the original instance so there is no contradiction from unit clause propagation. The lowest order, non-unit, positive clause is <span class="math-container">$(a1 \lor a2 \lor a3)$</span>. Set <span class="math-container">$a1$</span> to true. Unit clause propagation does not cause a contradiction. <span class="math-container">$(b2 \lor b3)$</span> is now the lowest order, non-unit, positive clause. Setting <span class="math-container">$b2$</span> to true does cause a contradiction.</p>
<p>Add the learned clause <span class="math-container">$(\bar {a1} \lor \bar {b2})$</span>. Perform unit clause propagation on the assignments <span class="math-container">$a1 \bar {b2}$</span> and <span class="math-container">$\bar {a1} b2$</span>. Both of these assignments cause contradictions. Replace the learned clause <span class="math-container">$(\bar {a1} \lor \bar {b2})$</span> with the clauses <span class="math-container">$(\bar {a1})$</span> and <span class="math-container">$(\bar {b2})$</span>. Undo all variable assignments and restart at step 1.</p>
<p>The new learned unit clauses do not cause a contradiction when unit clause propagation is performed. The lowest order, non-unit, positive clause is <span class="math-container">$(a2 \lor a3)$</span>. Set <span class="math-container">$a2$</span> to true. This does not cause a contradiction. The lowest order, positive clause is now <span class="math-container">$(b1 \lor b3)$</span>. Set <span class="math-container">$b1$</span> to true. This does cause a contradiction. Test the assignments <span class="math-container">$a2 \bar {b1}$</span> and <span class="math-container">$\bar {a2} b1$</span>. Both assignments cause contradictions. Add the learned clauses <span class="math-container">$(\bar {a2})$</span> and <span class="math-container">$(\bar {b1})$</span> to the instance. Restart.</p>
<p>The four learned unit clauses <span class="math-container">$(\bar {a1})$</span>, <span class="math-container">$(\bar {a2})$</span>, <span class="math-container">$(\bar {b1})$</span>, and <span class="math-container">$(\bar {b2})$</span> cause a contradiction proving the instance is unsatisfiable.</p>
<p>Is this technique for subsuming learned clauses known? Are there any similar techniques? I would be interested in any references to SAT solvers that try to subsume clauses.</p>

<reference-request><sat><resolution>
Subsuming Learned Clauses
Russell Easterly
# Subsuming Learned Clauses

(Asked by: username_0 on 2024-06-29)

I’m interested in finding papers about DPLL+CDCL SAT solvers that try to subsume learned clauses. I found this paper on arxiv: [Subsumption-driven clause learning with DPLL+restarts](https://arxiv.org/abs/1906.07508).

I’m still studying the paper which seems to search for ways to subsume existing clauses in the SAT instance. My own experience with CDCL solvers is that they often find learned clauses that subsume previously learned clauses. I may have found a way to speed up this subsumption process.

Assume the partial variable assignment where $a$, $b$, and $c$ are true causes a contradiction when unit clause propagation is done. A typical CDCL solver would create the learned clause $(\bar a \lor \bar b \lor \bar c)$. We can also immediately test if any of the three assignments $a b \bar c$, $a \bar b c$, or $\bar a b c$ cause a contradiction. If so, we can subsume the clause $(\bar a \lor \bar b \lor \bar c)$. If all three assignments cause a contradiction we can add the learned clauses $(\bar a \lor \bar b)$, $(\bar a \lor \bar c)$, and $(\bar b \lor \bar c)$. All three of these subsume $(\bar a \lor \bar b \lor \bar c)$.

I show how this process can speed up a DPLL+CDCL SAT solver on Pigeon Hole problems.

I describe a SAT solver that extends the ideas presented in [An Early Sign of Satisfiability](https://arxiv.org/abs/1612.05019).

The authors define a “positive clause” as a clause that only has positive literals and a “negative clause” as a clause with only negative literals. All other clauses are called “unipolar”. The basic idea is that a SAT solver only has to find a partial variable assignment the satisfies all of the positive or all of the negative clauses. The remaining clauses can be satisfied by assuming the unassigned variables are all negative if the positive clauses are satisfied or the unassigned variables are all positive if the negative clauses are satisfied. My solver only cares about positive clauses.

Note, clauses can become positive clauses during processing. The clause $(a \lor b \lor \bar c)$ becomes the positive clause $(a \lor b)$ if the partial variable assignment sets $c$ to true.

This is the flow of the positive clause based DPLL-CDCL solver.

1. Perform unit clause propagation. If a conflict is found the SAT instance is unsatisfiable.
2. If there are no non-unit, positive clauses then the SAT instance can be satisfied by assuming all unset variables are false.
3. Choose the lowest order, unsatisfied, non-unit, positive clause. Set the lowest order, unassigned variable in the clause to true. This is a decision variable.
4. Perform unit clause propagation. If no conflict is found go to step 2.
5. Add a learned clause formed by inverting the positive decision variables involved in the conflict.
6. Try to find subsuming clauses by inverting each decision variable one at a time and performing unit clause propagation. If this causes a conflict then a subsuming clause has been found.
7. Undo all variable assignments and restart at step 1. Keep all learned clauses.

I will use the 4 pigeons in 3 holes problem as an example.

$(a1 \lor a2 \lor a3)(b1 \lor b2 \lor b3)(c1 \lor c2 \lor c3)(d1 \lor d2 \lor d3)$

$(\bar {a1} \lor \bar {b1})(\bar {a1} \lor \bar {c1})(\bar {a1} \lor \bar {d1})(\bar {b1} \lor \bar {c1})(\bar {b1} \lor \bar {d1})(\bar {c1} \lor \bar {d1})$

$(\bar {a2} \lor \bar {b2})(\bar {a2} \lor \bar {c2})(\bar {a2} \lor \bar {d2})(\bar {b2} \lor \bar {c2})(\bar {b2} \lor \bar {d2})(\bar {c2} \lor \bar {d2})$

$(\bar {a3} \lor \bar {b3})(\bar {a3} \lor \bar {c3})(\bar {a3} \lor \bar {d3})(\bar {b3} \lor \bar {c3})(\bar {b3} \lor \bar {d3})(\bar {c3} \lor \bar {d3})$

There are no unit clauses in the original instance so there is no contradiction from unit clause propagation. The lowest order, non-unit, positive clause is $(a1 \lor a2 \lor a3)$. Set $a1$ to true. Unit clause propagation does not cause a contradiction. $(b2 \lor b3)$ is now the lowest order, non-unit, positive clause. Setting $b2$ to true does cause a contradiction.

Add the learned clause $(\bar {a1} \lor \bar {b2})$. Perform unit clause propagation on the assignments $a1 \bar {b2}$ and $\bar {a1} b2$. Both of these assignments cause contradictions. Replace the learned clause $(\bar {a1} \lor \bar {b2})$ with the clauses $(\bar {a1})$ and $(\bar {b2})$. Undo all variable assignments and restart at step 1.

The new learned unit clauses do not cause a contradiction when unit clause propagation is performed. The lowest order, non-unit, positive clause is $(a2 \lor a3)$. Set $a2$ to true. This does not cause a contradiction. The lowest order, positive clause is now $(b1 \lor b3)$. Set $b1$ to true. This does cause a contradiction. Test the assignments $a2 \bar {b1}$ and $\bar {a2} b1$. Both assignments cause contradictions. Add the learned clauses $(\bar {a2})$ and $(\bar {b1})$ to the instance. Restart.

The four learned unit clauses $(\bar {a1})$, $(\bar {a2})$, $(\bar {b1})$, and $(\bar {b2})$ cause a contradiction proving the instance is unsatisfiable.

Is this technique for subsuming learned clauses known? Are there any similar techniques? I would be interested in any references to SAT solvers that try to subsume clauses.

**Tags:** reference-request, sat, resolution

---

## 1 answers

### Answer by username_0 on 2024-10-21. Score: 1

The subsumption process I described is called vivification: [Clause Vivification by Unit Propagation in CDCL SAT Solvers](https://arxiv.org/abs/1807.11061)

It was used by Glucose which won SAT Competition 2017 and Maple LCM which won Bronze in SAT Competition 2018. It is now used by most SAT Solvers that compete. Some solvers that once used vivification, like Lingeling 271, have removed it.

Vivication is computationally expensive. Most solvers only use it on learned clauses with a small Literal Block Distance (LBD) score: [Characterization of Glue Variables in CDCL SAT Solving](https://arxiv.org/abs/1904.11106#:%7E:text=A%20state%2Dof%2Dthe%2D,the%20better%20is%20its%20quality). LDB measures the number of distinct decision levels in a given learned clause. The lower the LBD score the better.


---

