Sciweavers

SAT
2010
Springer

Exploiting Circuit Representations in QBF Solving

13 years 10 months ago
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 nonprenex non-CNF track of the QBFEval’10 competition.
Alexandra Goultiaeva, Fahiem Bacchus
Added 30 Jan 2011
Updated 30 Jan 2011
Type Journal
Year 2010
Where SAT
Authors Alexandra Goultiaeva, Fahiem Bacchus
Comments (0)