All Versions
16
Latest Version
Avg Release Cycle
113 days
Latest Release
232 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