new public method UBTree#generateSubsumedUBTree to generate a subsume…

…d UBTree

CHANGELOG.md

@@ -4,6 +4,10 @@ LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
 ## [2.5.0] - 2023-xx-xx
 
+### Added
+
+- Class `UBTree` offers new method `generateSubsumedUBTree` to directly generate a subsumed UBTree for the given sets. 
+
 ### Changed
 
 - UBTree data structure now supports empty sets.

src/main/java/org/logicng/datastructures/ubtrees/UBTree.java

@@ -29,8 +29,10 @@
 package org.logicng.datastructures.ubtrees;
 
 import java.util.ArrayList;
+import java.util.Collection;
 import java.util.LinkedHashSet;
 import java.util.List;
+import java.util.Map;
 import java.util.Set;
 import java.util.SortedMap;
 import java.util.SortedSet;
@@ -56,6 +58,28 @@ public UBTree() {
         this.rootSet = null;
     }
 
+    /**
+     * Generates a subsumed UBTree from the given sets.
+     * @param sets the sets
+     * @param <E>  the type of the elements (must be comparable)
+     * @return the subsumed UBTree
+     */
+    public static <E extends Comparable<E>> UBTree<E> generateSubsumedUBTree(final Collection<? extends Collection<E>> sets) {
+        final SortedMap<Integer, List<SortedSet<E>>> sizes = new TreeMap<>();
+        for (final Collection<E> set : sets) {
+            sizes.computeIfAbsent(set.size(), k -> new ArrayList<>()).add(new TreeSet<>(set));
+        }
+        final UBTree<E> ubTree = new UBTree<>();
+        for (final Map.Entry<Integer, List<SortedSet<E>>> entry : sizes.entrySet()) {
+            for (final SortedSet<E> set : entry.getValue()) {
+                if (ubTree.firstSubset(set) == null) {
+                    ubTree.addSet(set);
+                }
+            }
+        }
+        return ubTree;
+    }
+
     /**
      * Adds a set of comparable objects to this UBTree.
      * @param set the set of comparable objects

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

@@ -30,41 +30,40 @@
 
 import org.logicng.datastructures.ubtrees.UBTree;
 import org.logicng.formulas.Formula;
+import org.logicng.formulas.FormulaFactory;
 import org.logicng.formulas.Literal;
+import org.logicng.formulas.NAryOperator;
 
 import java.util.ArrayList;
 import java.util.List;
-import java.util.Map;
-import java.util.SortedMap;
 import java.util.SortedSet;
-import java.util.TreeMap;
 
 /**
  * A superclass for subsumptions (CNF or DNF).
- * @version 2.0.0
+ * @version 2.5.0
  * @since 1.5.0
  */
 public abstract class Subsumption {
 
-    /**
-     * Generates a UBTree from the formulas operands (clauses in CNF, minterms in DNF)
-     * where all subsumed operands are already deleted.
-     * @param formula the formula (must be an n-ary operator and CNF or DNF)
-     * @return the UBTree with the operands and deleted subsumed operands
-     */
-    protected static UBTree<Literal> generateSubsumedUBTree(final Formula formula) {
-        final SortedMap<Integer, List<SortedSet<Literal>>> mapping = new TreeMap<>();
-        for (final Formula term : formula) {
-            mapping.computeIfAbsent(term.literals().size(), k -> new ArrayList<>()).add(term.literals());
+    protected static Formula compute(final NAryOperator nary, final boolean cnf) {
+        final List<SortedSet<Literal>> terms = getTerms(nary);
+        final UBTree<Literal> ubTree = UBTree.generateSubsumedUBTree(terms);
+        return toNormalForm(ubTree, cnf, nary.factory());
+    }
+
+    private static List<SortedSet<Literal>> getTerms(final NAryOperator nary) {
+        final List<SortedSet<Literal>> terms = new ArrayList<>();
+        for (final Formula term : nary) {
+            terms.add(term.literals());
         }
-        final UBTree<Literal> ubTree = new UBTree<>();
-        for (final Map.Entry<Integer, List<SortedSet<Literal>>> entry : mapping.entrySet()) {
-            for (final SortedSet<Literal> set : entry.getValue()) {
-                if (ubTree.firstSubset(set) == null) {
-                    ubTree.addSet(set);
-                }
-            }
+        return terms;
+    }
+
+    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));
         }
-        return ubTree;
+        return cnf ? f.cnf(terms) : f.or(terms);
     }
 }

src/main/java/org/logicng/transformations/cnf/CNFSubsumption.java

@@ -28,23 +28,18 @@
 
 package org.logicng.transformations.cnf;
 
-import org.logicng.datastructures.ubtrees.UBTree;
+import org.logicng.formulas.And;
 import org.logicng.formulas.FType;
 import org.logicng.formulas.Formula;
 import org.logicng.formulas.FormulaTransformation;
-import org.logicng.formulas.Literal;
 import org.logicng.transformations.Subsumption;
 
-import java.util.ArrayList;
-import java.util.List;
-import java.util.SortedSet;
-
 /**
  * This transformation performs subsumption on a given CNF and returns a new CNF.
  * I.e. performs as many subsumptions as possible.  A subsumption in a CNF means,
  * that e.g. a clause {@code A | B | C} is subsumed by another clause {@code A | B}
  * and can therefore be deleted for an equivalent CNF.
- * @version 2.3.0
+ * @version 2.5.0
  * @since 1.5.0
  */
 public final class CNFSubsumption extends Subsumption implements FormulaTransformation {
@@ -77,11 +72,6 @@ public Formula apply(final Formula formula, final boolean cache) {
             return formula;
         }
         assert formula.type() == FType.AND;
-        final UBTree<Literal> ubTree = generateSubsumedUBTree(formula);
-        final List<Formula> clauses = new ArrayList<>();
-        for (final SortedSet<Literal> literals : ubTree.allSets()) {
-            clauses.add(formula.factory().clause(literals));
-        }
-        return formula.factory().cnf(clauses);
+        return compute((And) formula, true);
     }
 }

src/main/java/org/logicng/transformations/dnf/DNFSubsumption.java

@@ -28,23 +28,18 @@
 
 package org.logicng.transformations.dnf;
 
-import org.logicng.datastructures.ubtrees.UBTree;
 import org.logicng.formulas.FType;
 import org.logicng.formulas.Formula;
 import org.logicng.formulas.FormulaTransformation;
-import org.logicng.formulas.Literal;
+import org.logicng.formulas.Or;
 import org.logicng.transformations.Subsumption;
 
-import java.util.ArrayList;
-import java.util.List;
-import java.util.SortedSet;
-
 /**
  * This transformation performs subsumption on a given DNF and returns a new DNF.
  * I.e. performs as many subsumptions as possible.  A subsumption in a DNF means,
  * that e.g. a minterm {@code A & B & C} is subsumed by another minterm {@code A & B}
  * and can therefore be deleted for an equivalent DNF.
- * @version 2.3.0
+ * @version 2.5.0
  * @since 1.5.0
  */
 public final class DNFSubsumption extends Subsumption implements FormulaTransformation {
@@ -76,11 +71,6 @@ public Formula apply(final Formula formula, final boolean cache) {
             return formula;
         }
         assert formula.type() == FType.OR;
-        final UBTree<Literal> ubTree = generateSubsumedUBTree(formula);
-        final List<Formula> minterms = new ArrayList<>();
-        for (final SortedSet<Literal> literals : ubTree.allSets()) {
-            minterms.add(formula.factory().and(literals));
-        }
-        return formula.factory().or(minterms);
+        return compute((Or) formula, false);
     }
 }

src/test/java/org/logicng/datastructures/ubtrees/UBTreeTest.java

@@ -28,11 +28,13 @@
 
 package org.logicng.datastructures.ubtrees;
 
+import static java.util.Arrays.asList;
+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;
 
-import java.util.Arrays;
 import java.util.SortedSet;
 import java.util.TreeSet;
 
@@ -43,6 +45,19 @@
  */
 public class UBTreeTest {
 
+    @Test
+    public void testGenerateSubsumedUBTree() {
+        final SortedSet<String> e0123 = set("e0", "e1", "e2", "e3");
+        final SortedSet<String> e013 = set("e0", "e1", "e3");
+        final SortedSet<String> e012 = set("e0", "e1", "e2");
+        final SortedSet<String> e23 = set("e2", "e3");
+        final SortedSet<String> empty = set();
+        assertThat(UBTree.generateSubsumedUBTree(emptyList()).allSets()).isEmpty();
+        assertThat(UBTree.generateSubsumedUBTree(singletonList(e0123)).allSets()).containsExactlyInAnyOrder(e0123);
+        assertThat(UBTree.generateSubsumedUBTree(asList(e0123, e013, e012, e23)).allSets()).containsExactlyInAnyOrder(e013, e012, e23);
+        assertThat(UBTree.generateSubsumedUBTree(asList(e0123, e013, e012, e23, empty)).allSets()).containsExactlyInAnyOrder(empty);
+    }
+
     @Test
     public void testEmtpyUBTree() {
         final UBTree<String> tree = new UBTree<>();
@@ -410,6 +425,6 @@ public void testAllSets() {
     }
 
     private static SortedSet<String> set(final String... elements) {
-        return new TreeSet<>(Arrays.asList(elements));
+        return new TreeSet<>(asList(elements));
     }
 }