Translating pure literal elimination into rup

Question

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.

Answer 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.