RAReQS-NN - Recursive Abstraction Refinement QBF Solver for Non-Prenex and Non-CNF inputs.


RAReQS-NN 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]. This is a Non-CNF, Non-Prenex formula. The solver assumes cleansed QCIR-G14 format (Originally, however, it was implemented with different input in mind so some conversions are needed.)

This is a Beta version, we would be happy to hear about your use cases!

The QCNF version of RAReQS can be found here.


(C) 2013 Mikolas Janota

rareqs-nn 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.

[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:33:14 PM