xenial (1) depqbf.1.gz

NAME

       depqbf - a solver for quantified boolean formulae

SYNOPSIS

       depqbf [options ...] [NUM] [FILE]

DESCRIPTION

       depqbf  is a search-based solver for quantified boolean formulae (QBF) in prenex conjunctive normal form.
       It is based on the DPLL algorithm for QBF with conflict-driven clause and solution-driven cube  learning.
       By  analyzing  the structure of a formula, DepQBF tries to identify independent variables. In addition to
       other benefits, this often increases freedom for decision making. See also the JSAT system description of
       DepQBF 0.1 from QBFEVAL'10 for references and a brief outline of the idea.

       depqbf  reads  QBF  formulas  in  QDIMACS format. If FILE is not given, it reads its input from stdin. It
       complies with input/output standards as required by QBFEVAL'10.

OPTIONS

       depqbf accepts the following options:

       -h, --help
              Print usage information.

       --version
              Print version.

       --pretty-print
              Only parse and print formula.

       -v     Increase verbosity incrementally.

       NUM    Optional: time-out after NUM seconds.

       FILE   Optional: read input from FILE.

EXIT STATUS

       The exit status is 10 if the QBF formula given as input is satisfiable, and 20 if  it  is  unsatisfiable;
       any other exit code indicates that the formula was not solved.

SEE ALSO

       picosat(1), minisat(1), clasp(1).

AUTHOR

       depqbf was written by Florian Lonsing <florian.lonsing@jku.at>.

       This manual page was written by Thomas Krennwallner <tkren@kr.tuwien.ac.at>,

                                                 August 26, 2011                                       DEPQBF(1)