All Versions
22
Latest Version
Avg Release Cycle
113 days
Latest Release
687 days ago
Changelog History
Page 1
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 ofAssignment
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.
 โ Removed

v2.3.0 Changes
July 18, 2022โ Added
 Overloaded method
createAssignment
inMiniSat
by flag whether the created assignment should be a fast evaluable assignment.  ๐ Extended
ModelEnumerationFunction.Builder
by flagfastEvaulable
which indicates whether the created assignments should be a fast evaluable assignment.  Convenience methods
isNNF()
,isDNF()
andisCNF()
in classFormula
 Two new constructors for
Substitution
s and a new methodgetMapping()
to get the internal mapping  Method
getSubstitution
onAnonymizer
to get the mapping from original variable to anonymized one  A DNF from BDD function
BDDDNFFunction
, a subclass of the newly added classBDDNormalFormFunction
 A DNF from BDD formula transformation
BDDDNFTransformation
, a subclass of the newly added classBDDNormalFormTransforamtion
 A canonical CNF enumeration
CanonicalCNFEnumeration
, a subclass of the newly added classCanonicalEnumeration
.
๐ Changed
 ๐ Improved methods
intersection
andunion
inCollectionHelper
by using bounded wildcards.  ๐ Improved performance of
hashCode
andequals
inAssignment
by avoiding redundant hash set creation.  Method
BDD#dnf()
uses the newly introducedBDDDNFFunction
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 predicateTermPredicate#getMintermPredicate()
tested for a maxterm and theTermPredicate#getMaxtermPredicate()
tested for a minterm. To prevent silent errors for callers of these predicates, the factory method names were changed tominterm()
andmaxterm()
, 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.
 Overloaded method

v2.2.1 Changes
June 11, 2022โ Added
 ๐ Basic support for OSGi via
mavenbundleplugin
 ๐ Basic support for OSGi via

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 theFormulaFactory
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
andFormulaHelper
by additional convenient methods.
๐ Fixed
 ๐ Fixed a bug in the
addSoftFormula
method of theMaxSATSolver
class. A soft formula is now weighted properly if the soft formula is not a clause.  ๐ Fixed a bug in the
addWithRelaxation
method of theSATSolver
class. The CNF of the formula is now computed properly regarding the configuration of the solver.
๐ Deprecated
 ๐ Deprecation of method
addWithoutUnknown
in classSATSolver
 this method will be removed in future versions.  ๐ Deprecation of method
addWithRelaxation
for propositions in classSATSolver
 this method will be removed in future versions.
 ๐ Improved

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'sstarted()
method is calledRESTARTING_TIMEOUT
: The timeout is restarted everytime the handler'sstarted()
method is calledFIXED_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
 Reworked handlers

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
 DNNFbased 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 pseudoBoolean 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 (notPBConstraint
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
toantlr
โ Removed
 CleaneLing solver
ImmutableFormulaList
class

v1.6.2 Changes
January 18, 2020โ Added
 ๐ New BDD handlers
๐ Changed
 Some improvements to handlers for computations