Provided by: depqbf_0.1-1_amd64 bug


       depqbf - a solver for quantified boolean formulae


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


       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.


       depqbf accepts the following options:

       -h, --help
              Print usage information.

              Print version.

              Only parse and print formula.

       -v     Increase verbosity incrementally.

       NUM    Optional: time-out after NUM seconds.

       FILE   Optional: read input from FILE.


       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.


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


       depqbf was written by Florian Lonsing <>.

       This manual page was written by Thomas Krennwallner <>,

                                         August 26, 2011                                DEPQBF(1)