v1.3

Parsing was completely rewritten in this version, so it is more united. Furthermore, this also allowed to change localisation a bit, quantifier trees can now share subtrees, significantly reducing memory usage.

New

• added parsing of non-cleansed prenex (D)QCIR format
• added two new options '--dqcir-output' and '--dqcir-output-cleansed' for printing parsed and possibly preprocessed input into given output file in non-cleansed or cleansed prenex DQCIR format (the option '--hqspre-dqcir-output' was removed, as '--dqcir-output-cleansed' with preprocessing turned on replaces it)
• quantifier trees used for localisation can now share subtrees, significantly reducing memory usage

v1.2

This release updates the localisation algorithm to save memory/time and also fixes the problems with using copies of variables with the same name for localisation of existential quantifiers. Furthermore, this release can be compiled and run on Mac systems. It also uses newer version of HQSpre (the one packaged with the version of HQS from 18-03-2021). Finally, it adds support for prenex cleansed DQCIR format with a possibility to write the output of HQSpre preprocessing to DQCIR file.

Fixes

• added checks in DQDIMACS parser for errors and fixed parsing of free variables
• some solved instances by HQSpre during parsing were not caught, leading to a thrown exception
• the copies of universal variables (which DQBDD does not rename) will now not be taken into account for computing the conditions of pushing existential variables for disjunction

New

• added parser for QBFs in prenex cleansed (D)QCIR format (prenex DQCIR is like prenex QCIR, where we can add quantifier depend(v, v1, ..., vn) which represents existential variable v with dependency set {v1, ..., vn})
• added an option to force file format (otherwise it is selected automatically by file type)
• DQBDD now works also on Mac
• changed how localisation is computed to save on memory/time
• added option '--hqspre-dqcir-output' which takes filename.dqdimacs file, preprocesses it with HQSpre and transforms the result (with gate extraction) into filename.dqcir

v1.1

Fixes:

• dynamic reordering is temporarily turned off during creation of existential dependency copies

New:

• added option to turn on/off dynamic reordering (turned on by default)

v1.0

Initial release of DQBDD, a BDD based DQBF solver. This version allows quantifier elimination with localisation (with option to eliminate only simple variables). It also implements three types of universal variables ordering (for elimination), either based on the number of dependencies (set either at beginning or dynamically chosen) or based on the number of variables occuring in the two conjuncts of universal expansion.