All Versions
17
Latest Version
Avg Release Cycle
125 days
Latest Release
349 days ago
Changelog History
Page 1
Changelog History
Page 1
-
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
-
v1.6.1 Changes
September 16, 2019โ Added
- A new method for solving a formula with a given literal ordering.
๐ Changed
- ๐จ Minor refactoring of the Formatter super class (no effects on callers).
๐ Fixed
- ๐ Fixed the behaviour of model enumeration with additional variables.
-
v1.6.0 Changes
September 04, 2019โ Added
- A new method for generating CNFs directly on the solver instead of using the formula factory. This often leads to a faster generation and reduced Heap consumption but with the loss of caching
- The current formula on a MiniSat-based solver can be extracted
๐ Changed
- The standard MiniSat-based solvers can now directly efficiently compute a backone. No extra solver is required anymore
- BDD factory can now be extended externally
-
v1.5.2 Changes
July 15, 2019๐ Changed
- Clarified behaviour of the
Backbone
object
๐ Fixed
- ๐ Fixed caching behaviour when using a
sat()
call without assumptions after a call with assumptions
- Clarified behaviour of the
-
v1.5.1 Changes
May 08, 2019โ Added
- Introduced a new
FormulaHelper
class for small utility methods on formulas - โ Added a new NNF predicate
๐ Fixed
- ๐ Fixed an unspecified behaviour in
SATPredicate
- ๐ Fixed a small performance issue in the new backbone solver
- ๐ Fixed a bug in a special case of the CNF transformation of a pseudo-Boolean constraint
- Introduced a new
-
v1.5.0 Changes
March 17, 2019โ Added
- Algorithm & data structures for efficiently computing backbones of formulas
- Data structures for UBTrees in order to efficiently identify sub- and supersets
- CNF and DNF subsumption as formula transformations
- Backbone simplifier (compute and propagate the backbone of a formula)
- ๐จ A new sorted formula formatter which respects a given variable ordering when printing formulas
๐ Changed
- ๐จ Minor code refactorings and improvements
๐ Deprecated
- ๐ Deprecation of CleaneLing - this solver will be removed in future versions.