caqe-picosat
| Submitter: | Leander Tentrup | ||
| Description: | Devised by L. Tentrup and M. N. Rabe, is a CEGAR-based algorithm for QBF. The algorithm builds on a decomposition of QBFs into a sequence of propositional formulas called 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. It uses PICOSAT as back-end SAT solver and BLOQQER as preprocessor. Details are available in Rabe, M.N., Tentrup, L.: CAQE: A Certifying QBF Solver. In: Proceedings of the 15th Conference on Formal Methods in Computer-aided Design (FMCAD’15). | ||
| Results: | |||