Uwe Egly

SAT Conference 2019 Conference Paper

QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties

• Florian Lonsing
• Uwe Egly

Abstract We present version 2. 0 of QRATPre +, a preprocessor for quantified Boolean formulas (QBFs) based on the \(\mathsf {QRAT} \) proof system and its generalization \(\mathsf {QRAT}^{+} \). These systems rely on strong redundancy properties of clauses and universal literals. QRATPre + is the first implementation of these redundancy properties in \(\mathsf {QRAT} \) and \(\mathsf {QRAT}^{+} \) used to simplify QBFs in preprocessing. It is written in C and features an API for easy integration in other QBF tools. We present implementation details and report on experimental results demonstrating that QRATPre + improves upon the power of state-of-the-art preprocessors and solvers.

SAT Conference 2016 Conference Paper

On Stronger Calculi for QBFs

• Uwe Egly

Abstract Quantified Boolean formulas (QBFs) generalize propositional formulas by admitting quantifications over propositional variables. QBFs can be viewed as (restricted) formulas of first-order predicate logic and easy translations of QBFs into first-order formulas exist. We analyze different translations and show that first-order resolution combined with such translations can polynomially simulate well-known deduction concepts for QBFs. Furthermore, we extend QBF calculi by the possibility to instantiate a universal variable by an existential variable of smaller level. Combining such an enhanced calculus with the propositional extension rule results in a calculus with a universal quantifier rule which essentially introduces propositional formulas for universal variables. In this way, one can mimic a very general quantifier rule known from sequent systems.

SAT Conference 2016 Conference Paper

Q-Resolution with Generalized Axioms

• Florian Lonsing
• Uwe Egly
• Martina Seidl

Abstract Q-resolution is a proof system for quantified Boolean formulas (QBFs) in prenex conjunctive normal form (PCNF) which underlies search-based QBF solvers with clause and cube learning (QCDCL). With the aim to derive and learn stronger clauses and cubes earlier in the search, we generalize the axioms of the Q-resolution calculus resulting in an exponentially more powerful proof system. The generalized axioms introduce an interface of Q-resolution to any other QBF proof system allowing for the direct combination of orthogonal solving techniques. We implemented a variant of the Q-resolution calculus with generalized axioms in the QBF solver DepQBF. As two case studies, we apply integrated SAT solving and resource-bounded QBF preprocessing during the search to heuristically detect potential axiom applications. Experiments with application benchmarks indicate a substantial performance improvement.

LPAR Conference 2015 Conference Paper

Automated Benchmarking of Incremental SAT and QBF Solvers

• Uwe Egly
• Florian Lonsing
• Johannes Oetsch

Abstract Incremental SAT and QBF solving potentially yields improvements when sequences of related formulas are solved. An incremental application is usually tailored towards some specific solver and decomposes a problem into incremental solver calls. This hinders the independent comparison of different solvers, particularly when the application program is not available. As a remedy, we present an approach to automated benchmarking of incremental SAT and QBF solvers. Given a collection of formulas in (Q)DIMACS format generated incrementally by an application program, our approach automatically translates the formulas into instructions to import and solve a formula by an incremental SAT/QBF solver. The result of the translation is a program which replays the incremental solver calls and thus allows to evaluate incremental solvers independently from the application program. We illustrate our approach by different hardware verification problems for SAT and QBF solvers.

LPAR Conference 2015 Conference Paper

Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination

• Florian Lonsing
• Fahiem Bacchus
• Armin Biere
• Uwe Egly
• Martina Seidl

Abstract Among preprocessing techniques for quantified Boolean formula (QBF) solving, quantified blocked clause elimination (QBCE) has been found to be extremely effective. We investigate the power of dynamically applying QBCE in search-based QBF solving with clause and cube learning (QCDCL). This dynamic application of QBCE is in sharp contrast to its typical use as a mere preprocessing technique. In our dynamic approach, QBCE is applied eagerly to the formula interpreted under the assignments that have been enumerated in QCDCL. The tight integration of QBCE in QCDCL results in a variant of cube learning which is exponentially stronger than the traditional method. We implemented our approach in the QBF solver DepQBF and ran experiments on instances from the QBF Gallery 2014. On application benchmarks, QCDCL with dynamic QBCE substantially outperforms traditional QCDCL. Moreover, our approach is compatible with incremental solving and can be combined with preprocessing techniques other than QBCE.

SAT Conference 2015 Conference Paper

Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API

• Florian Lonsing
• Uwe Egly

Abstract We consider the incremental computation of minimal unsatisfiable cores (MUCs) of QBFs. To this end, we equipped our incremental QBF solver DepQBF with a novel API to allow for incremental solving based on clause groups. A clause group is a set of clauses which is incrementally added to or removed from a previously solved QBF. Our implementation of the novel API is related to incremental SAT solving based on selector variables and assumptions. However, the API entirely hides selector variables and assumptions from the user, which facilitates the integration of DepQBF in other tools. We present implementation details and, for the first time, report on experiments related to the computation of MUCs of QBFs using DepQBF’s novel clause group API.

SAT Conference 2013 Conference Paper

Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation

• Florian Lonsing
• Uwe Egly
• Allen Van Gelder

Abstract Recent solvers for quantified boolean formulas (QBF) use a clause learning method based on a procedure proposed by Giunchiglia et al. (JAIR 2006), which avoids creating tautological clauses. Recently, an exponential worst case for this procedure has been shown by Van Gelder (CP 2012). That paper introduced QBF Pseudo Unit Propagation (QPUP) for non-tautological clause learning in a limited setting and showed that its worst case is theoretically polynomial, although it might be impractical in a high-performance QBF solver, due to excessive time and space consumption. No implementation was reported. We describe an enhanced version of QPUP learning that is practical to incorporate into high-performance QBF solvers, being compatible with pure-literal rules and dependency schemes. It can be used for proving in a concise format that a QBF formula is either unsatisfiable or satisfiable (working on both proofs in tandem). A lazy version of QPUP permits non-tautological clauses to be learned without actually carrying out resolutions, but this version is unable to produce proofs. Experimental results show that QPUP is somewhat faster than the previous non-tautological clause learning procedure on benchmarks from QBFEVAL-12-SR.

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.

SAT Conference 2012 Conference Paper

On Sequent Systems and Resolution for QBFs

• Uwe Egly

Abstract Quantified Boolean formulas generalize propositional formulas by admitting quantifications over propositional variables. We compare proof systems with different quantifier handling paradigms for quantified Boolean formulas (QBFs) with respect to their ability to allow succinct proofs. We analyze cut-free sequent systems extended by different quantifier rules and show that some rules are better than some others. Q-resolution is an elegant extension of propositional resolution to QBFs and is applicable to formulas in prenex conjunctive normal form. In Q-resolution, there is no explicit handling of quantifiers by specific rules. Instead the forall reduction rule which operates on single clauses inspects the global quantifier prefix. We show that there are classes of formulas for which there are short cut-free tree proofs in a sequent system, but any Q-resolution refutation of the negation of the formula is exponential.

SAT Conference 2009 Conference Paper

(1, 2)-QSAT: A Good Candidate for Understanding Phase Transitions Mechanisms

• Nadia Creignou
• Hervé Daudé
• Uwe Egly
• Raphaël Rossignol

Abstract We explore random Boolean quantified CNF formulas of the form ∀ X ∃ Y ϕ ( X, Y ), where X has \(m=\lfloor \alpha \log n\rfloor\) variables ( α > 0), Y has n variables and each clause in ϕ has one literal from X and two from Y. These (1, 2)-QCNF -formulas, which can be seen as quantified extended 2-CNF formulas, were introduced in SAT’08. It was proved that the threshold phenomenon associated to the satisfiability of such random formulas, (1, 2)-QSAT, is controlled by the ratio c between the number of clauses and the number n of existential variables. In this paper, we prove that the threshold is sharp. For any value of α, we give the exact location of the associated critical ratio, a ( α ). At this ratio, our study highlights the sudden emergence of unsatisfiable formulas with a very specific shape. From the experimental point of view (1, 2)-QSAT is challenging. Indeed, while for small values of m the critical ratio can be observed experimentally, it is not anymore the case for bigger values of m. For small values of m we give precise numerical estimates of the probability of satisfiability for critical (1, 2)-QCNF -formulas. These experiments give evidence that the asymptotical regime is difficult to reach and provide some indication on the behavior of random instances. Moreover, experiments show that the computational effort, which is increasing with m, is maximized within the phase transition.

SAT Conference 2008 Conference Paper

New Results on the Phase Transition for Random Quantified Boolean Formulas

• Nadia Creignou
• Hervé Daudé
• Uwe Egly
• Raphaël Rossignol

Abstract The QSAT problem is the quantified version of the satisfiability problem SAT. We study the phase transition associated with random QSAT instances. We focus on a certain subclass of closed quantified Boolean formulas that can be seen as quantified extended 2-CNF formulas. The evaluation problem for this class is coNP -complete. We carry out an advanced practical and theoretical study, which illuminates the influence of the different parameters used to define random quantified instances.

ECAI Conference 2006 Conference Paper

A Solver for QBFs in Nonprenex Form

• Uwe Egly
• Martina Seidl
• Stefan Woltran

Various problems in artificial intelligence (AI) can be solved by translating them into a quantified boolean formula (QBF) and evaluating the resulting encoding. In this approach, a QBF solver is used as a black box in a rapid implementation of a more general reasoning system. Most of the current solvers for QBFs require formulas in prenex conjunctive normal form as input, which makes a further translation necessary, since the encodings are usually not in a specific normal form. This additional step increases the number of variables in the formula or disrupts the formula's structure. Moreover, the most important part of this transformation, prenexing, is not deterministic. In this paper, we focus on an alternative way to process QBFs without these drawbacks and describe a solver, qpro, which is able to handle arbitrary formulas. To this end, we extend algorithms for QBFs to the non-normal form case and compare qpro with the leading normal-form provers on problems from the area of AI.

SAT Conference 2003 Conference Paper

Comparing Different Prenexing Strategies for Quantified Boolean Formulas

• Uwe Egly
• Martina Seidl
• Hans Tompits
• Stefan Woltran
• Michael Zolda

Abstract The majority of the currently available solvers for quantified Boolean formulas (QBFs) process input formulas only in prenex conjunctive normal form. However, the natural representation of practicably relevant problems in terms of QBFs usually results in formulas which are not in a specific normal form. Hence, in order to evaluate such QBFs with available solvers, suitable normal-form translations are required. In this paper, we report experimental results comparing different prenexing strategies on a class of structured benchmark problems. The problems under consideration encode the evaluation of nested counterfactuals over a propositional knowledge base, and span the entire polynomial hierarchy. The results show that different prenexing strategies influence the evaluation time in different ways across different solvers. In particular, some solvers are robust to the chosen strategies while others are not.

AAAI Conference 2000 Conference Paper

Solving Advanced Reasoning Tasks Using Quantified Boolean Formulas

• Uwe Egly
• Hans Tompits

We consider the compilation of different reasoning tasks into the evaluation problem of quantified boolean formulas (QBFs) as an approach to develop prototype reasoning systems useful for, e. g. , experimental purposes. Such a method is a natural generalization of a similar technique applied to NP-problems and has been recently proposed by other researchers. More specifically, we present translations of several well-known reasoning tasks from the area of nonmonotonic reasoning into QBFs, and compare their implementation in the prototype system QUIP with established NMRprovers. The results show reasonable performance, and document that the QBF approach is an attractive tool for rapid prototyping of experimental knowledge-representation systems.

CSL Conference 1999 Conference Paper

Quantifers and the System KE: Some Surprising Results

• Uwe Egly

Abstract In this paper, we consider the free-variable variant of the calculus KE and investigate the effect of different preprocessing activities to the proof length of variants of KE. In this context, skolemization is identified to be harmful as compared to the δ -rule. This does not only have consequences for proof length in KE, but also for the “efficiency” of some structural translations. Additionally, we investigate the effect of quantifier-shifting and quantifier-distributing rules, respectively. In all these comparisons, we identify classes of formulae for which a non-elementary difference in proof length occur.

TCS Journal 1998 Journal Article

An answer to an open problem of Urquhart

• Uwe Egly

LPAR Conference 1994 Conference Paper

On the Value of Antiprenexing

• Uwe Egly

Abstract In this paper, we examine the effect of antiprenexing on the proof length if resolution deduction concepts are applied. Roughly speaking, our version of antiprenexing moves ∀-quantifiers downward in the formula tree whereas ∃-quantifiers are moved upward. We show that two different Skolemization techniques result in two clause sets with rather different resolution refutations. The lower bounds on the length of both refutations differ exponentially. Furthermore, we demonstrate that both techniques can be improved if antiprenexing is applied before Skolemization. Finally, we examine the influence of antiprenexing if extended resolution deduction concepts are used.

LPAR Conference 1993 Conference Paper

A First Order Resolution Calculus with Symmetries

• Uwe Egly

Abstract In this paper, we present a resolution calculus extended by the notion of symmetries. A new deduction rule named symmetry extension is introduced. Combining resolution deduction and symmetry extension yields a new extended resolution deduction concept called SR-deduction (resolution deduction with symmetries). By extending the given clause set by a clause derived by symmetry extension, exponentially shorter refutations may be obtained than by applying resolution to the given clause set.

ECAI Conference 1992 Conference Paper

A Simple Proof for the Pigeonhole Formulae

• Uwe Egly

LPAR Conference 1992 Conference Paper

Shortening Proofs by Quantifier Introduction

• Uwe Egly

Abstract In this paper, we describe an extended resolution calculus based on the introduction of new existential quantifiers. The additional rule is called Q-extension (quantifier extension). We show how polynomial refutations can be obtained by applying Q-extension, whereas usual resolution refutations are exponential. We compare our new deduction concept with FR-deduction