# Translating pure literal elimination into rup

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.

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.