Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
T. Philipp, A. Rebola Pardo:
"DRAT Proofs for XOR Reasoning";
Vortrag: European Conference on Logics in Artificial Intelligence (JELIA),
Cyprus;
09.11.2016
- 11.11.2016; in: "Logics in Artificial Intelligence",
Springer,
Lecture Notes in Computer Science/10021
(2016),
S. 415
- 429.
Kurzfassung 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.
Schlagworte:
proof systems, satisfiability solvers
"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-319-48758-8_27
Zugeordnete Projekte:
Projektleitung Georg Weissenbacher:
Bit-level Accurate Reasoning and Interpolation
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.