Florian Lonsing, Uwe Egly, Martina Seidl,
"Q-Resolution with Generalized Axioms"
, in Nadia Creignou, Daniel Le Berre: Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Serie Lecture Notes in Computer Science (LNCS), Vol. 9710, Springer, Seite(n) 435-452, 2016
Original Titel:
Q-Resolution with Generalized Axioms
Sprache des Titels:
Englisch
Original Buchtitel:
Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016
Original Kurzfassung:
Q-resolution is a proof system for quantified Boolean formulas (QBFs) in prenex conjunctive normal form (PCNF) which underlies search-based QBF solvers with clause and cube learning (QCDCL). With the aim to derive and learn stronger clauses and cubes earlier in the search, we generalize the axioms of the Q-resolution calculus resulting in an exponentially more powerful proof system. The generalized axioms introduce an interface of Q-resolution to any other QBF proof system allowing for the direct combination of orthogonal solving techniques. We implemented a variant of the Q-resolution calculus with generalized axioms in the QBF solver DepQBF. As two case studies, we apply integrated SAT solving and resource-bounded QBF preprocessing during the search to heuristically detect potential axiom applications. Experiments with application benchmarks indicate a substantial performance improvement.
Forschungs-