Skip to content

v2.5.0
Compare
Choose a tag to compare
@czengler czengler released this 02 May 09:08
· 21 commits to master since this release
v2.5.0
e6f6024

Removed (Potentially Breaking Change!)

  • All parser classes from org.logicng.io.parsers (including in particular the two main parsers PropositionalParser and PseudoBooleanParser) as well as the class org.logicng.io.readers.FormulaReader were moved to the new artifacts org.logicng.logicng-parser-j8 (or org.logicng.logicng-parser-j11 for Java 11). So LogicNG now consists of two artifacts:
    • All the core functionality of LogicNG except for the parser is located in the "old" org.logicng:logicng artifact. This artifact does not depend on ANTLR anymore (which was the reason for splitting the library). This library will stay on Java 8, but nothing should prevent its usage in higher Java versions.
    • The parser functionality is located in org.logicng:logicng-parser-j8 (for Java 8 and ANTLR 4.9.3) and org.logicng:logicng-parser-j11 (for Java 11 and the most recent ANTLR version). The version of this library will stay in sync with the core library.
  • The method FormulaFactory.parse() was removed. If you're using this method you should include one of the new parser artefacts and then just create your own PropositionalParser or PseudoBooleanParser and call parse() on them.

Added

  • Added unsafe methods term and dnf to the FormulaFactory to create a term (conjunction of literals) or a DNF (c.f. with method FormulaFactory#clause and FormulaFactory#cnf). Both methods do not perform reduction operations and therefore are faster. Only use these methods if you are sure the input is free of complementary and redundant operands.
  • Class UBTree offers new method generateSubsumedUBTree to directly generate a subsumed UBTree for the given sets.
  • The DnnfFactory now offers a method to compile a DNNF with a DnnfCompilationHandler
  • The ModelCounter now offers a method to pass a DnnfCompilationHandler in order to control long-running computations

Changed

  • UBTree data structure now supports empty sets.
  • Added side effect note in SATSolver for the four assumption solving methods.
  • Methods for reordering and swapping variables on BDD were refactored: BDD.getReordering, BDDKernel.getReordering, and BDD.swapVariables are now deprecated and should not be used anymore. Instead, there are new methods on the BDDKernel. Note that these actions affect all BDDs generated by the kernel.
    • BDDKernel.swapVariables for swapping two variables (or variable indices)
    • BDDKernel.reorder for automatically reordering the BDD
    • BDDKernel.activateReorderDuringBuild for activating reordering during build
    • BDDKernel.addVariableBlock for defining a variable block for reordering
    • BDDKernel.addAllVariablesAsBlock for defining one block for each variable (s.t. all variables are allowed to be reordered independently)
  • Significant performance improvements in the DTree generation for DNNFs
  • Minor performance improvements in some DNF/CNF generating algorithms by using faster cnf/dnf.

Fixed

  • The formula generation on BDDs was broken when the ordering was changed by BDDKernel.reorder or BDDKernel.swapVariables. This is now fixed.
Assets 5
Loading