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

Changelog History
Page 1

  • v2.3.2 Changes

    August 02, 2022

    ๐Ÿ”„ Changed

    • The cached PB and CC encodings are no longer held in the constraint itselt but analogously to the other caches in the formula factory.

    ๐Ÿ›  Fixed

    • A small bug which could occur when using the extended formula factory in combination with cached CC and PB encodings.
  • v2.3.1 Changes

    July 27, 2022

    ๐Ÿ”„ Changed

    • โœ‚ Removed negativeVariables from the internal representation of Assignment it is now computed each time the method is called. This leeds to a minimal performance disadvantage but to a proportional better memory footprint. The public API is not changed.
    • โšก๏ธ Updated ANTLR to 4.9.3 (there were no relevant updates to the Java target, therefore no changes are expected for LogicNG)

    ๐Ÿ›  Fixed

    • A small bug when comparing two backbones with the same set of negative/positive/optional variables but different satisfiability.
  • v2.3.0 Changes

    July 18, 2022

    โž• Added

    • Overloaded method createAssignment in MiniSat by flag whether the created assignment should be a fast evaluable assignment.
    • ๐Ÿ— Extended ModelEnumerationFunction.Builder by flag fastEvaulable which indicates whether the created assignments should be a fast evaluable assignment.
    • Convenience methods isNNF(), isDNF() and isCNF() in class Formula
    • Two new constructors for Substitutions and a new method getMapping() to get the internal mapping
    • Method getSubstitution on Anonymizer to get the mapping from original variable to anonymized one
    • A DNF from BDD function BDDDNFFunction, a subclass of the newly added class BDDNormalFormFunction
    • A DNF from BDD formula transformation BDDDNFTransformation, a subclass of the newly added class BDDNormalFormTransforamtion
    • A canonical CNF enumeration CanonicalCNFEnumeration, a subclass of the newly added class CanonicalEnumeration.

    ๐Ÿ”„ Changed

    • ๐Ÿ‘Œ Improved methods intersection and union in CollectionHelper by using bounded wildcards.
    • ๐Ÿ‘Œ Improved performance of hashCode and equals in Assignment by avoiding redundant hash set creation.
    • Method BDD#dnf() uses the newly introduced BDDDNFFunction to obtain a smaller DNF instead of a canonical DNF
    • Class BDDCNFFunction uses the singleton pattern
    • 0๏ธโƒฃ All functions/transformations/predicates with only a default constructor introduce a static get() method with the singleton pattern. The public constructors are now deprecated and will be removed with LogicNG 3.0
    • ๐Ÿ”ง Always use the default configuration of algorithms from the formula factory and do not construct them in the respective classes separately.

    ๐Ÿ›  Fixed

    • Minor edge case issue in NegationSimplifier which yielded a larger result formula than input formula.
    • โœ… The TermPredicate logic was inverted. In detail, the minterm predicate TermPredicate#getMintermPredicate() tested for a maxterm and the TermPredicate#getMaxtermPredicate() tested for a minterm. To prevent silent errors for callers of these predicates, the factory method names were changed to minterm() and maxterm(), respectively. Thus, an intentional breaking change on compile time level has been introduced to force callers to adjust their logic.
    • Minor edge case issue in MiniSat when performing assumption solving with proof tracing.
    • ๐Ÿ›  Fixed two bugs in the backbone computation on the MiniCard solver.
  • v2.2.1 Changes

    June 11, 2022

    โž• Added

    • ๐Ÿ”Œ Basic support for OSGi via maven-bundle-plugin
  • v2.2.0 Changes

    November 09, 2021

    โž• Added

    • ๐Ÿ‘Œ Improved FormulaFactory by avoiding creating unnecessary negations (cache pollution) during the check for complementary operands.
    • ๐Ÿ‘Œ Improved the NNF computation by avoiding creating unnecessary negations (cache pollution) during the recursive calls.
    • Extracted the NNF computation in its own transformation class NNFTransformation.
    • ๐Ÿšš Moved all formula caches from the Formula class to the FormulaFactory to save memory by avoiding creating empty cache maps.
    • ๐Ÿ†• New TermPredicate class to check whether a formula is a minterm (clause) or maxterm (DNF term).
    • Extended helper classes CollectionHelper and FormulaHelper by additional convenient methods.

    ๐Ÿ›  Fixed

    • ๐Ÿ›  Fixed a bug in the addSoftFormula method of the MaxSATSolver class. A soft formula is now weighted properly if the soft formula is not a clause.
    • ๐Ÿ›  Fixed a bug in the addWithRelaxation method of the SATSolver class. The CNF of the formula is now computed properly regarding the configuration of the solver.

    ๐Ÿ—„ Deprecated

    • ๐Ÿšš Deprecation of method addWithoutUnknown in class SATSolver - this method will be removed in future versions.
    • ๐Ÿšš Deprecation of method addWithRelaxation for propositions in class SATSolver - this method will be removed in future versions.
  • v2.1.0 Changes

    July 18, 2021

    โž• Added

    • Reworked handlers
      • New handlers for backbones, MUS, SMUS, prime compilation, and advanced simplifier
      • three different types for timeout handlers:
        • SINGLE_TIMEOUT: The timeout is started when the handler's started() method is called
        • RESTARTING_TIMEOUT: The timeout is restarted everytime the handler's started() method is called
        • FIXED_END: The timeout is interpreted as a fixed point in time (in milliseconds) at which the computation should be aborted
    • ๐Ÿ‘Œ Improved version detection for compiled and packaged versions of LogicNG
    • โœ… Introduced Mockito for unit tests

    ๐Ÿ›  Fixed

    • ๐Ÿ›  Fixed a bug in the DIMACS formula writer when there was only a single clause with multiple literals
  • 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