Exploiting circuit representations in QBF solving. Previous work has shown that circuit representations can be exploited in QBF solvers to obtain useful performance improvements. In this paper we examine some additional techniques for exploiting a circuit representations. We discuss the techniques of propagating a dual set of values through the circuit, conversion from simple negation normal form to a more optimized circuit representation, and adding phase memorization during search. We have implemented these techniques in a new QBF solver called CirQit2 and evaluated their impact experimentally. The solver has also displayed superior performance in the non-prenex non-CNF track of the QBFEval’10 competition.
Keywords for this software
References in zbMATH (referenced in 6 articles , 2 standard articles )
Showing results 1 to 6 of 6.
- Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2016)
- Tentrup, Leander: Non-prenex QBF solving using abstraction (2016)
- Wintersteiger, Christoph M.; Hamadi, Youssef; De Moura, Leonardo: Efficiently solving quantified bit-vector formulas (2013)
- Büning, Hans Kleine; Zhao, Xishun; Bubeck, Uwe: Transformations into normal forms for quantified circuits (2011)
- Goultiaeva, Alexandra; Bacchus, Fahiem: Exploiting circuit representations in QBF solving (2010)
- Goultiaeva, Alexandra; Iverson, Vicki; Bacchus, Fahiem: Beyond CNF: a circuit-based QBF solver (2009)