.\"                                      Hey, EMACS: -*- nroff -*-
.\" First parameter, NAME, should be all caps
.\" Second parameter, SECTION, should be 1-8, maybe w/ subsection
.\" other parameters are allowed: see man(7), man(1)
.TH DEPQBF 1 "August 26, 2011"
.\" Please adjust this date whenever revising the manpage.
.\"
.\" Some roff macros, for reference:
.\" .nh        disable hyphenation
.\" .hy        enable hyphenation
.\" .ad l      left justify
.\" .ad b      justify to both left and right margins
.\" .nf        disable filling
.\" .fi        enable filling
.\" .br        insert line break
.\" .sp <n>    insert n+1 empty lines
.\" for manpage-specific macros, see man(7)
.SH NAME
depqbf \- a solver for quantified boolean formulae
.SH SYNOPSIS
.B depqbf
[\fIoptions\fR ...] [\fINUM\fR] [\fIFILE\fR]
.SH DESCRIPTION
.B 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.
.\" TeX users may be more comfortable with the \fB<whatever>\fP and
.\" \fI<whatever>\fP escape sequences to invode bold face and italics,
.\" respectively.
.PP
\fBdepqbf\fP reads QBF formulas in QDIMACS format. If \fIFILE\fP is not given,
it reads its input from stdin. It complies with input/output standards
as required by QBFEVAL'10.
.SH OPTIONS
\fBdepqbf\fP accepts the following options:
.TP
.B \-h, \-\-help
Print usage information.
.TP
.B \-\-version
Print version.
.TP
.B \-\-pretty\-print
Only parse and print formula.
.TP
.B \-v
Increase verbosity incrementally.
.TP
.B NUM
Optional: time-out after NUM seconds.
.TP
.B FILE
Optional: read input from FILE.
.SH 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.
.SH SEE ALSO
.BR picosat (1),
.BR minisat (1),
.BR clasp (1).
.br
.SH AUTHOR
depqbf was written by Florian Lonsing <florian.lonsing@jku.at>.
.PP
This manual page was written by Thomas Krennwallner <tkren@kr.tuwien.ac.at>,