LogicNG changelog

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

• 1
• 2
• 3
• Next ›
• Last »