diff --git a/CHANGELOG.md b/CHANGELOG.md index ddf2d14f..d5397337 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,10 +2,16 @@ LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## [2.0.2] - 2020-09-19 +### Fixed +- Fixed another bug for a special case in the DRUP proof generation + + ## [2.0.1] - 2020-09-18 ### Fixed - Fixed a bug for a special case in the DRUP proof generation + ## [2.0.0] - 2020-07-30 ### Added - DNNF data structure and compilation diff --git a/README.md b/README.md index aabf75c8..1be1c0db 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -[![wercker status](https://app.wercker.com/status/24c4765f3a0d79520ad80a1e4c20cfa2/s/master "wercker status")](https://app.wercker.com/project/bykey/24c4765f3a0d79520ad80a1e4c20cfa2) [![Coverage Status](https://coveralls.io/repos/logic-ng/LogicNG/badge.svg?branch=master&service=github)](https://coveralls.io/github/logic-ng/LogicNG?branch=master) ![License](https://img.shields.io/badge/license-Apache%202-blue.svg) ![Version](https://img.shields.io/badge/version-2.0.1-ff69b4.svg) +[![wercker status](https://app.wercker.com/status/24c4765f3a0d79520ad80a1e4c20cfa2/s/master "wercker status")](https://app.wercker.com/project/bykey/24c4765f3a0d79520ad80a1e4c20cfa2) [![Coverage Status](https://coveralls.io/repos/logic-ng/LogicNG/badge.svg?branch=master&service=github)](https://coveralls.io/github/logic-ng/LogicNG?branch=master) ![License](https://img.shields.io/badge/license-Apache%202-blue.svg) ![Version](https://img.shields.io/badge/version-2.0.2-ff69b4.svg) logo @@ -19,7 +19,7 @@ LogicNG is released in the Maven Central Repository. To include it just add org.logicng logicng - 2.0.1 + 2.0.2 ``` to your Maven POM. diff --git a/pom.xml b/pom.xml index e5f0d4ee..cc9278b8 100644 --- a/pom.xml +++ b/pom.xml @@ -26,7 +26,7 @@ 4.0.0 org.logicng logicng - 2.0.1 + 2.0.2 jar LogicNG diff --git a/src/main/java/org/logicng/solvers/sat/GlucoseSyrup.java b/src/main/java/org/logicng/solvers/sat/GlucoseSyrup.java index 1fb97e1b..078131e0 100644 --- a/src/main/java/org/logicng/solvers/sat/GlucoseSyrup.java +++ b/src/main/java/org/logicng/solvers/sat/GlucoseSyrup.java @@ -277,10 +277,16 @@ public boolean addClause(final LNGIntVector ps, final Proposition proposition) { if (ps.size() == 0) { this.ok = false; + if (this.config.proofGeneration) { + this.pgProof.push(new LNGIntVector(1, 0)); + } return false; } else if (ps.size() == 1) { uncheckedEnqueue(ps.get(0), null); this.ok = propagate() == null; + if (!this.ok && this.config.proofGeneration) { + this.pgProof.push(new LNGIntVector(1, 0)); + } return this.ok; } else { final MSClause c = new MSClause(ps, false); diff --git a/src/main/java/org/logicng/solvers/sat/MiniSat2Solver.java b/src/main/java/org/logicng/solvers/sat/MiniSat2Solver.java index a28b9b14..8175a3f4 100644 --- a/src/main/java/org/logicng/solvers/sat/MiniSat2Solver.java +++ b/src/main/java/org/logicng/solvers/sat/MiniSat2Solver.java @@ -169,6 +169,9 @@ public boolean addClause(final LNGIntVector ps, final Proposition proposition) { if (ps.empty()) { this.ok = false; + if (this.config.proofGeneration) { + this.pgProof.push(new LNGIntVector(1, 0)); + } return false; } else if (ps.size() == 1) { uncheckedEnqueue(ps.get(0), null); @@ -176,6 +179,9 @@ public boolean addClause(final LNGIntVector ps, final Proposition proposition) { if (this.incremental) { this.unitClauses.push(ps.get(0)); } + if (!this.ok && this.config.proofGeneration) { + this.pgProof.push(new LNGIntVector(1, 0)); + } return this.ok; } else { final MSClause c = new MSClause(ps, false); diff --git a/src/test/java/org/logicng/explanations/drup/DRUPTest.java b/src/test/java/org/logicng/explanations/drup/DRUPTest.java index 37190d87..792ed092 100644 --- a/src/test/java/org/logicng/explanations/drup/DRUPTest.java +++ b/src/test/java/org/logicng/explanations/drup/DRUPTest.java @@ -30,6 +30,7 @@ import static org.assertj.core.api.Assertions.assertThat; import static org.logicng.datastructures.Tristate.FALSE; +import static org.logicng.datastructures.Tristate.TRUE; import org.assertj.core.api.SoftAssertions; import org.junit.jupiter.api.Test; @@ -323,6 +324,50 @@ public void testWithCcPropositions() throws ParserException { assertThat(solver.unsatCore().propositions()).containsExactlyInAnyOrder(p1, p2, p3); } + @Test + public void testWithSpecialUnitCaseMiniSat() throws ParserException { + final FormulaFactory f = new FormulaFactory(); + final SATSolver solver = MiniSat.miniSat(f, MiniSatConfig.builder().proofGeneration(true).build()); + final StandardProposition p1 = new StandardProposition(f.parse("a => b")); + final StandardProposition p2 = new StandardProposition(f.parse("a => c | d")); + final StandardProposition p3 = new StandardProposition(f.parse("b => c | d")); + final StandardProposition p4 = new StandardProposition(f.parse("e | f | g | h => i")); + final StandardProposition p5 = new StandardProposition(f.parse("~j => k | j")); + final StandardProposition p6 = new StandardProposition(f.parse("b => ~(e | f)")); + final StandardProposition p7 = new StandardProposition(f.parse("c => ~j")); + final StandardProposition p8 = new StandardProposition(f.parse("l | m => ~i")); + final StandardProposition p9 = new StandardProposition(f.parse("j => (f + g + h = 1)")); + final StandardProposition p10 = new StandardProposition(f.parse("d => (l + m + e + f = 1)")); + final StandardProposition p11 = new StandardProposition(f.parse("~k")); + solver.addPropositions(p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11); + assertThat(solver.sat()).isEqualTo(TRUE); + solver.add(f.variable("a")); + assertThat(solver.sat()).isEqualTo(FALSE); + assertThat(solver.unsatCore().propositions()).contains(p1, p2, p4, p5, p6, p7, p8, p9, p10, p11); + } + + @Test + public void testWithSpecialUnitCaseGlucose() throws ParserException { + final FormulaFactory f = new FormulaFactory(); + final SATSolver solver = MiniSat.glucose(f, MiniSatConfig.builder().proofGeneration(true).incremental(false).build(), GlucoseConfig.builder().build()); + final StandardProposition p1 = new StandardProposition(f.parse("a => b")); + final StandardProposition p2 = new StandardProposition(f.parse("a => c | d")); + final StandardProposition p3 = new StandardProposition(f.parse("b => c | d")); + final StandardProposition p4 = new StandardProposition(f.parse("e | f | g | h => i")); + final StandardProposition p5 = new StandardProposition(f.parse("~j => k | j")); + final StandardProposition p6 = new StandardProposition(f.parse("b => ~(e | f)")); + final StandardProposition p7 = new StandardProposition(f.parse("c => ~j")); + final StandardProposition p8 = new StandardProposition(f.parse("l | m => ~i")); + final StandardProposition p9 = new StandardProposition(f.parse("j => (f + g + h = 1)")); + final StandardProposition p10 = new StandardProposition(f.parse("d => (l + m + e + f = 1)")); + final StandardProposition p11 = new StandardProposition(f.parse("~k")); + solver.addPropositions(p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11); + assertThat(solver.sat()).isEqualTo(TRUE); + solver.add(f.variable("a")); + assertThat(solver.sat()).isEqualTo(FALSE); + assertThat(solver.unsatCore().propositions()).contains(p1, p2, p4, p5, p6, p7, p8, p9, p10, p11); + } + /** * Checks that each formula of the core is part of the original problem and that the core is really unsat. * @param originalCore the original core