PV4 CAQE: Clausal Abstraction for Quantifier Eliminationproduces a satisfiability result for a quantified boolean formula

Solver for quantified boolean formulas (QBF)

Application domain/field

Type of tool

QBF (quantified boolean formulas) solver

Expected input

quantified Boolean formula (QBF) in prenex conjunctive normal (prenex CNF) form


QDIMACS file format

Expected output

Result code 10 for satisfiable and 20 for unsatisfiable instances. It can also output in the QDIMACS format which has partial assignments to variables.


Uses PicoSAT, MiniSat, CryptoMiniSat and Lingeling as underlying SAT solver.


Related papers

On Expansion and Resolution in CEGAR Based QBF Solving (CAV '17)

Last publication date

13 July 2017

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.