Polynomial-Time Validation of QCDCL Certificates (bibtex)
by Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
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.
Reference:
Polynomial-Time Validation of QCDCL CertificatesTomáš Peitl, Friedrich Slivovsky, Stefan SzeiderTheory and Applications of Satisfiability Testing – SAT 2018 (Olaf Beyersdorff, Christoph M. Wintersteiger, eds.), pages 253–269, 2018, Springer International Publishing.
Bibtex Entry:
@InProceedings{PeitlSlivovskySzeider18,
    author="Peitl, Tom{\'a}{\v{s}}
            and Slivovsky, Friedrich
            and Szeider, Stefan",
    editor="Beyersdorff, Olaf
            and Wintersteiger, Christoph M.",
    title="Polynomial-Time Validation of QCDCL Certificates",
    booktitle="Theory and Applications of Satisfiability Testing -- SAT 2018",
    year="2018",
    publisher="Springer International Publishing",
    address="Cham",
    pages="253--269",
    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.",
    isbn="978-3-319-94144-8",
    doi="https://doi.org/10.1007/978-3-319-94144-8_16",
    url="https://www.ac.tuwien.ac.at/files/tr/ac-tr-18-003.pdf"
}
Powered by bibtexbrowser