Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
V. Balabanov, J. Jiang, M. Janota, M. Widl:
"Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs";
Vortrag: 2nd International Workshop on Quantified Boolean Formulas,
Wien;
13.07.2014; in: "2nd International Workshop on Quantified Boolean Formulas",
(2014),
13 S.
Kurzfassung englisch:
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.
Zugeordnete Projekte:
Projektleitung Uwe Egly:
FAME: Formalisierung und Handhabung von Evolution in modellbasierter Softwareentwicklung
Projektleitung Uwe Egly:
Quantified Boolean Formulas
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.