<p>Pure literal elimination over base clauses is effectively deleting those clauses from the formula, an action which cannot be encoded in a RUP proof since such proofs only encode clause additions.  But since an unsatisfiable formula will be unsatisfiable even without the clauses that contain pure literals you can treat the formula as if those clauses were not present.  Any RUP proof of the unsatisfiability of the formula with those clauses missing will also be a RUP proof of the unsatisfiability of the original formula.</p>
<p>As for the second example, you can't validly add <span class="math-container">$(\lnot A \lor \lnot B)$</span> to the proof because that clause isn't an actual requirement to satisfy the formula.  <span class="math-container">$A$</span> dominating <span class="math-container">$B$</span> after a partial assignment doesn't indicate that <span class="math-container">$\lnot B$</span> is mandatory, rather it means that asserting <span class="math-container">$B$</span> isn't helpful.  In fact, it might be a bad thing to do if <span class="math-container">$\lnot B$</span> is needed to satisfy some clauses later.  If you assert <span class="math-container">$\lnot B$</span> to satisfy all clauses containing <span class="math-container">$\lnot B$</span> you can be confident that <span class="math-container">$B$</span> will never appear in a downstream conflict clause and thus will never be part of a RUP clause generated by this partial assignment.  So asserting <span class="math-container">$\lnot B$</span> can't hurt but you can't be sure that it is <em>necessary</em>.  RUP proof clauses state only what is necessary.</p>

CC BY-SA 4.0
2020-09-02T21:59:51.103Z
2020-09-02T21:59:51.103Z
Kyle Jones
<p>I'm exploring building a CDCL SAT-solver with interesting reduction rules. I have two rules based on pure literal elimination, but if either of these rules generate a conflict, I don't know what to report for an RUP (reverse unit propagation) proof.</p>
<p>The first is pure-literal elimination over &quot;base&quot; clauses. That is, if a literal shows up with only one sign among the original clauses (but can still have the opposite sign in learnt clauses), then we set it.</p>
<p>The second is &quot;would-be&quot; pure-literal elimination binary clauses. If, among base (not learnt) clauses, literal <code>A</code> <em>dominates</em> literal <code>B</code> (but does not dominate <code>-B</code>) in the sense that every remaining unsatisfied rule containing <code>B</code> <em>also</em> contains <code>A</code>, then <em>temporarily</em> (while searching this branch) add the rule <code>-A \/ -B</code> since by setting <code>A</code> we would infer <code>-B</code> via pure literal elimination.</p>
<p>For both of these operations, it's easy to show that if a solution exists, then a solution still exists after applying the operation. But these rules can't be inferred via RUP and so it's unclear what to do in terms of providing a proof when they show up in a conflict.</p>

<sat>
Translating pure literal elimination into rup
dspyz
# Translating pure literal elimination into rup

(Asked by: username_0 on 2020-08-31)

I'm exploring building a CDCL SAT-solver with interesting reduction rules. I have two rules based on pure literal elimination, but if either of these rules generate a conflict, I don't know what to report for an RUP (reverse unit propagation) proof.

The first is pure-literal elimination over "base" clauses. That is, if a literal shows up with only one sign among the original clauses (but can still have the opposite sign in learnt clauses), then we set it.

The second is "would-be" pure-literal elimination binary clauses. If, among base (not learnt) clauses, literal `A` *dominates* literal `B` (but does not dominate `-B`) in the sense that every remaining unsatisfied rule containing `B` *also* contains `A`, then *temporarily* (while searching this branch) add the rule `-A \/ -B` since by setting `A` we would infer `-B` via pure literal elimination.

For both of these operations, it's easy to show that if a solution exists, then a solution still exists after applying the operation. But these rules can't be inferred via RUP and so it's unclear what to do in terms of providing a proof when they show up in a conflict.

**Tags:** sat

---

## 1 answers

### Answer by username_1 on 2020-09-02. Score: 1

Pure literal elimination over base clauses is effectively deleting those clauses from the formula, an action which cannot be encoded in a RUP proof since such proofs only encode clause additions. But since an unsatisfiable formula will be unsatisfiable even without the clauses that contain pure literals you can treat the formula as if those clauses were not present. Any RUP proof of the unsatisfiability of the formula with those clauses missing will also be a RUP proof of the unsatisfiability of the original formula.

As for the second example, you can't validly add $(\lnot A \lor \lnot B)$ to the proof because that clause isn't an actual requirement to satisfy the formula. $A$ dominating $B$ after a partial assignment doesn't indicate that $\lnot B$ is mandatory, rather it means that asserting $B$ isn't helpful. In fact, it might be a bad thing to do if $\lnot B$ is needed to satisfy some clauses later. If you assert $\lnot B$ to satisfy all clauses containing $\lnot B$ you can be confident that $B$ will never appear in a downstream conflict clause and thus will never be part of a RUP clause generated by this partial assignment. So asserting $\lnot B$ can't hurt but you can't be sure that it is *necessary*. RUP proof clauses state only what is necessary.


---

