Thursday, November 3, 2016
Speaker: Adrian Rebola Pardo
Venue: IST Austria
Thursday, 4pm, Mondi 3
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 transla-
tions 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.