Paper Info
Title
Polynomial-Time Validation of QCDCL Certificates.
Abstract
Quantified Boolean Formulas (QBFs) offer compact encodings 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 representation 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 substituting 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 extracted to directly generate a (propositional) proof of the validation formula 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.
Year
DOI
Venue
2018
10.1007/978-3-319-94144-8_16
Lecture Notes in Computer Science
Field
DocType
Volume
Discrete mathematics,Computer science,Correctness,Boolean satisfiability problem,Automated proof checking,Theoretical computer science,Mathematical proof,Constraint learning,Time complexity,Propositional formula,Certificate
Conference
10929
ISSN
Citations 
PageRank 
0302-9743
0
0.34
References 
Authors
20
3
Name
Order
Citations
PageRank
Tomás Peitl164.82
Friedrich Slivovsky2627.96
Stefan Szeider3134199.97