All Versions
16
Latest Version
Avg Release Cycle
113 days
Latest Release
399 days ago

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
    • DNNF-based 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 pseudo-Boolean 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 (not PBConstraint 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 to antlr

    โœ‚ 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 MiniSat-based solver can be extracted

    ๐Ÿ”„ Changed

    • The standard MiniSat-based 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
  • 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 pseudo-Boolean constraint
  • 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 Quine-McCluskey implementation does not yield CNF auxiliary variables anymore

    ๐Ÿ›  Fixed

    • ๐Ÿ›  Fixed a minor bug in the generation of incremental cardinality constraints