[Back]


Talks and Poster Presentations (with Proceedings-Entry):

U. Egly, M. Widl:
"Solution extraction from long-distance resolution proofs";
Talk: International Workshop on Quantified Boolean Formulas, Helsinki; 2013-07-09; in: "International Workshop on Quantified Boolean Formulas 2013 Informal Workshop Report", M. Seidl, F. Lonsing (ed.); (2013), 10 pages.



English abstract:
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.

Keywords:
Quantified Boolean formulas, proof systems, certificates


Electronic version of the publication:
http://publik.tuwien.ac.at/files/PubDat_223813.pdf



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.