Author name cluster

Magdalena Widl

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

2 author rows

AAAI Conference 2015 Conference Paper

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

Valeriy Balabanov
Jie-Hong Jiang
Mikolas Janota
Magdalena Widl

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. 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 longdistance resolution (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 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.

PDF Details

SAT Conference 2014 Conference Paper

QBF Resolution Systems and Their Proof Complexities

Valeriy Balabanov
Magdalena Widl
Jie-Hong Roland Jiang

Abstract Quantified Boolean formula (QBF) evaluation has a broad range of applications in computer science and is gaining increasing attention. Recent progress has shown that for a certain family of formulas, Q -resolution, which forms the foundation of learning in modern search-based QBF solvers, is exponentially inferior in proof size to two of its extensions: Q -resolution with resolution over universal literals ( QU -resolution) and long-distance Q -resolution ( LQ -resolution). The relative proof power between LQ -resolution and QU -resolution, however, remains unknown. In this paper, we show their incomparability by exponential separations on two families of QBFs, and further propose a combination of the two resolution methods to achieve an even more powerful proof system. These results may shed light on solver development with enhanced learning mechanisms. In addition, we show how QBF Skolem/Herbrand certificate extraction can benefit from polynomial LQ -resolution proofs in contrast to their exponential Q -resolution counterparts.

Details

LPAR Conference 2013 Conference Paper

Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving

Uwe Egly
Florian Lonsing
Magdalena Widl

Abstract Strategies (and certificates) for quantified Boolean formulas (QBFs) are of high practical relevance as they facilitate the verification of results returned by QBF solvers and the generation of solutions to problems formulated as QBFs. State of the art approaches to obtain strategies require traversing a Q-resolution proof of a QBF, which for many real-life instances is too large to handle. In this work, we consider the long-distance Q-resolution (LDQ) calculus, which allows particular tautological resolvents. We show that for a family of QBFs using the LDQ-resolution allows for exponentially shorter proofs compared to Q-resolution. We further show that an approach to strategy extraction originally presented for Q-resolution proofs can also be applied to LDQ-resolution proofs. As a practical application, we consider search-based QBF solvers which are able to learn tautological clauses based on resolution and the conflict-driven clause learning method. We prove that the resolution proofs produced by these solvers correspond to proofs in the LDQ calculus and can therefore be used as input for strategy extraction algorithms. Experimental results illustrate the potential of the LDQ calculus in search-based QBF solving.

Details