Circuit-Based Search Space Pruning in QBF

摘要

This paper describes the algorithm implemented in the QBF solver CQESTO, which has placed second in the non-CNF track of the last year's QBF competition. The algorithm is inspired by the CNF-based solver QESTO. Just as QESTO, CQESTO invokes a SAT solver in a black-box fashion. However, it directly operates on the circuit representation of the formula. The paper analyzes the individual operations that the solver performs.