Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs


  • Valeriy Balabanov National Taiwan University
  • Jie-Hong Jiang National Taiwan University
  • Mikolas Janota INESC-ID
  • Magdalena Widl Vienna University of Technology




Quantified Boolean Formula, Long-Distance Resolution, Model, Countermodel, Skolem Function, Herbrand Function


Many computer science problems can be naturally and compactly expressed using quantified Boolean formulas (QBFs). Evaluating thetruth 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. Modern 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 long-distanceresolution (LQ-resolution) 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 forLQ-resolution proofs. 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 from some LQ-resolution proofs that are not obtainable from Q-resolution proofs.




How to Cite

Balabanov, V., Jiang, J.-H., Janota, M., & Widl, M. (2015). Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs. Proceedings of the AAAI Conference on Artificial Intelligence, 29(1). https://doi.org/10.1609/aaai.v29i1.9750



Main Track: Search and Constraint Satisfaction