• [pronounced "rah-rex"]
• Authors: Mikoláš Janota, William Klieber
• Contribution: Joao Marques-Silva, Edmund Clarke
• Contact: mikolas DOT-GOES-HERE janota AT-SIGN-GOES-HERE gmail DOT-GOES-HERE com

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.

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.

• SAT12

• rareqs-1.1, linux 64 bit binaries
• rareqs-1.1, sources

(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.

Last updated: Nov 20, 2018 07:20:08 PM