Solution extraction from long-distance resolution proofs

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.