All Versions
22
Latest Version
Avg Release Cycle
113 days
Latest Release
623 days ago

Changelog History
Page 2

  • 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

  • v1.4.0 Changes

    June 03, 2018

    ➕ Added

    • 📦 BDD package (based on Buddy) for creating, manipulating, and writing BDDs
      • Creation of BDDs from LogicNG formulas
      • CNF, DNF transformation of BDDs
      • Restriction, existential & universal quantifier elimination
      • Model counting & enumeration
      • Different static variable ordering heuristics (FORCE, DFS, BFS, MinMax)
      • Writing BDDs in the GraphViz .dot format
    • Quine-McCluskey Implementation for minimizing canonical DNFs
    • 🆕 New formula transformation for anonymizing formulas

    🔄 Changed

    • 📜 Internal parser and IO improvements. Variables can now start with a digit.

  • v1.3.1 Changes

    January 28, 2018

    ➕ Added

    • 🆕 New formula transformation which imports formulas in another formula factory

    🔄 Changed

    • 🐎 Huge performance boost in the model enumeration of MiniSat

    🛠 Fixed

    • 🛠 Small bugfix for a trivial case in DRUP

  • v1.3.0 Changes

    October 25, 2017

    ➕ Added

    • MiniSat and Glucose have a new option for proof tracing. A DRUP implementation stores all the necessary information for generating a proof for unsatisfiable formulas after solving them. The new method can be found in the SAT solver class: unsatCore()
    • A new simplifier which applies the distributive law was added: DistributiveSimplifier

    🔄 Changed

    • Unsat Cores are now parametrized with the proposition type

    🛠 Fixed

    • 🛠 Some minor bug-fixes in handling corner cases of cardinality and pseudo-Boolean constraints

  • v1.2.0 Changes

    July 14, 2017

    ➕ Added

    • Introduced an extended formula factory which is able to return to a previously saved state and delete old formulas (and get them garbage collected)
    • A simple data structure for generic graphs including algorithms for connected components and maximal cliques
    • 👌 Improved IO (Writers for formulas, Dimacs CNFs, and graphs)

    🔄 Changed

    • SAT solvers can now track the currently known variables
    • ⚡️ Updated to ANTLR 4.7

    🛠 Fixed

    • 🛠 Various smaller bugfixes