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

Format:

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.

Internals

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

Links

Last commit date

24 February 2021

Related papers

https://doi.org/10.1007/978-3-319-63390-9_25 (CAV '17)

Last publication date

13 July 2017

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.