Efficient extraction of QBF (counter) models from long-distance resolution proofs

Abstract

Many computer science problems can be naturally and compactly expressed using quantified Boolean formulas (QBFs). Evaluating the truth or falsity of a QBF is an important task, and constructing the corresponding model or countermodel can be as important and sometimes even more useful in practice. Modem search and learning based QBF solvers rely fundamentally on resolution and can be instrumented to produce resolution proofs, from which in turn Skolem-function models and Herbrand-function countermodels can be extracted. These (counter) models are the key enabler of various applications. Not until recently the superiority of longdistance resolution (LQ-resoiution) to short-distance resolution (Q-resolution) was demonstrated. While a polynomial algorithm exists for (counter)model extraction from Q-resolution proofs, it remains open whether it exists for LQ-resolution proofs. This paper settles this open problem affirmatively by constructing a lineartime extraction procedure. Experimental results show the distinct benefits of the proposed method in extracting high quality certificates from some LQ-resolution proofs that are not obtainable from Q-resolution proofs.