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.