[HOME]

RAReQS - Recursive Abstraction Refinement QBF Solver

Description

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.

A non-prenex, non-cnf version of RAReQS can be found here.

Results
Download
COPYRIGHT NOTICE

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

References
[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: Jul 14, 2014 12:21:06 PM