RAReQS-NN: Recursive Abstraction Refinement QBF Solver

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

[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

Description

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.

Download

rareqs-nn-beta, linux 64 bit binaries

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.

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)

Last updated: Jul 14, 2014 12:33:14 PM