diff --git a/CHANGELOG.md b/CHANGELOG.md index 60568f49..69c878df 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,10 +2,11 @@ LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html). -## [2.5.0] - 2023-xx-xx +## [2.5.0] - 2024-xx-xx ### 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 @@ -21,6 +22,8 @@ LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html). - `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 +- 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/formulas/FormulaFactory.java b/src/main/java/org/logicng/formulas/FormulaFactory.java index 664df73c..58e77ab5 100644 --- a/src/main/java/org/logicng/formulas/FormulaFactory.java +++ b/src/main/java/org/logicng/formulas/FormulaFactory.java @@ -80,7 +80,7 @@ *

* A formula factory is NOT thread-safe. If you generate formulas from more than one thread you either need to synchronize the formula factory * yourself or you use a formula factory for each single thread. - * @version 2.4.0 + * @version 2.5.0 * @since 1.0 */ public class FormulaFactory { @@ -802,6 +802,84 @@ private Formula constructOr(final LinkedHashSet operandsIn) { return or; } + /** + * Creates a new DNF from an array of terms (conjunctions of literals). + *

+ * ATTENTION: it is assumed that the operands are really terms - this is not checked for performance reasons. + * Also, no reduction of operands is performed - this method should only be used if you are sure that the DNF is free + * of redundant terms. + * @param terms the array of terms + * @return a new DNF + */ + public Formula dnf(final Formula... terms) { + final LinkedHashSet ops = new LinkedHashSet<>(terms.length); + Collections.addAll(ops, terms); + return this.constructDNF(ops); + } + + /** + * Creates a new DNF from a collection of terms (conjunctions of literals). + *

+ * ATTENTION: it is assumed that the operands are really terms - this is not checked for performance reasons. + * Also, no reduction of operands is performed - this method should only be used if you are sure that the DNF is free + * of redundant terms. + * @param terms the collection of terms + * @return a new DNF + */ + public Formula dnf(final Collection terms) { + final LinkedHashSet ops = new LinkedHashSet<>(terms); + return this.constructDNF(ops); + } + + /** + * Creates a new DNF. + * @param termsIn the terms + * @return a new DNF + */ + private Formula constructDNF(final LinkedHashSet termsIn) { + final LinkedHashSet terms = importOrPanic(termsIn); + if (terms.isEmpty()) { + return this.falsum(); + } + if (terms.size() == 1) { + return terms.iterator().next(); + } + Map, Or> opOrMap = this.orsN; + switch (terms.size()) { + case 2: + opOrMap = this.ors2; + break; + case 3: + opOrMap = this.ors3; + break; + case 4: + opOrMap = this.ors4; + break; + default: + break; + } + Or tempOr = opOrMap.get(terms); + if (tempOr != null) { + return tempOr; + } + tempOr = new Or(terms, this); + setCnfCaches(tempOr, isCnf(termsIn)); + opOrMap.put(terms, tempOr); + return tempOr; + } + + private static boolean isCnf(final LinkedHashSet terms) { + if (terms.size() <= 1) { + return true; + } + for (final Formula term : terms) { + if (term.type() != LITERAL) { + return false; + } + } + return true; + } + /** * Creates a new clause from an array of literals. *

@@ -866,6 +944,70 @@ private Formula constructClause(final LinkedHashSet literalsIn) { return tempOr; } + /** + * Creates a new term from an array of literals. + *

+ * ATTENTION: No reduction of operands is performed - this method should only be used if you are sure that the term + * is free of redundant or contradicting literals. + * @param literals the collection of literals + * @return a new term + */ + public Formula term(final Literal... literals) { + final LinkedHashSet ops = new LinkedHashSet<>(literals.length); + Collections.addAll(ops, literals); + return this.constructTerm(ops); + } + + /** + * Creates a new term from a collection of literals. + *

+ * ATTENTION: No reduction of operands is performed - this method should only be used if you are sure that the term + * is free of contradicting literals. + * @param literals the collection of literals + * @return a new term + */ + public Formula term(final Collection literals) { + final LinkedHashSet ops = new LinkedHashSet<>(literals); + return this.constructTerm(ops); + } + + /** + * Creates a new term. + * @param literalsIn the literals + * @return a new term + */ + private Formula constructTerm(final LinkedHashSet literalsIn) { + final LinkedHashSet literals = importOrPanic(literalsIn); + if (literals.isEmpty()) { + return this.verum(); + } + if (literals.size() == 1) { + return literals.iterator().next(); + } + Map, And> opAndMap = this.andsN; + switch (literals.size()) { + case 2: + opAndMap = this.ands2; + break; + case 3: + opAndMap = this.ands3; + break; + case 4: + opAndMap = this.ands4; + break; + default: + break; + } + And tempAnd = opAndMap.get(literals); + if (tempAnd != null) { + return tempAnd; + } + tempAnd = new And(literals, this); + setCnfCaches(tempAnd, true); + opAndMap.put(literals, tempAnd); + return tempAnd; + } + private void setCnfCaches(final Formula formula, final boolean isCNF) { if (isCNF) { setPredicateCacheEntry(formula, IS_CNF, true); 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); } } diff --git a/src/test/java/org/logicng/formulas/AndTest.java b/src/test/java/org/logicng/formulas/AndTest.java index f92742f1..0bc2d126 100644 --- a/src/test/java/org/logicng/formulas/AndTest.java +++ b/src/test/java/org/logicng/formulas/AndTest.java @@ -28,6 +28,8 @@ package org.logicng.formulas; +import static java.util.Collections.emptyList; +import static java.util.Collections.singletonList; import static org.assertj.core.api.Assertions.assertThat; import static org.assertj.core.api.Assertions.assertThatThrownBy; @@ -44,7 +46,7 @@ /** * Unit Tests for the class {@link And}. - * @version 2.3.0 + * @version 2.5.0 * @since 1.0 */ public class AndTest extends TestWithExampleFormulas { @@ -74,7 +76,16 @@ public void testCreator() { assertThat(this.f.and(lits)).isEqualTo(this.AND1); assertThat(this.f.and(this.A, this.B, this.X, this.FALSE)).isEqualTo(this.FALSE); assertThat(this.f.and(this.f.and(this.A, this.B), this.f.and(this.X, this.Y))).isEqualTo(this.f.and(this.A, this.B, this.X, this.Y)); + assertThat(this.f.cnf(emptyList())).isEqualTo(this.f.verum()); + assertThat(this.f.cnf(singletonList(this.f.falsum()))).isEqualTo(this.f.falsum()); + assertThat(this.f.cnf(singletonList(this.f.verum()))).isEqualTo(this.f.verum()); assertThat(this.f.cnf(this.f.clause(this.X, this.Y), this.f.and(this.f.or(this.f.and(this.NX, this.NX), this.NY), this.f.or(this.f.and(this.NX, this.TRUE), this.NY)))).isEqualTo(this.AND3); + assertThat(this.f.term()).isEqualTo(this.f.verum()); + assertThat(this.f.term(this.A)).isEqualTo(this.A); + assertThat(this.f.term(this.A, this.NB)).isEqualTo(this.f.and(this.A, this.NB)); + assertThat(this.f.term(emptyList())).isEqualTo(this.f.verum()); + assertThat(this.f.term(singletonList(this.A))).isEqualTo(this.A); + assertThat(this.f.term(Arrays.asList(this.A, this.NB))).isEqualTo(this.f.and(this.A, this.NB)); assertThat(this.f.naryOperator(FType.AND, this.A, this.B, this.A, this.B, this.A)).isEqualTo(this.AND1); assertThat(this.f.naryOperator(FType.AND, Arrays.asList(this.A, this.B, this.A, this.B, this.A))).isEqualTo(this.AND1); } @@ -223,6 +234,9 @@ public void testIsDNF() { assertThat(this.AND1.isDNF()).isTrue(); assertThat(this.AND2.isDNF()).isTrue(); assertThat(this.AND3.isDNF()).isFalse(); + assertThat(this.f.term().isDNF()).isTrue(); + assertThat(this.f.term(this.A).isDNF()).isTrue(); + assertThat(this.f.term(this.A, this.NB).isDNF()).isTrue(); } @Test @@ -230,5 +244,8 @@ public void testIsCNF() { assertThat(this.AND1.isCNF()).isTrue(); assertThat(this.AND2.isCNF()).isTrue(); assertThat(this.AND3.isCNF()).isTrue(); + assertThat(this.f.term().isCNF()).isTrue(); + assertThat(this.f.term(this.A).isCNF()).isTrue(); + assertThat(this.f.term(this.A, this.NB).isCNF()).isTrue(); } } diff --git a/src/test/java/org/logicng/formulas/OrTest.java b/src/test/java/org/logicng/formulas/OrTest.java index 5eec20a0..35cdce7a 100644 --- a/src/test/java/org/logicng/formulas/OrTest.java +++ b/src/test/java/org/logicng/formulas/OrTest.java @@ -28,6 +28,8 @@ package org.logicng.formulas; +import static java.util.Collections.emptyList; +import static java.util.Collections.singletonList; import static org.assertj.core.api.Assertions.assertThat; import org.junit.jupiter.api.Test; @@ -42,7 +44,7 @@ /** * Unit Tests for the class {@link Or}. - * @version 2.3.0 + * @version 2.5.0 * @since 1.0 */ public class OrTest extends TestWithExampleFormulas { @@ -71,6 +73,16 @@ public void testCreator() { assertThat(this.f.or(this.A, this.B, this.X, this.TRUE)).isEqualTo(this.TRUE); assertThat(this.f.or(this.f.or(this.A, this.B), this.f.or(this.X, this.Y))).isEqualTo(this.f.or(this.A, this.B, this.X, this.Y)); assertThat(this.f.or(this.f.and(this.A, this.B), this.f.or(this.f.and(this.f.and(this.NA, this.NB)), this.f.and(this.f.or(this.NA, this.FALSE), this.NB)))).isEqualTo(this.OR3); + assertThat(this.f.dnf(emptyList())).isEqualTo(this.f.falsum()); + assertThat(this.f.dnf(singletonList(this.f.falsum()))).isEqualTo(this.f.falsum()); + assertThat(this.f.dnf(singletonList(this.f.verum()))).isEqualTo(this.f.verum()); + assertThat(this.f.dnf(this.f.or(this.f.and(this.A, this.B), this.f.and(this.NA, this.NB)))).isEqualTo(this.OR3); + assertThat(this.f.clause()).isEqualTo(this.f.falsum()); + assertThat(this.f.clause(this.A)).isEqualTo(this.A); + assertThat(this.f.clause(this.A, this.NB)).isEqualTo(this.f.or(this.A, this.NB)); + assertThat(this.f.clause(emptyList())).isEqualTo(this.f.falsum()); + assertThat(this.f.clause(singletonList(this.A))).isEqualTo(this.A); + assertThat(this.f.clause(Arrays.asList(this.A, this.NB))).isEqualTo(this.f.or(this.A, this.NB)); assertThat(this.f.naryOperator(FType.OR, Arrays.asList(this.X, this.Y, this.X, this.Y, this.X))).isEqualTo(this.OR1); } @@ -210,6 +222,10 @@ public void testIsDNF() { assertThat(this.OR1.isDNF()).isTrue(); assertThat(this.OR2.isDNF()).isTrue(); assertThat(this.OR3.isDNF()).isTrue(); + assertThat(this.f.clause().isDNF()).isTrue(); + assertThat(this.f.clause(this.A).isDNF()).isTrue(); + assertThat(this.f.clause(this.A, this.NB).isDNF()).isTrue(); + assertThat(this.f.dnf(this.f.or(this.f.and(this.A, this.B), this.f.and(this.NA, this.NB))).isDNF()).isTrue(); } @Test @@ -217,5 +233,12 @@ public void testIsCNF() { assertThat(this.OR1.isCNF()).isTrue(); assertThat(this.OR2.isCNF()).isTrue(); assertThat(this.OR3.isCNF()).isFalse(); + assertThat(this.f.clause().isCNF()).isTrue(); + assertThat(this.f.clause(this.A).isCNF()).isTrue(); + assertThat(this.f.clause(this.A, this.NB).isCNF()).isTrue(); + assertThat(this.f.dnf(this.A).isCNF()).isTrue(); + assertThat(this.f.dnf(this.A, this.NB, this.C).isCNF()).isTrue(); + assertThat(this.f.dnf(this.A, this.NB, this.f.and(this.A, this.C)).isCNF()).isFalse(); + assertThat(this.f.dnf(this.f.or(this.f.and(this.A, this.B), this.f.and(this.NA, this.NB))).isCNF()).isFalse(); } }