Go to page
 

Bibliographic Metadata

Title
DRAT proofs for XOR reasoning
AuthorRebola-Pardo, Adrian ; Tobias, Philipp
Published in
Logics in Artificial Intelligence, 15th European Conference, JELIA 2016, Larnaca, Cyprus, November 9-11, 2016, Proceedings / Loizos, Michael, Cham, 2016, page 415-429
Published2016
Edition
Accepted version
LanguageEnglish
SeriesLecture Notes in Computer Science ; 10021
Document typeArticle in a collected edition
Project-/ReportnumberAustrian Science Fund (FWF): W1255-N23
Project-/ReportnumberVienna 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 
Restriction-Information
 The work is publicly available
Files
DRAT proofs for XOR reasoning [0.38 mb]
Links
Reference
Classification
Abstract (English)

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.

Note
Stats
The PDF-Document has been downloaded 27 times.
License
CC-BY-License (4.0)Creative Commons Attribution 4.0 International License