Zur Seitenansicht
 

Titelaufnahme

Titel
DRAT proofs for XOR reasoning
VerfasserRebola-Pardo, Adrian ; Tobias, Philipp
Erschienen in
Logics in Artificial Intelligence, 15th European Conference, JELIA 2016, Larnaca, Cyprus, November 9-11, 2016, Proceedings / Loizos, Michael, Cham, 2016, S. 415-429
Erschienen2016
Ausgabe
Accepted version
SpracheEnglisch
SerieLecture Notes in Computer Science ; 10021
DokumenttypAufsatz in einem Sammelwerk
Projekt-/ReportnummerAustrian Science Fund (FWF): W1255-N23
Projekt-/ReportnummerVienna Science and Technology Fund (WWTF): VRG11-005
ISBN978-3-319-48757-1
URNurn:nbn:at:at-ubtuw:3-3026 Persistent Identifier (URN)
DOI10.1007/978-3-319-48758-8_27 
Zugriffsbeschränkung
 Das Werk ist frei verfügbar
Dateien
DRAT proofs for XOR reasoning [0.38 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Englisch)

Unsatisfiability proofs in the DRAT format became the de facto standard to increase the reliability of contemporary SAT solvers. We consider the problem of generating proofs for the XOR reasoning component in SAT solvers and propose two methods: direct translation transforms every XOR constraint addition inference into a DRAT proof, whereas T-translation avoids the exponential blow-up in direct translations by using fresh variables. T-translation produces DRAT proofs from Gaussian elimination records that are polynomial in the size of the input CNF formula. Experiments show that a combination of both approaches with a simple prediction method outperforms the BDD-based method.

Notiz
Lizenz
CC-BY-Lizenz (4.0)Creative Commons Namensnennung 4.0 International Lizenz