Quantified Boolean Formulas and DepQBF
4. DepQBF in Practice

Uwe Egly

Florian Lonsing

Knowledge-Based Systems Group
Institute of Information Systems
Vienna University of Technology

This work is supported by the Austrian Science Fund (FWF) under grant S11409-N23.

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice1 / 22

Overview

DepQBF: search-based, QCDCL solver.
First release in February 2010, under active development.
Approx. 20,000 lines of C code.
Open source under GPL: http://lonsing.github.io/depqbf/“DepQBF”: optional dependency analysis to relax the quantifier ordering.
Design decision: allow for use as a library.
No pre/inprocessing (not yet officially released).
Trace generation for certificate generation.
Based on PCNF, QDIMACS input format.
Incremental solving: beneficial when solving sequences of closely related PCNFs.
API to manipulate the input PCNF, configure the solver.
New version 4.0 released in February 2015.

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice2 / 22

Overview

DepQBF: search-based, QCDCL solver.
First release in February 2010, under active development.
Approx. 20,000 lines of C code.
Open source under GPL: http://lonsing.github.io/depqbf/“DepQBF”: optional dependency analysis to relax the quantifier ordering.
Design decision: allow for use as a library.
No pre/inprocessing (not yet officially released).
Trace generation for certificate generation.
Based on PCNF, QDIMACS input format.
Incremental solving: beneficial when solving sequences of closely related PCNFs.
API to manipulate the input PCNF, configure the solver.
New version 4.0 released in February 2015.

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice2 / 22

Input Format
QDIMACS:
Extension of DIMACS format used in SAT solving.
Easy to parse.
Literals of variables encoded as signed integers.
One quantifier block per line (“a” labels ∀, “e” labels ∃), terminated by zero.
One clause per line, terminated by zero.

Example∃x1 , x3 , x4 ∀y5 ∃x2 .(¬x1 ∨x2 )∧(x3 ∨y5 ∨¬x2 )∧(x4 ∨¬y5 ∨¬x2 )∧(¬x3 ∨¬x4 )Encode literals of variables xi , yi as signed integers i.

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practicep cnf 5 4
e 1 3 4 0
a 5 0
e 2 0
-1 2 03 5 -2 0
4 -5 -2 0-3 -4 03 / 22

Using DepQBF in Your Application

Encode your problem in QDIMACS format: support for other formats?
DepQBF is a standalone QBF solver and. . .
. . . provides a library with a API in C: add a formula, solve, . . .
Library use is more convenient: incremental calls.

Compile DepQBF, which produces the library libqdpll.a.
Include the header file qdpll.h in your source code.
Compile and link against the solver library: gcc your_code.c -L. -lqdpll
Call the solver API from your application.

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice4 / 22

Using DepQBF in Your Application

Encode your problem in QDIMACS format: support for other formats?
DepQBF is a standalone QBF solver and. . .
. . . provides a library with a API in C: add a formula, solve, . . .
Library use is more convenient: incremental calls.

Compile DepQBF, which produces the library libqdpll.a.
Include the header file qdpll.h in your source code.
Compile and link against the solver library: gcc your_code.c -L. -lqdpll
Call the solver API from your application.

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice4 / 22

API: Solver Object Generation/* Create and initialize solver instance. */QDPLL * qdpll_create (void);/* Delete solver instance and release all memory. */void qdpll_delete (QDPLL * qdpll);/* Ensure variable table size to be at least ’num’. */void qdpll_adjust_vars (QDPLL * qdpll, VarID num);

No static data: allows to generate multiple solver objects.
DepQBF uses variable indices as given by the QDIMACS file to index a table ofvariable objects: keep indices compact in the encoding.

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

5 / 22

API: Solver Configuration/* Configure solver instance via configuration string.
Returns null pointer on success and error string otherwise. */char * qdpll_configure (QDPLL * qdpll, char * configure_str);

Possible configuration strings:
Call ./depqbf -h for a partial listing of options.
--no-cdcl: disable clause learning and backtrack chronologically from conflicts.
--no-sdcl: disable cube learning backtrack chronologically from solutions.
--no-pure-literals: disable pure literal detection.
Various learning variants: long-distance resolution, lazy learning.
Many more: heuristics,. . .

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

6 / 22

API: Manipulating the Input FormulaPrefix Manipulation:
Add quantifier blocks of any type at any prefix position.
Add new variables to quantifier blocks.
No explicit deletion of blocks/variables: garbage collection.
CNF Manipulation:
Add/delete clauses.
No modifications of present clauses: must delete old and add new clause.
Stack-Based Clause Additions/Deletions:
Push new clauses onto the clause stack.
Pop most recently added clauses from the stack.
Group-Based Clause Additions/Deletions:
Declare groups (sets) of clauses.
Add clauses to a group, remove entire groups.

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

7 / 22

API: Manipulating the Input FormulaPrefix Manipulation:
Add quantifier blocks of any type at any prefix position.
Add new variables to quantifier blocks.
No explicit deletion of blocks/variables: garbage collection.
CNF Manipulation:
Add/delete clauses.
No modifications of present clauses: must delete old and add new clause.
Stack-Based Clause Additions/Deletions:
Push new clauses onto the clause stack.
Pop most recently added clauses from the stack.
Group-Based Clause Additions/Deletions:
Declare groups (sets) of clauses.
Add clauses to a group, remove entire groups.

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

7 / 22

API: Manipulating the Input FormulaPrefix Manipulation:
Add quantifier blocks of any type at any prefix position.
Add new variables to quantifier blocks.
No explicit deletion of blocks/variables: garbage collection.
CNF Manipulation:
Add/delete clauses.
No modifications of present clauses: must delete old and add new clause.
Stack-Based Clause Additions/Deletions:
Push new clauses onto the clause stack.
Pop most recently added clauses from the stack.
Group-Based Clause Additions/Deletions:
Declare groups (sets) of clauses.
Add clauses to a group, remove entire groups.

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

7 / 22

API: Manipulating the Input FormulaPrefix Manipulation:
Add quantifier blocks of any type at any prefix position.
Add new variables to quantifier blocks.
No explicit deletion of blocks/variables: garbage collection.
CNF Manipulation:
Add/delete clauses.
No modifications of present clauses: must delete old and add new clause.
Stack-Based Clause Additions/Deletions:
Push new clauses onto the clause stack.
Pop most recently added clauses from the stack.
Group-Based Clause Additions/Deletions:
Declare groups (sets) of clauses.
Add clauses to a group, remove entire groups.

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

7 / 22

API: Prefix Manipulation (1/3)
enum QDPLLQuantifierType:QDPLL_QTYPE_EXISTS = -1
QDPLL_QTYPE_UNDEF = 0
QDPLL_QTYPE_FORALL = 1

typedef unsigned int Nesting;/* Add new quantifier block with type ’qtype’ at right end of prefix. */Nesting qdpll_new_scope (QDPLL * qdpll, QDPLLQuantifierType qtype);/* Add new quantifier block with type ’qtype’ at level ’nesting’. */Nesting qdpll_new_scope_at_nesting (QDPLL * qdpll,
QDPLLQuantifierType qtype,
Nesting nesting);

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

8 / 22

API: Prefix Manipulation (2/3)

typedef unsigned int VarID;/* Add new variable ’id’ to the block at level ’nesting’.
Fails if a variable with ’id’ already exists. */void qdpll_add_var_to_scope (QDPLL * qdpll, VarID id, Nesting nesting);

typedef int LitID;/* Add new variable ’id’ to the current quantifier block
opened by a previous call of ’qdpll_new_scope’ or’qdpll_new_scope_at_nesting’.
Adding ’0’ closes the current block.
Fails if a variable with ’id’ already exists. */void qdpll_add (QDPLL * qdpll, LitID id);

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

9 / 22

API: Prefix Manipulation (3/3)/* Returns the nesting level of the current rightmost block. */Nesting qdpll_get_max_scope_nesting (QDPLL * qdpll);/* Return largest declared variable ID. */VarID qdpll_get_max_declared_var_id (QDPLL * qdpll);/* Returns non-zero iff. variable ’id’ has been added to the formula. */int qdpll_is_var_declared (QDPLL * qdpll, VarID id);/* Return nesting of block which contains variable ’id’. */Nesting qdpll_get_nesting_of_var (QDPLL * qdpll, VarID id);/* Return the type of the block at level ’nesting’.*/
QDPLLQuantifierType qdpll_get_scope_type (QDPLL *qdpll, Nesting nesting);

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

10 / 22

API: Basic CNF Manipulation/* Add a literal ’id’ to the current open clause.
Adding ’0’ closes the clause. */void qdpll_add (QDPLL * qdpll, LitID id);/* Pretty-print PCNF to ’out’ using QDIMACS format. */void qdpll_print (QDPLL * qdpll, FILE * out);

Note: qdpll_add is used to add variables to blocks and literals to clauses.
Tautological input clauses are discarded.
Superfluous literals (double occurrences) in clauses are discarded.
Literals in input clauses are sorted by prefix order and universal-reduced.
No free variables: if id in a clause is a literal of new variable, then that variable isput into a default existential quantifier block ∃B0 at the left end of the prefix:∃B0 Q1 B1 . . . Qn Bn . φ.
In practice: first add the prefix, then the clauses.

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

11 / 22

API: Basic CNF Manipulation/* Add a literal ’id’ to the current open clause.
Adding ’0’ closes the clause. */void qdpll_add (QDPLL * qdpll, LitID id);/* Pretty-print PCNF to ’out’ using QDIMACS format. */void qdpll_print (QDPLL * qdpll, FILE * out);

Note: qdpll_add is used to add variables to blocks and literals to clauses.
Tautological input clauses are discarded.
Superfluous literals (double occurrences) in clauses are discarded.
Literals in input clauses are sorted by prefix order and universal-reduced.
No free variables: if id in a clause is a literal of new variable, then that variable isput into a default existential quantifier block ∃B0 at the left end of the prefix:∃B0 Q1 B1 . . . Qn Bn . φ.
In practice: first add the prefix, then the clauses.

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

11 / 22

API: Stack-Based CNF Manipulation (1/2)/* Open a new top-most frame on the clause stack.
Clauses added by ’qdpll_add’ are added to the top-most frame. */unsigned int qdpll_push (QDPLL * qdpll);/* Pop the top-most frame from the clause stack.
The clauses in that frame are considered deleted from the formula. */unsigned int qdpll_pop (QDPLL * qdpll);/* Enforce garbage collection of popped off clauses. */void qdpll_gc (QDPLL * qdpll);

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

12 / 22

API: Stack-Based CNF Manipulation (2/2)

Must configure by --dep-man=simple (use given linear quantifier ordering). . .
. . . and by --incremental-use.
Useful if a sequence of closely related PCNFs is solved.
Example: encoding a transition relation for i steps, i + 1 steps,. . .
No need to parse all the PCNFs from scratch, but only the new clauses.
More important: learned clauses and cubes are re-used (if possible) when solving
other PCNFs in the sequence.
Incorrect learned clauses and cubes are automatically discarded.
Pushing is optional: without any push before, clauses are added to a default frameand cannot be removed.

In Practice:
Push and add clauses which are shared between the PCNFs first.
Push clauses which have to be removed last, so that they can be deleted by a pop.

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

13 / 22

API: Stack-Based CNF Manipulation (2/2)

Must configure by --dep-man=simple (use given linear quantifier ordering). . .
. . . and by --incremental-use.
Useful if a sequence of closely related PCNFs is solved.
Example: encoding a transition relation for i steps, i + 1 steps,. . .
No need to parse all the PCNFs from scratch, but only the new clauses.
More important: learned clauses and cubes are re-used (if possible) when solving
other PCNFs in the sequence.
Incorrect learned clauses and cubes are automatically discarded.
Pushing is optional: without any push before, clauses are added to a default frameand cannot be removed.

In Practice:
Push and add clauses which are shared between the PCNFs first.
Push clauses which have to be removed last, so that they can be deleted by a pop.

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

13 / 22

API: Group-Based CNF Manipulation (1/3)/* Declare a new clause group and return its handle. */ClauseGroupID qdpll_new_clause_group (QDPLL *qdpll);/* Delete the clause group ’cg’. Its handle ’cg’ becomes invalid. */void qdpll_delete_clause_group (QDPLL *qdpll, ClauseGroupID cg);/* Returns non-zero iff. a clause group with handle ’cg’ exists. */int qdpll_exists_clause_group (QDPLL *qdpll, ClauseGroupID cg);/* Open the clause group ’cg’. Clause can be added to open groups only.
Only one group can be open at a time. */void qdpll_open_clause_group (QDPLL *qdpll, ClauseGroupID cg);/* Closes the open clause group ’cg’. */void qdpll_close_clause_group (QDPLL *qdpll, ClauseGroupID cg);/* Returns handle of currently open clause group or zero if there is
no open group. */ClauseGroupID qdpll_get_open_clause_group (QDPLL *qdpll);
U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

14 / 22

API: Group-Based CNF Manipulation (2/3)/* Temporarily disable (remove) clauses in clause group ’cg’. */void qdpll_deactivate_clause_group (QDPLL *qdpll, ClauseGroupID cg);/* Enable (add) clauses in clause group ’cg’ again. By default, newclause groups are activated after creation. */void qdpll_activate_clause_group (QDPLL *qdpll, ClauseGroupID cg);/* If the formula is unsatisfiable (qdpll_sat() == QDPLL_RESULT_UNSAT):
returns zero-terminated list of clause groups containing clauses
which were actually used by the solver (unsatisfiable core). */ClauseGroupID * qdpll_get_relevant_clause_groups (QDPLL * qdpll);/* Enforce garbage collection of deleted groups. */void qdpll_gc (QDPLL * qdpll);

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

15 / 22

API: Group-Based CNF Manipulation (3/3)

Must configure by --dep-man=simple (use given linear quantifier ordering). . .
. . . and by --incremental-use.
More flexible than stack-based API (push/pop).
Calls of stack/group-based API functions cannot be mixed.
Allows deletion of arbitrary clauses instead of only most recently added ones.

In Practice:In general, clause groups result in increased overhead compared to push/pop API.
Use push/pop whenever appropriate.

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

16 / 22

API: Group-Based CNF Manipulation (3/3)

Must configure by --dep-man=simple (use given linear quantifier ordering). . .
. . . and by --incremental-use.
More flexible than stack-based API (push/pop).
Calls of stack/group-based API functions cannot be mixed.
Allows deletion of arbitrary clauses instead of only most recently added ones.

In Practice:In general, clause groups result in increased overhead compared to push/pop API.
Use push/pop whenever appropriate.

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

16 / 22

API: Deletion of Clauses, Variables, and Quantifier Blocks
Clauses:
No explicit deletion through API.
A clause is considered deleted after its frame has been popped from the stack.
A clause is considered deleted after its group has been deleted.
Garbage collection triggered heuristically, or enforced by calling qdpll_gc.
Variables:
No explicit deletion through API.
A variable x is deleted by qdpll_gc if all the clauses where x occurs have been
deleted before.
The IDs of deleted variables can be re-used: check with qdpll_is_var_declared.
Quantifier Blocks:
No explicit deletion through API.
A quantifier block is deleted by qdpll_gc if all of its variables have been deleted
before.
U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

17 / 22

API: Deletion of Clauses, Variables, and Quantifier Blocks
Clauses:
No explicit deletion through API.
A clause is considered deleted after its frame has been popped from the stack.
A clause is considered deleted after its group has been deleted.
Garbage collection triggered heuristically, or enforced by calling qdpll_gc.
Variables:
No explicit deletion through API.
A variable x is deleted by qdpll_gc if all the clauses where x occurs have been
deleted before.
The IDs of deleted variables can be re-used: check with qdpll_is_var_declared.
Quantifier Blocks:
No explicit deletion through API.
A quantifier block is deleted by qdpll_gc if all of its variables have been deleted
before.
U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

17 / 22

API: Deletion of Clauses, Variables, and Quantifier Blocks
Clauses:
No explicit deletion through API.
A clause is considered deleted after its frame has been popped from the stack.
A clause is considered deleted after its group has been deleted.
Garbage collection triggered heuristically, or enforced by calling qdpll_gc.
Variables:
No explicit deletion through API.
A variable x is deleted by qdpll_gc if all the clauses where x occurs have been
deleted before.
The IDs of deleted variables can be re-used: check with qdpll_is_var_declared.
Quantifier Blocks:
No explicit deletion through API.
A quantifier block is deleted by qdpll_gc if all of its variables have been deleted
before.
U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

17 / 22

API: Solving (1/2)
enum QDPLLResult:
QDPLL_RESULT_UNKNOWN = 0
QDPLL_RESULT_SAT = 10
QDPLL_RESULT_UNSAT = 20/* Solve the given PCNF. */QDPLLResult qdpll_sat (QDPLL * qdpll);/* Reset internal solver state, but keep the PCNF and learned constraints. *void qdpll_reset (QDPLL * qdpll);/* Discard all learned constraints. */void qdpll_reset_learned_constraints (QDPLL * qdpll);
QDPLL_RESULT_UNKNOWN returned only if formula not solved under imposed limits.
qdpll_reset deletes the variable assignments.
Incremental calls after reset: may add/delete clauses.
For convenience: calling qdpll_reset_learned_constraints is never required forthe correctness of incremental solving. The solver keeps track of learned constraints.
U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

18 / 22

API: Solving (2/2)
typedef int QDPLLAssignment;#define QDPLL_ASSIGNMENT_FALSE -1#define QDPLL_ASSIGNMENT_UNDEF 0#define QDPLL_ASSIGNMENT_TRUE 1/* Get current assignment of variable. */QDPLLAssignment qdpll_get_value (QDPLL * qdpll, VarID id);/* Like ’qdpll_get_value’ but print to standard output. */void qdpll_print_qdimacs_output (QDPLL * qdpll);
Call after qdpll_sat but before qdpll_reset.
From the command line: --qdo
Get partial certificates of (un)satisfiability as assignments to leftmost variables. . .
. . . if the PCNF ∃B1 . . . ., φ is satisfiable.
. . . if the PCNF ∀B1 . . . ., φ is unsatisfiable.
In practice: useful for encodings of problems from the second level of the polynomial
hierarchy with prefix ∀∃ and ∃∀.
U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

19 / 22

API: Solving Under Assumptions/* Assign a variable permanently in the next run (assumption).
If ’id < 0’ then assign variable ’id’ to false.
If ’id > 0’ then assign variable ’id’ to true. */void qdpll_assume (QDPLL * qdpll, LitID id);/* Returns an array of safe arguments to ’qdpll_assume’. */LitID * qdpll_get_assumption_candidates (QDPLL * qdpll);/* Returns the subset of assumptions used by the solver
to determine the result. */LitID * qdpll_get_relevant_assumptions (QDPLL * qdpll);Can be combined with push and pop.
Safe arguments to qdpll_assume are variables from the leftmost block (recursively).
Assignments added by qdpll_assume are persistent in the next call of qdpll_sat.
qdpll_reset removes assignments added by qdpll_assume before.
Constraints learned under assumptions are correct independently.
For convenience: calling qdpll_reset_learned_constraints is never required forthe correctness of incremental solving. The solver keeps track of learned constraints.
U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

20 / 22

API: Generating Traces and Certificates/* Configure solver instance via configuration string.
Returns null pointer on success and error string otherwise. */char * qdpll_configure (QDPLL * qdpll, char * configure_str);

Print the full resolution derivation in QRP format to standard output: can be huge!
--trace=qrp (text format) or --trace=bqrp (binary format).
QBFcert framework: http://fmv.jku.at/qbfcert/.
Acknowledgments: Aina Niemetz and Mathias Preiner.
Resolution proof checking by QRPcheck: http://fmv.jku.at/qrpcheck/.
Certificate extraction (Skolem/Herbrand functions) by QRPcert:
http://fmv.jku.at/qrpcert/.
Skolemization/Herbrandization by CertCheck: http://fmv.jku.at/certcheck/.
Checking skolemized/herbrandized formula using a SAT solver.

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

21 / 22

Remarks

Please publish your benchmarks!
Effective use of QBF solvers (sometimes) requires expert knowledge and fine tuning.
Long-term goal: usability, integrated workflow.

U. Egly and F. Lonsing (TU Wien)

QBFs and DepQBF : DepQBF in Practice

22 / 22