A First Step Towards a Unified Proof Checker for QBF Export

@incollection{citeulike:6083579, abstract = {Compared to SAT, there is no simple concept of what a solution to a QBF problem is. Furthermore, as the series of QBF evaluations shows, the QBF solvers that are available often disagree. Thus, proof generation for QBF seems to be even more important than for SAT. In this paper we propose a new uniform proof format, which captures refutations and witnesses for a variety of QBF solvers, and is based on a novel extended resolution rule for QBF. Our experiments show the flexibility of this new format. We also identify shortcomings of our format and conjecture that a purely resolution based proof calculus is not powerful enough to trace the most efficient solvers.}, author = {Jussila, Toni and Biere, Armin and Sinz, Carsten and Kr\"{o}ning, Daniel and Wintersteiger, Christoph}, citeulike-article-id = {6083579}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-540-72788-0_21}, citeulike-linkout-1 = {http://www.springerlink.com/content/m8444431nr787303}, doi = {10.1007/978-3-540-72788-0_21}, journal = {Theory and Applications of Satisfiability Testing – SAT 2007}, keywords = {certification, qbf, sat}, pages = {201--214}, posted-at = {2009-11-08 01:06:25}, priority = {2}, title = {A First Step Towards a Unified Proof Checker for QBF}, url = {http://dx.doi.org/10.1007/978-3-540-72788-0_21}, year = {2007} }

TY - CHAP ID - citeulike:6083579 L3 - citeulike-article-id:6083579 N2 - Compared to SAT, there is no simple concept of what a solution to a QBF problem is. Furthermore, as the series of QBF evaluations shows, the QBF solvers that are available often disagree. Thus, proof generation for QBF seems to be even more important than for SAT. In this paper we propose a new uniform proof format, which captures refutations and witnesses for a variety of QBF solvers, and is based on a novel extended resolution rule for QBF. Our experiments show the flexibility of this new format. We also identify shortcomings of our format and conjecture that a purely resolution based proof calculus is not powerful enough to trace the most efficient solvers. JF - Theory and Applications of Satisfiability Testing – SAT 2007 EP - 214 TI - A First Step Towards a Unified Proof Checker for QBF SP - 201 KW - certification KW - qbf KW - sat AU - Jussila, Toni AU - Biere, Armin AU - Sinz, Carsten AU - Kröning, Daniel AU - Wintersteiger, Christoph PY - 2007/// UR - http://dx.doi.org/10.1007/978-3-540-72788-0_21 ER -