Non-prenex QBF Solving Using Abstraction
Leander Tentrup
In a recent work, we introduced an abstraction based algorithm for solving quantified Boolean formulas~(QBF) in prenex negation normal form~(PNNF) where quantifiers are only allowed in the formula’s prefix and negation appears only in front of variables. In this paper, we present a modified algorithm that lifts the restriction on prenex quantifiers. Instead of a linear quantifier prefix, the algorithm handles tree-shaped quantifier hierarchies where different branches can be solved independently. In our implementation, we exploit this property by solving independent branches in parallel. We report on an evaluation of our implementation on a recent case study regarding the synthesis of finite-state controllers from omega-regular specifications.
19th International Conference on Theory and Applications of Satisfiability Testing (SAT 2016).
Copyright by Springer. The original publication is available at http://link.springer.com.