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'.