Merge branch 'feature/unsafe-dnf' into development

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
 

src/main/java/org/logicng/formulas/FormulaFactory.java

@@ -80,7 +80,7 @@
  * <p>
  * 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<? extends Formula> operandsIn) {
         return or;
     }
 
+    /**
+     * Creates a new DNF from an array of terms (conjunctions of literals).
+     * <p>
+     * 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<Formula> 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).
+     * <p>
+     * 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<? extends Formula> terms) {
+        final LinkedHashSet<? extends Formula> 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<? extends Formula> termsIn) {
+        final LinkedHashSet<? extends Formula> terms = importOrPanic(termsIn);
+        if (terms.isEmpty()) {
+            return this.falsum();
+        }
+        if (terms.size() == 1) {
+            return terms.iterator().next();
+        }
+        Map<LinkedHashSet<? extends Formula>, 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<? extends Formula> 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.
      * <p>
@@ -866,6 +944,70 @@ private Formula constructClause(final LinkedHashSet<Literal> literalsIn) {
         return tempOr;
     }
 
+    /**
+     * Creates a new term from an array of literals.
+     * <p>
+     * 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<Literal> ops = new LinkedHashSet<>(literals.length);
+        Collections.addAll(ops, literals);
+        return this.constructTerm(ops);
+    }
+
+    /**
+     * Creates a new term from a collection of literals.
+     * <p>
+     * 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<? extends Literal> literals) {
+        final LinkedHashSet<Literal> 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<Literal> literalsIn) {
+        final LinkedHashSet<? extends Formula> literals = importOrPanic(literalsIn);
+        if (literals.isEmpty()) {
+            return this.verum();
+        }
+        if (literals.size() == 1) {
+            return literals.iterator().next();
+        }
+        Map<LinkedHashSet<? extends Formula>, 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);

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<Formula> ops = new ArrayList<>();
         for (final Assignment a : enumeration) {
             final SortedSet<Literal> 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);
     }
 }

src/main/java/org/logicng/transformations/Subsumption.java

@@ -62,8 +62,8 @@ private static List<SortedSet<Literal>> getTerms(final NAryOperator nary) {
     private static Formula toNormalForm(final UBTree<Literal> ubTree, final boolean cnf, final FormulaFactory f) {
         final List<Formula> terms = new ArrayList<>();
         for (final SortedSet<Literal> 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);
     }
 }

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,12 +234,18 @@ 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
     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();
     }
 }

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,12 +222,23 @@ 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
     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();
     }
 }