Skip to content

Latest commit

 

History

History
116 lines (91 loc) · 6.34 KB

README.md

File metadata and controls

116 lines (91 loc) · 6.34 KB
Raw

DQBDD

DQBDD is a dependency quantified Boolean formula (DQBF) solver that uses binary decision diagrams (BDDs) as an underlying representation of formulas. It is written in C++ and it reads DQBFs encoded in DQDIMACS or prenex DQCIR format for which it checks their satisfiability using quantifier elimination. For an explanation of the techniques used in DQBDD, see this paper and my master's thesis.

Installation

You can find binaries in tagged release versions. If you want to compile it yourself, you need C++ compiler supporting C++14 standard (GCC 7.4.0 on Ubuntu 18.04.1 and Clang 11.0.3 on macOS 11.1 are known to work) and CMake (3.5 or later). Execute

mkdir Release
cd Release
cmake -DCMAKE_BUILD_TYPE=Release ..
make

to build DQBDD which will be located in Release/src/. However, using master branch is not recommended as it is generally a work in progress.

Dependencies

There is no need to install any dependency, all of them are in libs/ and are compiled with DQBDD. They are these:

Input Formats

DQBDD accepts two input formats: DQDIMACS and prenex DQCIR.

DQDIMACS

DQDIMACS is used to represent DQBFs in prenex CNF form. It is an extension of QDIMACS format where not only a and e quantifiers can be used (representing universal and existential variables respectively), but also d quantifier is introduced (representing existential variable with its dependencies). Appendix C of my thesis contains a full definition of DQDIMACS format.

Example of DQDIMACS format:

p cnf 6 2
a 1 2 0
e 3 0
a 4 0
e 5 0
d 6 1 4 0
-1 6 -3 5 0
-2 -4 5 0

This represents DQBF ∀x1 ∀x2 ∀x4 ∃x3(x1, x2) ∃x5(x1, x2, x4) ∃x6(x1, x4).(¬x1 ∨ x6 ∨ ¬x3 ∨ x5) ∧ (¬x2 ∨ ¬x4 ∨ x5)

Prenex DQCIR

Prenex DQCIR is an extension of prenex QCIR format. This format is used for DQBFs in prenex form, however, it does not need to be in CNF. It adds quantifiers of type depend(v, v1, ..., vn) which represents existential variable v with the dependency set v1, ..., vn. It is assumed that v1, ..., vn were already defined as forall variables and that v was not yet defined. The quantifier exists can still be used and it represents existential variables with the dependency set equal to the set of universal variables which were already defined with forall quantifier.

Example of prenex (cleansed) DQCIR format:

#QCIR-G14 10
forall(1, 2)
exists(3)
forall(4)
exists(5)
depend(6, 1, 4)
output(7)
8 = and(-6, 3)
9 = or(-1, -8, 5)
10 = or(-2, -4, 5)
7 = and(9, 10)

This represents DQBF ∀x1 ∀x2 ∀x4 ∃x3(x1, x2) ∃x5(x1, x2, x4) ∃x6(x1, x4).(¬x1 ∨ ¬(¬x6 ∧ x3) ∨ x5) ∧ (¬x2 ∨ ¬x4 ∨ x5)

Usage

dqbdd [OPTION...] <input file>

<input file> should be a path to formula in DQDIMACS or DQCIR format. For the list of options run DQBDD --help. If the formula is satisfiable, the return value is 10, otherwise it is 20.

Examples

dqbdd file.dqdimacs

solves the formula in file.dqdimacs with the default settings.

dqbdd --preprocess 0 --dyn-reordering 0 file.dqdimacs

solves the formula in file.dqdimacs without running the preprocessor HQSpre first (the default for DQDIMACS files is preprocess 1, i.e. preprocessing is enabled) and without using dynamic reordering of variables in BDDs as implemented in CUDD (dynamic reordering is enabled by default, DQBDD uses Rudell's sifting algorithm).

dqbdd --localise 0 --uvar-choice 1 file.dqdimacs

solves the formula in file.dqdimacs without localising quantifiers (or creating quantifier tree, the default behaviour is --localise 1) where the next universal variable for universal expansion is always the one that has the minimal number of dependent existential variables (--uvar-choice 1). The other options of --uvar-choice are:

  • 0 - the order of universal variables to expand is set at beginning from the smallest to the largest number of dependencies (this is the default),
  • 2 - the next variable is chosen by the number of variables in BDDs representing the two conjucts of universal expansion.
dqbdd --localise 1 --elimination-choice 2 file.dqdimacs

solves the formula in file.dqdimacs with localising quantifiers (this is the default behaviour) where it eliminates all universal and possible existential variables while creating the final BDD from the quantifier tree (--elimination-choice 2). The other options of --elimination-choice are:

  • 0 - does not eliminate any quantifiers,
  • 1 - eliminates only universal variables which do not have any dependencies and all possible existential variables (this is the default).
dqbdd file.dqcir

solves the formula in DQCIR format with the default settings. The default settings are the same as for DQDIMACS format except for preprocessing. As HQSpre can only accept files in DQDIMACS format, there is no preprocessing for DQCIR files.

dqbdd --dqcir-output outfile.dqcir infile.dqdimacs

does not solve the formula, but transforms it into DQCIR format. If preprocessing is turned on (by default it is), it runs HQSpre preprocessor and saves the result of HQSpre with gate extraction to file.dqcir. This is basically the same formula that DQBDD takes when it processes DQDIMACS file with preprocessing.

dqbdd --dqcir-output-cleansed outfile.dqcir file.dqdimacs

same as previous example, but the result is formula in cleansed format (XOR and MUX gates are replaced with a combination of AND and OR gates).

Licence

  • LGPL v3
  • Copyright 2020-2022 Juraj Síč