All Versions
22
Latest Version
Avg Release Cycle
113 days
Latest Release
181 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