---
name: "depqbf"
section: "1"
platform: "linux"
package: "depqbf"
version: "5.01-3"
release: "Debian 13 (Trixie)"
platforms: ["linux"]
url: "https://new.carta.tech/depqbf"
---

# depqbf(1)

a solver for quantified boolean formulae

## 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)](/picosat/1.md), [**minisat**(1)](/minisat/1.md), [**clasp**(1)](/clasp/1.md).\

## AUTHOR

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

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