CAQE: a certifying QBF solver. We present a new CEGAR-based algorithm for QBF. The algorithm builds on a decomposition of QBFs into a sequence of propositional formulas, which we call the clausal abstraction. Each of the propositional formulas contains the variables of just one quantifier level and additional variables describing the interaction with adjacent quantifier levels. This decomposition leads to a simpler notion of refinement compared to earlier approaches. We also show how to effectively construct Skolem and Herbrand functions from true, respectively false, QBFs; allowing us to certify the solver result. We implemented the algorithm in a solver called CAQE. The experimental evaluation shows that CAQE has competitive performance compared to current QBF solvers and outperforms previous certifying solvers.
Keywords for this software
References in zbMATH (referenced in 9 articles )
Showing results 1 to 9 of 9.
- Pulina, Luca; Seidl, Martina: The 2016 and 2017 QBF solvers evaluations (QBFEVAL’16 and QBFEVAL’17) (2019)
- Lonsing, Florian; Egly, Uwe: (\textsfQRAT^+): generalizing QRAT by a more powerful QBF redundancy property (2018)
- Mahajan, Meena: Lower bound techniques for QBF proof systems (2018)
- Faymonville, Peter; Finkbeiner, Bernd; Rabe, Markus N.; Tentrup, Leander: Encodings of bounded synthesis (2017)
- Peitl, Tomáš; Slivovsky, Friedrich; Szeider, Stefan: Dependency learning for QBF (2017)
- Lonsing, Florian; Egly, Uwe; Seidl, Martina: Q-resolution with generalized axioms (2016)
- Rabe, Markus N.; Seshia, Sanjit A.: Incremental determinization (2016)
- Tentrup, Leander: Non-prenex QBF solving using abstraction (2016)
- Wimmer, Karina; Wimmer, Ralf; Scholl, Christoph; Becker, Bernd: Skolem functions for DQBF (2016)