NEWS Version 1.1 --> 1.2 (2011-06-30) - Fixed clause count for non-QDIMACS-compliant inputs and some minor issues. Version 1.0 --> 1.1 (2011-05-25) - Fixed a bug in cleanup code (thanks to Allen van Gelder). - Fixed a bug in heuristic choice of Q-resolution candidates. DESCRIPTION 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 (see http://fmv.jku.at/picosat/) is used for SAT-based FL. Additionally, unit clauses learnt by PicoSAT are propagated using QBF-specific QBCP rules within QxBF. Details about the implemented approaches and references may be found in our paper "Failed Literal Detection for QBF", to appear in proceedings of SAT 2011 conference. LICENSE For copying conditions, see COPYING. CONTACT For contact information (questions, bug reports, etc.), see project web page at http://fmv.jku.at/qxbf/ INSTALLATION / USAGE Create a new directory DIR. Download a recent source package of PicoSAT from http://fmv.jku.at/picosat/ copy it to DIR and unpack it. (Installation should work with 'picosat-936.tar.gz'.) In the directory of PicoSAT, call './configure -O -static' and then 'make'. Make sure that the directory of PicoSAT is named 'picosat'. Rename it if necessary. Copy the source package of QxBF to directory DIR and unpack it. The directory tree should now look like 'DIR/picosat' and 'DIR/qxbf'. Call 'make' in the directory of QxBF. Compilation process of QxBF requires to have PicoSAT compiled before in directory 'DIR/picosat/' Call 'DIR/qxbf/qxbf -h' to display usage information. QxBF will read from 'stdin' unless a QBF in QDIMACS format is given. In the default configuration (i.e. when no command line arguments are given), QxBF applies abstraction-based FL and SAT-based FL using a time limit of 40 seconds each. The preprocessed formula is written to 'stdout', everything else like progress information and statistics to 'stderr'.