Skip to content

Commit

Permalink
minor performance improvement in some DNF/CNF generating algorithms
Browse files Browse the repository at this point in the history
  • Loading branch information
rouven-walter committed Feb 5, 2024
1 parent d058151 commit 0533c04
Show file tree
Hide file tree
Showing 3 changed files with 7 additions and 6 deletions.
3 changes: 2 additions & 1 deletion CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -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);
}
}
4 changes: 2 additions & 2 deletions src/main/java/org/logicng/transformations/Subsumption.java
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
}

0 comments on commit 0533c04

Please sign in to comment.