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.

Suggestions and Remarks

Rather than RAReQS, I suggest using the non-cnf solvers: QFUN or CQESTO.

If you still use CNF, consider using a preprocessor, such as bloqqer.


(C) 2012 Mikolas Janota

rareqs is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version.

rareqs is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

You should have received a copy of the GNU General Public License along with rareqs. If not, see GNU Licence.

[1] Solving QBF with Counterexample Guided Refinement
Mikoláš Janota, William Klieber , Joao Marques-Silva, and Edmund M. Clarke
The 15th International Conference on Theory and Applications of Satisfiability Testing (SAT '12)

Valid XHTML 1.0 Strict VI Improved Last updated: Nov 20, 2018 07:20:08 PM