Lee Barnett, Armin Biere,
"Non-Clausal Redundancy Properties (Extended Version)"
, Serie FMV Reports Series, Vol. 21/2, Institute for Formal Models and Verification, Linz, 4-2021
State-of-the-art refutation systems for SAT are largely based
on the derivation of clauses meeting some redundancy criteria, ensuring
their addition to a formula does not alter its satisfiability. However, there
are strong propositional reasoning techniques whose inferences are not
easily expressed in such systems. This paper extends the redundancy
framework beyond clauses to characterize redundancy for Boolean con-
straints in general. We show this characterization can be instantiated to
develop efficiently checkable refutation systems using redundancy prop-
erties for Binary Decision Diagrams (BDDs). Using a form of reverse
unit propagation over conjunctions of BDDs, these systems capture, for
instance, Gaussian elimination reasoning over XOR constraints encoded
in a formula, without the need for clausal translations or extension vari-
ables. Notably, these systems generalize those based on the strong Prop-
agation Redundancy (PR) property, without an increase in complexity.