bunsat
Copyright © 2014 Saarland University
Maintainer: Leander Tentrup
Introduction
This page contains the DQBF solver bunsat and PEC benchmarks used for the SAT paper Fast DQBF Refutation.
The following tools are included:
- bunsat.py — Transforms a DQBF formula to a QBF formula by bounding the paths under consideration
- dqbf_solver_cudd.py — Expansion based DQBF solver using the CUDD BDD library
- dqbf2epr.py — Transforms a DQBF formula to an equivalent formula in the effectively propositional fragment (EPR) of first-order logic
- pec_generator.py — Generates DQBF instances from given circuits by inserting black boxes and random faults
Publications
| [FTe14b] | Fast DQBF Refutation. Bernd Finkbeiner and Leander Tentrup. SAT 2014. |
License
The tools and benchmarks are licensed under the GNU General Public License version 3.
Download
Prerequisites:
- Python 2 and Python 3 (for dqbf2epr.py only)
- bool2cnf for bunsat.py
- PyCUDD for dqbf_solver_cudd.py
- PyEDA for dqbf2epr.py
Downloads:
DQBF Format
formula := universal existential matrix
universal := A (variable)* :
existential := ( E{ (variable)* } (variable)+ : )+
matrix := arbitrary boolean formulas
Example: A x1 x2: E{x1} y1 : E{x2} y2: (y1 | y2) <--> (x1 ^ x2)