Lee Barnett, Armin Biere,
"Non-clausal Redundancy Properties"
: Proc. 28th International Conference on Automated Deduction(CADE 28), Serie Lecture Notes in Computer Science (LNCS), Vol. volume 12699, Springer, Seite(n) 252-272, 7-2021
Original Titel:
Non-clausal Redundancy Properties
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 28th International Conference on Automated Deduction(CADE 28)
Original Kurzfassung:
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.
Forschungs-