Title: DRAT proofs for XOR reasoning
Language: English
Authors: Rebola-Pardo, Adrian 
Tobias, Philipp 
Issue Date: 2016
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.
URI: https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:3-3026
Library ID: AC11362485
Organisation: E192 - Institut für Informationssysteme 
Publication Type: Inproceedings
Appears in Collections:Conference Paper

Files in this item:

Page view(s)

checked on Aug 18, 2021


checked on Aug 18, 2021

Google ScholarTM


This item is licensed under a Creative Commons License Creative Commons