[  download | overview | publications | license ]

Download

QxBF requires PicoSAT. Please see the README file for installation instructions and release notes.

• Source code: QxBF 1.2.
• Old releases: QxBF 1.1, QxBF 1.0.

Overview

QxBF is a preprocessor for QBFs in QDIMACS format based on failed literal detection (FL). The basic idea of FL is to assign a variable as assumption. If boolean constraint propagation (BCP) yields an empty clause then the negated assumption is necessary for satisfiability. Whereas FL is common in SAT, it cannot easily be applied to QBF due to universal quantification.

QxBF features failed literal detection for QBF based on three approaches: SAT-based FL, abstraction-based FL, and QBCP-guided Q-resolution where QBCP is the QBF-specific variant of BCP including unit propagation, pure literal rule and universal reduction rule. The tool operates in rounds with three phases.

First, QBCP with the full set of QBF-specific rules is carried out on the original formula, including any unit clauses learnt in earlier rounds. The second phase consists of either abstraction-based FL or QBCP-guided Q-resolution. Finally, SAT-based FL is applied in the third phase. Rounds are run in cyclic fashion until completion unless a time limit is reached. The incremental SAT solver PicoSAT is used for SAT-based FL. Additionally, unit clauses learnt by PicoSAT are propagated using QBF-specific QBCP rules within QxBF.

For bug reports etc., please contact Florian Lonsing.

Publications

Paper and talk at SAT 2011 conference.

License

QxBF was developed by Florian Lonsing, Aina Niemetz and Mathias Preiner. It is released under GNU GPLv3. See also file COPYING that is part of the distribution.