Skip to content

Commit

Permalink
Merge branch 'feature/ubtree-empty-set' into development
Browse files Browse the repository at this point in the history
  • Loading branch information
@rouven-walter
rouven-walter committed Feb 5, 2024
2 parents 5eb5ef2 + 4df12d7 commit ae62996
Show file tree
Hide file tree
Showing 6 changed files with 263 additions and 61 deletions.
7 changes: 6 additions & 1 deletion CHANGELOG.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,10 +2,15 @@

LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html).

## [2.4.2] - 2023-xx-xx
## [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.
- Added side effect note in `SATSolver` for the four assumption solving methods.

### Fixed
Expand Down
66 changes: 58 additions & 8 deletions src/main/java/org/logicng/datastructures/ubtrees/UBTree.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -41,17 +43,41 @@
* A data structure for storing sets with efficient sub- and superset queries.
* C.f. `A New Method to Index and Query Sets`, Hoffmann and Koehler, 1999
* @param <T> the type of the elements (must be comparable)
* @version 2.0.0
* @version 2.5.0
* @since 1.5.0
*/
public final class UBTree<T extends Comparable<T>> {
private final SortedMap<T, UBNode<T>> rootNodes;
private SortedSet<T> rootSet;

/**
* Constructs an empty UBTree.
*/
public UBTree() {
this.rootNodes = new TreeMap<>();
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;
}

/**
Expand All @@ -69,7 +95,9 @@ public void addSet(final SortedSet<T> set) {
}
nodes = node.children();
}
if (node != null) {
if (node == null) {
this.rootSet = set;
} else {
node.setEndSet(set);
}
}
Expand All @@ -80,10 +108,15 @@ public void addSet(final SortedSet<T> set) {
* @return the first subset which is found for the given set or {@code null} if there is none
*/
public SortedSet<T> firstSubset(final SortedSet<T> set) {
if (this.rootNodes.isEmpty() || set == null || set.isEmpty()) {
final boolean emptyTree = this.rootSet == null && this.rootNodes.isEmpty();
if (emptyTree || set == null) {
return null;
}
return firstSubset(set, this.rootNodes);
if (this.rootSet == null) {
return set.isEmpty() ? null : firstSubset(set, this.rootNodes);
} else {
return this.rootSet;
}
}

/**
Expand All @@ -93,6 +126,9 @@ public SortedSet<T> firstSubset(final SortedSet<T> set) {
*/
public Set<SortedSet<T>> allSubsets(final SortedSet<T> set) {
final Set<SortedSet<T>> subsets = new LinkedHashSet<>();
if (this.rootSet != null) {
subsets.add(this.rootSet);
}
allSubsets(set, this.rootNodes, subsets);
return subsets;
}
Expand All @@ -103,6 +139,9 @@ public Set<SortedSet<T>> allSubsets(final SortedSet<T> set) {
* @return all supersets of the given set
*/
public Set<SortedSet<T>> allSupersets(final SortedSet<T> set) {
if (set.isEmpty()) {
return allSets();
}
final Set<SortedSet<T>> supersets = new LinkedHashSet<>();
allSupersets(set, this.rootNodes, supersets);
return supersets;
Expand All @@ -113,9 +152,11 @@ public Set<SortedSet<T>> allSupersets(final SortedSet<T> set) {
* @return all sets in this UBTree
*/
public Set<SortedSet<T>> allSets() {
final List<UBNode<T>> allEndOfPathNodes = getAllEndOfPathNodes(this.rootNodes);
final Set<SortedSet<T>> allSets = new LinkedHashSet<>();
for (final UBNode<T> endOfPathNode : allEndOfPathNodes) {
if (this.rootSet != null) {
allSets.add(this.rootSet);
}
for (final UBNode<T> endOfPathNode : getAllEndOfPathNodes(this.rootNodes)) {
allSets.add(endOfPathNode.set());
}
return allSets;
Expand All @@ -129,6 +170,15 @@ SortedMap<T, UBNode<T>> rootNodes() {
return this.rootNodes;
}

/**
* Returns the set of the root. If the root is a terminal node, it holds an empty set.
* In this case this method returns this set, otherwise it returns {@code null}.
* @return the set of the root node if it is a terminal node, {@code null} otherwise
*/
SortedSet<T> rootSet() {
return this.rootSet;
}

private SortedSet<T> firstSubset(final SortedSet<T> set, final SortedMap<T, UBNode<T>> forest) {
final Set<UBNode<T>> nodes = getAllNodesContainingElements(set, forest);
SortedSet<T> foundSubset = null;
Expand Down Expand Up @@ -159,7 +209,7 @@ private void allSubsets(final SortedSet<T> set, final SortedMap<T, UBNode<T>> fo
}

private void allSupersets(final SortedSet<T> set, final SortedMap<T, UBNode<T>> forest, final Set<SortedSet<T>> supersets) {
final Set<UBNode<T>> nodes = getAllNodesContainingElementsLessThan(set, forest, set.first());
final Set<UBNode<T>> nodes = getAllNodesContainingElementsLessThan(forest, set.first());
for (final UBNode<T> node : nodes) {
allSupersets(set, node.children(), supersets);
}
Expand Down Expand Up @@ -193,7 +243,7 @@ private Set<UBNode<T>> getAllNodesContainingElements(final SortedSet<T> set, fin
return nodes;
}

private Set<UBNode<T>> getAllNodesContainingElementsLessThan(final SortedSet<T> set, final SortedMap<T, UBNode<T>> forest, final T element) {
private Set<UBNode<T>> getAllNodesContainingElementsLessThan(final SortedMap<T, UBNode<T>> forest, final T element) {
final Set<UBNode<T>> nodes = new LinkedHashSet<>();
for (final UBNode<T> node : forest.values()) {
if (node != null && node.element().compareTo(element) < 0) {
Expand Down
43 changes: 21 additions & 22 deletions src/main/java/org/logicng/transformations/Subsumption.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
}
16 changes: 3 additions & 13 deletions src/main/java/org/logicng/transformations/cnf/CNFSubsumption.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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);
}
}
16 changes: 3 additions & 13 deletions src/main/java/org/logicng/transformations/dnf/DNFSubsumption.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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);
}
}
Loading

0 comments on commit ae62996

Please sign in to comment.