All Versions
16
Latest Version
Avg Release Cycle
113 days
Latest Release
232 days ago
Changelog History
Page 1
Changelog History
Page 1

v2.0.2 Changes
September 19, 2020๐ Fixed
 ๐ Fixed another bug for a special case in the DRUP proof generation

v2.0.1 Changes
September 18, 2020๐ Fixed
 ๐ Fixed a bug for a special case in the DRUP proof generation

v2.0.0 Changes
July 30, 2020โ Added
 DNNF data structure and compilation
 DNNFbased model counting
 BDD Reordering
 โ Computation of shortest MUSes
 Computation of prime implicant and implicates
 ๐ New algorithms for simplifying Boolean formulas including the possibility to define an own rating function for the formula complexity
 A new method for generation constraint graphs of formulas
 A SAT encoding of the SET COVER problem
 ๐ New explicit data structure for cardinality constraints
 ๐ New formula functions for
 Computing the depth of a formula
 Computing a minimum prime implicant of a formula
 ๐ New formula predicates for
 Pseudo Boolean Constraint containment
 Fast evaluation to a constant
 ๐ New formula transformations for
 Literal substitution
 Expansion of pseudoBoolean constraints
 ๐ New solver function for optimizing the current formula on the solver (wrt. the number of positive/negative literals)
 ๐ New formula randomizer and corner case generator, especially useful for testing
 ๐ง Configuration object for formula factory which can be used to allow trivial contradictions and tautologies in formulas and to specify a default merge strategy for formulas from different factories
 ๐ New helper classes for collections
 Stream operators on formulas
๐ Changed
 ๐ Changed Java Version to JDK 8
 switched to ANTLR 4.8
 switched to JUnit 5
 PBC and CC methods in the formula factory return
Formula
objects now (notPBConstraint
objects) and can simplify the constraints  ๐ฆ Moved BDD package to
knowledgecompilation
 ๐ฆ Reorganized
explanations
package  ๐ฆ Reorganized code location in the BDD package and simplified the
BDDFactory
 ๐ฆ Reorganized code location in the SAT Solver package, introduced solver functions which allow better separation of code for functions of the solver
 Propositions now hold a simple formula, no
ImmutableFormulaList
anymore  ๐ fixed a spelling problem: propositions now have a correct
backpack
 More classes are
protected
now and can be extended from outside  ๐ Moved parser grammars from
resources
toantlr
โ Removed
 CleaneLing solver
ImmutableFormulaList
class

v1.6.2 Changes
January 18, 2020โ Added
 ๐ New BDD handlers
๐ Changed
 Some improvements to handlers for computations

v1.6.1 Changes
September 16, 2019โ Added
 A new method for solving a formula with a given literal ordering.
๐ Changed
 โป๏ธ Minor refactoring of the Formatter super class (no effects on callers).
๐ Fixed
 ๐ Fixed the behaviour of model enumeration with additional variables.

v1.6.0 Changes
September 04, 2019โ Added
 A new method for generating CNFs directly on the solver instead of using the formula factory. This often leads to a faster generation and reduced Heap consumption but with the loss of caching
 The current formula on a MiniSatbased solver can be extracted
๐ Changed
 The standard MiniSatbased solvers can now directly efficiently compute a backone. No extra solver is required anymore
 BDD factory can now be extended externally

v1.5.2 Changes
July 15, 2019๐ Changed
 Clarified behaviour of the
Backbone
object
๐ Fixed
 ๐ Fixed caching behaviour when using a
sat()
call without assumptions after a call with assumptions
 Clarified behaviour of the

v1.5.1 Changes
May 08, 2019โ Added
 Introduced a new
FormulaHelper
class for small utility methods on formulas  โ Added a new NNF predicate
๐ Fixed
 ๐ Fixed an unspecified behaviour in
SATPredicate
 ๐ Fixed a small performance issue in the new backbone solver
 ๐ Fixed a bug in a special case of the CNF transformation of a pseudoBoolean constraint
 Introduced a new

v1.5.0 Changes
March 17, 2019โ Added
 Algorithm & data structures for efficiently computing backbones of formulas
 Data structures for UBTrees in order to efficiently identify sub and supersets
 CNF and DNF subsumption as formula transformations
 Backbone simplifier (compute and propagate the backbone of a formula)
 ๐จ A new sorted formula formatter which respects a given variable ordering when printing formulas
๐ Changed
 โป๏ธ Minor code refactorings and improvements
๐ Deprecated
 ๐ Deprecation of CleaneLing  this solver will be removed in future versions.

v1.4.1 Changes
December 07, 2018๐ Changed
 โป๏ธ Some refactorings for unit tests on Windows regarding encodings
 The QuineMcCluskey implementation does not yield CNF auxiliary variables anymore
๐ Fixed
 ๐ Fixed a minor bug in the generation of incremental cardinality constraints