All Versions
22
Latest Version
Avg Release Cycle
113 days
Latest Release
630 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
maven-bundle-plugin
- 🔌 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
- 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 (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