diff --git a/CHANGELOG.md b/CHANGELOG.md index 40ca17f6..43bcfdba 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,6 +2,12 @@ LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## [2.6.0] - 2024-08-02 + +### Added + +- Added configuration flag `minimalDnfCover` in `AdvancedSimplifierConfig` to set whether the step for computing the minimal DNF cover should be performed. Default is `true`. + ## [2.5.1] - 2024-07-31 ### Changed diff --git a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java index c5fe33a3..5e28a285 100644 --- a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java +++ b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java @@ -135,16 +135,18 @@ public Formula apply(final Formula formula, final boolean cache) { return config.returnIntermediateResult ? formula : null; } if (!backbone.isSat()) { - return f.falsum(); + return f.falsum(); } backboneLiterals.addAll(backbone.getCompleteBackbone()); simplified = formula.restrict(new Assignment(backboneLiterals)); } - final Formula simplifyMinDnf = computeMinDnf(f, simplified, config); - if (simplifyMinDnf == null) { - return config.returnIntermediateResult ? addLiterals(simplified, backboneLiterals) : null; + if (config.minimalDnfCover) { + final Formula simplifyMinDnf = computeMinDnf(f, simplified, config); + if (simplifyMinDnf == null) { + return config.returnIntermediateResult ? addLiterals(simplified, backboneLiterals) : null; + } + simplified = simplifyWithRating(simplified, simplifyMinDnf, config); } - simplified = simplifyWithRating(simplified, simplifyMinDnf, config); if (config.factorOut) { final Formula factoredOut = simplified.transform(new FactorOutSimplifier(config.ratingFunction)); simplified = simplifyWithRating(simplified, factoredOut, config); @@ -164,13 +166,13 @@ private static Formula addLiterals(final Formula formula, final SortedSet> primeImplicants = primeResult.getPrimeImplicants(); final List minimizedPIs = SmusComputation.computeSmusForFormulas(negateAllLiterals(primeImplicants, f), - Collections.singletonList(simplified), f, config.optimizationConfig); + Collections.singletonList(simplified), f, config.optimizationConfig); if (minimizedPIs == null || config.optimizationConfig.aborted()) { return null; } diff --git a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java index 3f491c05..b9e941c2 100644 --- a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java +++ b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java @@ -42,6 +42,7 @@ public class AdvancedSimplifierConfig extends Configuration { boolean restrictBackbone; + boolean minimalDnfCover; boolean factorOut; boolean simplifyNegations; boolean returnIntermediateResult; @@ -52,6 +53,7 @@ public class AdvancedSimplifierConfig extends Configuration { public String toString() { return "AdvancedSimplifierConfig{" + "restrictBackbone=" + this.restrictBackbone + + ", minimalDnfCover=" + this.minimalDnfCover + ", factorOut=" + this.factorOut + ", simplifyNegations=" + this.simplifyNegations + ", returnIntermediateResult=" + this.returnIntermediateResult + @@ -67,6 +69,7 @@ public String toString() { private AdvancedSimplifierConfig(final Builder builder) { super(ConfigurationType.ADVANCED_SIMPLIFIER); this.restrictBackbone = builder.restrictBackbone; + this.minimalDnfCover = builder.minimalDnfCover; this.factorOut = builder.factorOut; this.simplifyNegations = builder.simplifyNegations; this.returnIntermediateResult = builder.returnIntermediateResult; @@ -88,6 +91,7 @@ public static Builder builder() { public static class Builder { boolean restrictBackbone = true; + boolean minimalDnfCover = true; boolean factorOut = true; boolean simplifyNegations = true; boolean returnIntermediateResult = false; @@ -109,6 +113,17 @@ public Builder restrictBackbone(final boolean restrictBackbone) { return this; } + /** + * Sets the flag for whether a minimal DNF cover should be computed. The + * default is 'true'. + * @param minimalDnfCover flag for the minimal DNF cover computation + * @return the current builder + */ + public Builder minimalDnfCover(final boolean minimalDnfCover) { + this.minimalDnfCover = minimalDnfCover; + return this; + } + /** * Sets the flag for whether the formula should be factorized. The * default is 'true'. diff --git a/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java b/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java index 64a87dee..1a9905e6 100644 --- a/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java +++ b/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java @@ -191,11 +191,13 @@ public void testAdvancedSimplifierConfig() { final FormulaFactory f = new FormulaFactory(); final List configs = Arrays.asList( AdvancedSimplifierConfig.builder().build(), - AdvancedSimplifierConfig.builder().restrictBackbone(false).factorOut(false).simplifyNegations(false).build(), + AdvancedSimplifierConfig.builder().restrictBackbone(false).minimalDnfCover(false).factorOut(false).simplifyNegations(false).build(), AdvancedSimplifierConfig.builder().factorOut(false).simplifyNegations(false).build(), AdvancedSimplifierConfig.builder().restrictBackbone(false).simplifyNegations(false).build(), + AdvancedSimplifierConfig.builder().restrictBackbone(false).minimalDnfCover(false).build(), AdvancedSimplifierConfig.builder().restrictBackbone(false).factorOut(false).build(), AdvancedSimplifierConfig.builder().restrictBackbone(false).build(), + AdvancedSimplifierConfig.builder().minimalDnfCover(false).build(), AdvancedSimplifierConfig.builder().factorOut(false).build(), AdvancedSimplifierConfig.builder().simplifyNegations(false).build()); @@ -216,11 +218,11 @@ public void testAdvancedSimplifierConfig() { @Test public void testBackboneIntermediateResult() { final FormulaFactory f = new FormulaFactory(); - Formula formula = parse(f, "(a & b) | (a & c)"); - OptimizationHandler optHandler = mock(OptimizationHandler.class); + final Formula formula = parse(f, "(a & b) | (a & c)"); + final OptimizationHandler optHandler = mock(OptimizationHandler.class); // abort simplification after successful backbone computation final AtomicInteger count = new AtomicInteger(0); - when(optHandler.aborted()).then(invocationOnMock -> count.addAndGet(1) > 1); + when(optHandler.aborted()).then(invocationOnMock -> count.addAndGet(1) > 1); testHandler(optHandler, formula, true, true); }