Releases: gcharwat/dynqbf
Releases · gcharwat/dynqbf
Release v1.1.1
Release v1.1.0
- Counting support
- Enumeration: limit number of sum-over-product cover models
Release v1.0.2
- Optimization intervals
Release v1.0.1
- Fixed a bug related to QDIMACS input files with \r\n line ending
- Per default, now 30 tree decompositions are generated for TD selection
- Order of quantification and conjunction/disjunction changed
- htd graph preprocessing options (--td-preprocessing)
- Added enhanced maximum cardinality search
- Compatibility with htd release 1.2.0
(see https://github.com/mabseher/htd/releases/tag/1.2)
Release v1.0.0 (final)
- Default parameter tuning
Release candidate v1.0.0-rc.6
- Improved NSF/BDD size balancing
- Minor TD fitness function optimizations
- New LeafNodeCount fitness function
- Dynamic TD selection strategy is now available (2-QBFs: join-child-count, removed-level otherwise)
- Printing License information is now supported
- Compatibility with htd release 1.1-rc1-bugfix
(see https://github.com/mabseher/htd/releases/tag/1.1-rc1-bugfix)
Release candidate v1.0.0-rc.1
- Dynamic dependency scheme selection based on quantifier prefix
- Added detailed decomposition and NSF statistics output
- Unsatisfiable parts of NSFs ore now truncated
- Integrated tree decomposition preprocessing
- Removal cache can now be disabled
- Memory improvements: instance parsing and representation is now more efficient
- Improvements w.r.t. solution enumeration
- Fixed a bug when compiled with clang
- Compatibility with htd release 1.1-rc1
(see https://github.com/mabseher/htd/releases/tag/1.1-rc1)
Release v0.5.1
- Fixed a bug related to the default setting of the selected decomposition strategy
- Minor code cleaning
Release v0.5.0
- Added support for dependency schemes (none, simple and standard)
- "standard" is computed by DepQBF, its integration can be deactivated by modifying the Makefile, see the INSTALL file
- Added RemovedLevelFitness function (that should work well in combination with the "standard" and "simple" dependency schemes)
- Implemented signal handling: Benchmark information is now printed before exit
- The new "verbose" printer prints all computation steps, including the computed BDDs
- The "debug" printer now only prints the size of the BDDs in the NSF data structure
Release v0.4.1
- Fixed unnecessary iteration in unsatisfiability check
- Compatibility with htd release 1.0.1 (see https://github.com/mabseher/htd/releases/tag/1.0.1)