Release v2.0.0 · logic-ng/LogicNG

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 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 (not PBConstraint 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 to antlr

Provide feedback