[Back]

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.

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.

Project Head Uwe Egly:
FAME: Formalisierung und Handhabung von Evolution in modellbasierter Softwareentwicklung

Project Head Uwe Egly:
Quantified Boolean Formulas