[Zurück]


Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):

U. Egly, M. Widl:
"Solution extraction from long-distance resolution proofs";
Vortrag: International Workshop on Quantified Boolean Formulas, Helsinki; 09.07.2013; in: "International Workshop on Quantified Boolean Formulas 2013 Informal Workshop Report", M. Seidl, F. Lonsing (Hrg.); (2013), 10 S.



Kurzfassung englisch:
This paper is intended to advertise the use of LDQ-resolution. First, we argue that LDQ-resolution may greatly simplify the clause learning component in current QBF solvers as in this component, additional effort (in terms of Q-resolution steps) is required in order to
avoid the generation of tautological clauses over ∀ literals. This additional effort often results in an increase of refutation size. Second, we show that LDQ-resolution has the potential to produce shorter refutations. More precisely, we show an exponential speed-
up in refutation size compared to Q-resolution on formulas of a well-known family of QBFs that are known to have an exponential lower bound on their proof size. Third, we show that a state of the art strategy extraction can handle LDQ-resolution refutations. Therefore, the performance of this algorithm directly profits from exponentially shorter LDQ-resolution refutations. We finally point out open questions with respect to a certificate extraction procedure from the literature.

Schlagworte:
Quantified Boolean formulas, proof systems, certificates


Elektronische Version der Publikation:
http://publik.tuwien.ac.at/files/PubDat_223813.pdf



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.