<div class="csl-bib-body">
<div class="csl-entry">Peitl, T., Slivovsky, F., & Szeider, S. (2018). Polynomial-Time Validation of QCDCL Certificates. In O. Beyersdorff & C. M. Wintersteiger (Eds.), <i>Theory and Applications of Satisfiability Testing – SAT 2018</i> (pp. 253–269). Springer-Verlag, Lecture Notes in Artificial Intelligence 8268. https://doi.org/10.1007/978-3-319-94144-8_16</div>
</div>
-
dc.identifier.isbn
9783319941448
-
dc.identifier.isbn
9783319941431
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/57505
-
dc.description.abstract
Abstract. Quantified Boolean Formulas (QBFs) o er compact encod-ings of problems arising in areas such as verification and synthesis. These applications require that QBF solvers not only decide whether an input formula is true or false but also output a witnessing certificate, i.e. a rep-resentation of the winning strategy. State-of-the-art QBF solvers based on Quantified Conflict-Driven Constraint Learning (QCDCL) can emit Q-resolution proofs, from which in turn such certificates can be extracted. The correctness of a certificate generated in this way is validated by sub-stituting it into the matrix of the input QBF and using a SAT solver to check that the resulting propositional formula (the validation formula) is unsatisfiable. This final check is often the most time-consuming part of the entire certification workflow. We propose a new validation method that does not require a SAT call and provably runs in polynomial time. It uses the Q-resolution proof from which the given certificate was ex-tracted to directly generate a (propositional) proof of the validation for-mula in the RUP format, which can be verified by a proof checker such as DRAT-trim. Experiments with a prototype implementation show a robust, albeit modest, increase in the number of successfully validated certificates compared to validation with a SAT solver.
en
dc.publisher
Springer-Verlag, Lecture Notes in Artificial Intelligence 8268
-
dc.relation.ispartofseries
Lecture Notes in Computer Science
-
dc.title
Polynomial-Time Validation of QCDCL Certificates
-
dc.type
Konferenzbeitrag
de
dc.type
Inproceedings
en
dc.relation.publication
Theory and Applications of Satisfiability Testing – SAT 2018
-
dc.relation.isbn
978-3-319-94143-1
-
dc.relation.doi
10.1007/978-3-319-94144-8
-
dc.relation.issn
0302-9743
-
dc.description.startpage
253
-
dc.description.endpage
269
-
dc.type.category
Full-Paper Contribution
-
dc.relation.eissn
1611-3349
-
tuw.booktitle
Theory and Applications of Satisfiability Testing – SAT 2018
-
tuw.peerreviewed
true
-
tuw.relation.publisher
Springer
-
tuw.relation.publisherplace
Cham
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.value
100
-
tuw.publication.orgunit
E192-01 - Forschungsbereich Algorithms and Complexity