Academic
Publications
A Solver for QBFs in Nonprenex Form

A Solver for QBFs in Nonprenex Form,Uwe Egly,Martina Seidl,Stefan Woltran

A Solver for QBFs in Nonprenex Form   (Citations: 14)
BibTex | RIS | RefWorks Download
Various problems in 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 draw- backs and implement 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.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...A non-prenex NNF-based DPLL solver with dependency-directed (nonchronological) backtracking, but without learning, was developed by Egly, Seidl, and Woltran [4]...

    William Klieberet al. A Non-prenex, Non-clausal QBF Solver with Game-State Learning

    • ...In the first kind, procedures are based on resolution like QKN [6], are bottom-up quantifier elimination procedures like quantor [7] (for CNF QBF) or Nenofex [8] (for NNF QBF) as extension of Davis and Putnam algorithm, or are top-down quantifier elimination (or searchbased) procedures like Evaluate [9], QUBE [10] or QSOLVE [11] (all for CNF QBF) or qpro [12] (for NNF QBF) as extension of Davis, Logemann and Loveland algorithm...

    Benoit Da Motaet al. A new parallel architecture for QBF tools

    • ...The results of all possible combinations are presented in [16]; here, we show only the worst (upper picture in Fig. 18) and the best case (lower picture in Fig. 18) for all solvers...

    Uwe Eglyet al. A solver for QBFs in negation normal form

    • ...The same method can implicitly be applied in non-PCNF solvers [13]...
    • ...Thus they are also applicable to solvers using quantier scope analysis [4, 13, 18]...
    • ...Apart from non-determinism, which has already been reported in [4, 12, 13, 18], mini-scoping as well as quantier scope analysis [13, 18] is not optimal among syntactic methods for dependency computation...
    • ...Apart from non-determinism, which has already been reported in [4, 12, 13, 18], mini-scoping as well as quantier scope analysis [13, 18] is not optimal among syntactic methods for dependency computation...
    • ...applies to scope analysis like in [13, 18] because any tree-shaped prex of non-PCNF formulae can in principle be obtained by mini-scoping...

    Florian Lonsinget al. A Compact Representation for Syntactic Dependencies in QBFs

    • ...This transformation is not deterministic and it is crucial for the performance of QBF solvers requiring the input formula in this normal form (for details, see [20, 21])...

    Philippe Besnardet al. Encoding deductive argumentation in quantified Boolean formulae

Sort by: