Academic
Publications
Beyond CNF: A Circuit-Based QBF Solver

Beyond CNF: A Circuit-Based QBF Solver,10.1007/978-3-642-02777-2_38,Alexandra Goultiaeva,Vicki Iverson,Fahiem Bacchus

Beyond CNF: A Circuit-Based QBF Solver   (Citations: 7)
BibTex | RIS | RefWorks Download
State-of-the-art solvers for Quantified Boolean Formulas (QBF) have employed many techniques from the field of Boolean Satisfiability (SAT) including the use of Conjunctive Normal Form (CNF) in representing the QBF formula. Although CNF has worked well for SAT solvers, recent work has pointed out some inherent problems with using CNF in QBF solvers. In this paper, we describe a QBF solver, called CirQit (Cir-Q-it) that utilizes a circuit representation rather than CNF. The solver can exploit its circuit representation to avoid many of the problems of CNF. For example, we show how this approach generalizes some previously proposed techniques for overcoming the disadvantages of CNF for QBF solvers. We also show how important techniques like clause and cube learning can be made to work with a circuit representation. Finally, we empirically compare the resulting solver against other state-of-the-art QBF solvers, demonstrating that our approach can often outperform these solvers.
Conference: Theory and Applications of Satisfiability Testing , pp. 412-426, 2009
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.
    • ...It has thus been proposed to use non-prenex non-clausal form [11], [15]...

    Christoph M. Wintersteigeret al. Efficiently solving quantified bit-vector formulas

    • ...in [8,16]. The latter corresponds to directly considering the parse tree of a formula and can be integrated in non-PCNF solvers such as [9,18,28]...

    Florian Lonsinget al. Integrating Dependency Schemes in Search-Based QBF Solvers

    • ...For example, in [2] a QBF solver utilizing a circuit representation was presented and shown to have some advantages over CNF based solvers...
    • ...We have implemented all of these techniques as an extension of the CirQit solver [2], and we present empirical evidence supporting their usefulness...
    • ...In circuit-based solvers, e.g., the CirQit solver of [2], φ is represented as a logical circuit consisting of AND, OR and NOT gates along with lines running from gate outputs to the inputs of other gates...
    • ...As shown in [2] clausal reasons for each forced line can be extracted from the circuit, and clause learning can be performed when conflicts are detected...
    • ...Table 1 shows the comparison between CirQit2.1, CirQit2 [3], CirQit [2] and some state-of-the-art CNF-based QBF solvers: quantor (version 3.0, with the recommended picosat back end) [6], Qube (version 6.5) [7], nenofex [8] and depqbf [9]—the latter two are the versions submitted to the main track of QBFEVAL’10...

    Alexandra Goultiaevaet al. Exploiting Circuit Representations in QBF Solving

    • ...In particular, circuit observability don’t-cares can be used to improve the performance of QBF solvers [11], [12] just as they did for SAT [13], [14]...
    • ...More recently, QBF solvers that handle problems directly in a circuit-based format have shown promising results using various solving methods [12], [17], [18]...
    • ...They are originally given in the QBF1.0 format, and are converted in negligible time into our specified format using the converter of [12]...
    • ...Since none of the +sim runs terminate, our results were validated using the circuit-based QBF solver CirQit [12]...

    Hratch Mangassarianet al. Leveraging dominators for preprocessing QBF

    • ...Efficient QBF solvers would be of great benefit in applications such as model checking and verification, and multi-agent planning [GIB09], however the effectiveness of QBF solvers lags far behind that of SAT solvers...
    • ...In this context even more so than for SAT, techniques for solving the problem directly on formulae would be useful [GIB09], [Zha06]...

    Rahul Santhanam. Fighting Perebor: New and Improved Algorithms for Formula and QBF Sati...

Sort by: