Talks and Poster Presentations (with Proceedings-Entry):
V. Balabanov, J. Jiang, M. Janota, M. Widl:
"Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs";
Talk: 2nd International Workshop on Quantified Boolean Formulas,
Wien;
2014-07-13; in: "2nd International Workshop on Quantified Boolean Formulas",
(2014),
13 pages.
English abstract:
Resolution is a fundamental part of modern search and learning based QBF solvers, and the extraction of Skolem-function models and Herbrand-function countermodels from QBF resolution proofs is a key enabler for various applications. Although long-distance resolution (LQ-resolution) came into existence a decade ago, its superiority to short-distance resolution (Q-resolution) was not recognized until recently. It remains open whether there exists a polynomial time algorithm for model and countermodel extraction from LQ-resolution proofs, although an efficient algorithm does exist for the Q-resolution counterparts. This paper settles this open problem affirmatively by constructing a linear-time extraction procedure. Experimental results show the distinct benefits of the proposed method in extracting high quality certificates.
Related Projects:
Project Head Uwe Egly:
FAME: Formalisierung und Handhabung von Evolution in modellbasierter Softwareentwicklung
Project Head Uwe Egly:
Quantified Boolean Formulas
Created from the Publication Database of the Vienna University of Technology.