LogicNG v2.0.0 Release Notes

Release Date: 2020-07-30 // over 3 years ago
  • โž• 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