PV4 QuAbS: Quantified Abstraction Solverproduces a satisfiability result for a quantified boolean formula

Solver for quantified Booelan formulas (QBF) based on a CEGAR-based abstraction algorithm

Application domain/field

Type of tool

Satisfiability solver

Expected input

Quantified boolean formula

Format:

QCIR (quantified circuit) format.

Expected output

r SAT or r UNSAT

Comments

There is also a prototype that has been parallelized, which is referred to as PQUABS in the SAT '16 paper. They provide a conversion from QCIR to QAIGER
QBF

Links

Last commit date

24 October 2020

Related papers

Last publication date

2018

ProVerB specific

View/edit source (Markdown)



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