[HOME] |
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.
(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
The 15th International Conference on Theory and Applications of Satisfiability Testing (SAT '12) |
Last updated: Nov 20, 2018 07:20:08 PM |