Non-Clausal Redundancy Properties (Extended Version)

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.