RAReQS
swMATH ID: | 46008 |
Software Authors: | Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund |
Description: | RAReQS - Recursive Abstraction Refinement QBF Solver. RAReQS is a solver for Quantified Boolean Formulas (QBFs). The solver tackles the given formula recursively using counterexample abstraction refinement (CEGAR). More details can be found in our SAT 2012 paper [1]. While the RAReQS algorithm [1] is applicable to any QBF in the prenex form, the current implementation supports only the QDIMACS format. The CEGAR technique has also been incorporated, to a limited extent, into the DPLL-based solver GhostQ. |
Homepage: | http://sat.inesc-id.pt/~mikolas/sw/areqs/ |
Related Software: | DepQBF; Bloqqer; MiniSat; CAQE; Quaffle; QESTO; sQueezeBF; Nenofex; semprop; QUBOS; HQSpre; Quantor; Mjollnir; QUBE; QBFLIB; PicoSAT; QuBE++; Lingeling; z3; sKizzo |
Cited in: | 46 Documents |
Standard Articles
1 Publication describing the Software, including 1 Publication in zbMATH | Year |
---|---|
Solving QBF with counterexample guided refinement. Zbl 1351.68254 Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund |
2016
|
all
top 5
Cited by 85 Authors
all
top 5
Cited in 11 Serials
Cited in 4 Fields
41 | Computer science (68-XX) |
17 | Mathematical logic and foundations (03-XX) |
1 | Operations research, mathematical programming (90-XX) |
1 | Systems theory; control (93-XX) |