diff --git a/CHANGELOG.md b/CHANGELOG.md index 9b6fa80a..efa6b128 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,13 +6,14 @@ LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html). ### 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. +- 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. ### Changed - UBTree data structure now supports empty sets. - Added side effect note in `SATSolver` for the four assumption solving methods. +- Minor performance improvements in some DNF/CNF generating algorithms by using faster `cnf`/`dnf`. ### Fixed diff --git a/src/main/java/org/logicng/transformations/CanonicalEnumeration.java b/src/main/java/org/logicng/transformations/CanonicalEnumeration.java index 35b9033a..91188056 100644 --- a/src/main/java/org/logicng/transformations/CanonicalEnumeration.java +++ b/src/main/java/org/logicng/transformations/CanonicalEnumeration.java @@ -43,7 +43,7 @@ /** * Superclass for canonical normal form enumeration (CNF or DNF) via enumeration of the falsifying/satisfying assignments. - * @version 2.3.0 + * @version 2.5.0 * @since 2.3.0 */ public abstract class CanonicalEnumeration { @@ -65,9 +65,9 @@ protected static Formula compute(final Formula formula, final boolean cnf) { final List ops = new ArrayList<>(); for (final Assignment a : enumeration) { final SortedSet literals = a.literals(); - final Formula term = cnf ? f.or(FormulaHelper.negate(literals, ArrayList::new)) : f.and(a.literals()); + final Formula term = cnf ? f.clause(FormulaHelper.negateLiterals(literals, ArrayList::new)) : f.term(a.literals()); ops.add(term); } - return cnf ? f.and(ops) : f.or(ops); + return cnf ? f.cnf(ops) : f.dnf(ops); } } diff --git a/src/main/java/org/logicng/transformations/Subsumption.java b/src/main/java/org/logicng/transformations/Subsumption.java index faba0203..9407b236 100644 --- a/src/main/java/org/logicng/transformations/Subsumption.java +++ b/src/main/java/org/logicng/transformations/Subsumption.java @@ -62,8 +62,8 @@ private static List> getTerms(final NAryOperator nary) { private static Formula toNormalForm(final UBTree ubTree, final boolean cnf, final FormulaFactory f) { final List terms = new ArrayList<>(); for (final SortedSet term : ubTree.allSets()) { - terms.add(cnf ? f.or(term) : f.and(term)); + terms.add(cnf ? f.clause(term) : f.term(term)); } - return cnf ? f.cnf(terms) : f.or(terms); + return cnf ? f.cnf(terms) : f.dnf(terms); } }