The final publication is available via <a href="https://doi.org/10.1007/978-3-319-48758-8_27" target="_blank">https://doi.org/10.1007/978-3-319-48758-8_27</a>.
-
dc.description.abstract
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.
en
dc.description.sponsorship
Wiener Wissenschafts-, Forschungs- und Technologiefonds (WWTF)
-
dc.description.sponsorship
Austrian Science Funds (FWF)
-
dc.language
English
-
dc.language.iso
en
-
dc.relation.ispartofseries
Lecture Notes in Computer Science
-
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
-
dc.title
DRAT proofs for XOR reasoning
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Creative Commons Namensnennung 4.0 International
de
dc.rights.license
Creative Commons Attribution 4.0 International
en
dc.relation.publication
Logics in Artificial Intelligence, 15th European Conference, JELIA 2016, Larnaca, Cyprus, November 9-11, 2016, Proceedings ; Loizos, Michael
-
dc.relation.isbn
9783319487571
-
dc.relation.grantno
VRG11-005
-
dc.relation.grantno
W1255-N23
-
dc.rights.holder
Springer International Publishing AG 2016
-
dc.type.category
Full-Paper Contribution
-
tuw.container.volume
10021
-
tuw.relation.publisher
Cham
-
tuw.version
am
-
tuw.publication.orgunit
E192 - Institut für Informationssysteme
-
tuw.publisher.doi
10.1007/978-3-319-48758-8_27
-
dc.identifier.libraryid
AC11362485
-
dc.identifier.urn
urn:nbn:at:at-ubtuw:3-3026
-
tuw.author.orcid
0000-0001-9234-4377
-
dc.rights.identifier
CC BY 4.0
de
dc.rights.identifier
CC BY 4.0
en
item.fulltext
with Fulltext
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.cerifentitytype
Publications
-
item.openairetype
conference paper
-
item.grantfulltext
open
-
item.openaccessfulltext
Open Access
-
item.languageiso639-1
en
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering