Non-clausal redundancy properties
Abstract: 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 constraints in general. We show this characterization can be instantiated to develop efficiently checkable refutation systems using redundancy properties 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 variables. Notably, these systems generalize those based on the strong Propagation Redundancy (PR) property, without an increase in complexity
- Standort
-
Deutsche Nationalbibliothek Frankfurt am Main
- Umfang
-
Online-Ressource
- Sprache
-
Englisch
- Anmerkungen
-
ISBN: 978-3-030-79876-5
ISSN: 1611-3349
- Ereignis
-
Veröffentlichung
- (wo)
-
Freiburg
- (wer)
-
Universität
- (wann)
-
2023
- Urheber
- DOI
-
10.1007/978-3-030-79876-5_15
- URN
-
urn:nbn:de:bsz:25-freidok-2393763
- Rechteinformation
-
Open Access; Der Zugriff auf das Objekt ist unbeschränkt möglich.
- Letzte Aktualisierung
-
14.08.2025, 10:58 MESZ
Datenpartner
Deutsche Nationalbibliothek. Bei Fragen zum Objekt wenden Sie sich bitte an den Datenpartner.
Beteiligte
- Barnett, Lee A.
- Biere, Armin
- Universität
Entstanden
- 2023
Ähnliche Objekte (12)
Redundancy in distributed proofs
Encoding Redundancy for Satisfaction-Driven Clause Learning
Local redundancy in SAT: generalizations of blocked clauses
Time redundancy
Global data on earthworm abundance, biomass, diversity and corresponding environmental properties
Transport properties in non-Fermi liquid phases of nodal-point semimetals
Efficiency in redundancy
Dislocation arrangements in 4H-SiC and their influence on the local crystal lattice properties
Colluvial sediments originating from past land-use activities in the Erzgebirge Mountains, Central Europe: occurrence, properties, and historic environmental implications
Microscopic strain mapping in polymers equipped with non-covalent mechanochromic motifs
A theoretical study of the energy‐harvesting properties of non‐tracking semicircular concentrating troughs
CRC (Cyclic Redundancy Check)
Redundancy in distributed proofs
Encoding Redundancy for Satisfaction-Driven Clause Learning
Local redundancy in SAT: generalizations of blocked clauses
Time redundancy
Global data on earthworm abundance, biomass, diversity and corresponding environmental properties
Transport properties in non-Fermi liquid phases of nodal-point semimetals
Efficiency in redundancy
Dislocation arrangements in 4H-SiC and their influence on the local crystal lattice properties
Colluvial sediments originating from past land-use activities in the Erzgebirge Mountains, Central Europe: occurrence, properties, and historic environmental implications
Microscopic strain mapping in polymers equipped with non-covalent mechanochromic motifs
A theoretical study of the energy‐harvesting properties of non‐tracking semicircular concentrating troughs
CRC (Cyclic Redundancy Check)
Redundancy in distributed proofs
Encoding Redundancy for Satisfaction-Driven Clause Learning
Local redundancy in SAT: generalizations of blocked clauses
Time redundancy
Global data on earthworm abundance, biomass, diversity and corresponding environmental properties
Transport properties in non-Fermi liquid phases of nodal-point semimetals
Efficiency in redundancy
Dislocation arrangements in 4H-SiC and their influence on the local crystal lattice properties
Colluvial sediments originating from past land-use activities in the Erzgebirge Mountains, Central Europe: occurrence, properties, and historic environmental implications
Microscopic strain mapping in polymers equipped with non-covalent mechanochromic motifs
A theoretical study of the energy‐harvesting properties of non‐tracking semicircular concentrating troughs