Non-clausal Redundancy Properties

State-of-the-art refutation systems for SAT are largely basedon the derivation of clauses meeting some redundancy criteria, ensuringtheir addition to a formula does not alter its satisfiability. However, thereare strong propositional reasoning techniques whose inferences are noteasily expressed in such systems. This paper extends the redundancyframework beyond clauses to characterize redundancy for Boolean con-straints in general. We show this characterization can be instantiated todevelop efficiently checkable refutation systems using redundancy prop-erties for Binary Decision Diagrams (BDDs). Using a form of reverseunit propagation over conjunctions of BDDs, these systems capture, forinstance, Gaussian elimination reasoning over XOR constraints encodedin 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.