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