LogicNG v2.0.0 Release Notes
Release Date: 2020-07-30 // over 3 years ago-
โ 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