v2.6.0

Added

• New class OptimizationConfig used to configure optimization computations in various algorithms. It allows to configure the following aspects:
  • the optimizationType (either SAT-based optimization or a MaxSAT algorithm)
  • the maxSATConfig to further configure the MaxSAT algorithm
  • the optimizationHandler to use
  • the maxSATHandler to use
• Added three new configuration options to AdvancedSimplifierConfig:
  • minimalDnfCover determines whether the step for computing the minimal DNF cover should be performed. Default is true.
  • returnIntermediateResult allows to return an intermediate result from the AdvancedSimplifier if the computation was aborted by a handler. Default is false.
  • optimizationConfig can be used to configure the algorithms in the simplifier which perform optimizations, also the OptimizationHandler handler moved into this config

v2.5.1

Changed

• Changed visibility from some methods from package-private to public for formula and solver serializiation via the new https://github.com/logic-ng/serialization library

v2.5.0

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.

v2.4.3-j11

• Updated ANTLR to version 4.13.1

v2.4.2-j11

Changed

• Changed artifact id to logicng-j11 (for Java 11 only)
• Changed Java Version to JDK 11
• switched to ANTLR 4.11.1

v2.4.1

Changed

• Allowing symbol # in variable names for the PropositionalParser and the PseudoBooleanParser.
• Set the Java Jigsaw automatic module name to logicng in the manifest.

v2.4.0

Added

• Completely rewritten graphical outputs of formulas, BDDs, and graphs in the package org.logicng.io.graphical. It is now possible to configure the
  generated graphs by dynamically styling nodes, edges, and computing node labels. Also, there are now two possible output formats: GraphViz DOT and Mermaid.js.
• Convenience methods isSatisfiable, isTautology, isContradiction, implies, isImpliedBy and isEquivalentTo in the Formula class.
• New OLL algorithm for OpenWBO for more efficient weighted MaxSAT solving.
• Two overloaded factory methods mk in MiniSat to construct a solver by formula factory, solver style and optional configuration.
• Methods to directly apply Boolean functions on BDDs
• Added toFormula method on BDDs to generate a formula via Shannon expansion
• Convenience methods variables(Collection<String> names) and variables(String... names) for creating a list of variables in the FormulaFactory class.

Changed

• Methods generateFromCnf(Formula formula) and generateFromCnf(Collection<Formula> formulas) in ConstraintGraphGenerator are now deprecated, since the
  constraint graph generation is not CNF specific. Both methods will be removed with LogicNG 3.0. Instead, use the general
  method generateFromFormulas(Collection<Formula> formulas).

v2.3.2

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

Changed

• Removed negativeVariables from the internal representation of Assignment 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.

v2.3.0

Added

• Overloaded method createAssignment in MiniSat by flag whether the created assignment should be a fast evaluable assignment.
• Extended ModelEnumerationFunction.Builder by flag fastEvaulable which indicates whether the created assignments should be a fast evaluable assignment.
• Convenience methods isNNF(), isDNF() and isCNF() in class Formula
• Two new constructors for Substitutions and a new method getMapping() to get the internal mapping
• Method getSubstitution on Anonymizer to get the mapping from original variable to anonymized one
• A DNF from BDD function BDDDNFFunction, a subclass of the newly added class BDDNormalFormFunction
• A DNF from BDD formula transformation BDDDNFTransformation, a subclass of the newly added class BDDNormalFormTransforamtion
• A canonical CNF enumeration CanonicalCNFEnumeration, a subclass of the newly added class CanonicalEnumeration.

Changed

• Improved methods intersection and union in CollectionHelper by using bounded wildcards.
• Improved performance of hashCode and equals in Assignment by avoiding redundant hash set creation.
• Method BDD#dnf() uses the newly introduced BDDDNFFunction to obtain a smaller DNF instead of a canonical DNF
• Class BDDCNFFunction uses the singleton pattern
• 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 predicate TermPredicate#getMintermPredicate() tested for a maxterm and the
  TermPredicate#getMaxtermPredicate() tested for a minterm. To prevent silent errors for callers of these predicates, the factory method names were changed
  to minterm() and maxterm(), 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.