Version 2.0.2

logic-ng · Sep 19, 2020 · 994294f · 994294f
1 parent 708e7a9
commit 994294f
Show file tree

Hide file tree

Showing 6 changed files with 66 additions and 3 deletions.
diff --git 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
@@ -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)
 
 <img src="https://github.com/logic-ng/LogicNG/blob/master/doc/logo/logo_big.png" alt="logo" width="300">
 
@@ -19,7 +19,7 @@ LogicNG is released in the Maven Central Repository.  To include it just add
 <dependency>
   <groupId>org.logicng</groupId>
   <artifactId>logicng</artifactId>
-  <version>2.0.1</version>
+  <version>2.0.2</version>
 </dependency>
 ```
 to your Maven POM.

diff --git a/pom.xml b/pom.xml
@@ -26,7 +26,7 @@
   <modelVersion>4.0.0</modelVersion>
   <groupId>org.logicng</groupId>
   <artifactId>logicng</artifactId>
-  <version>2.0.1</version>
+  <version>2.0.2</version>
   <packaging>jar</packaging>
 
   <name>LogicNG</name>

diff --git 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
@@ -169,13 +169,19 @@ 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);
             this.ok = propagate() == null;
             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
@@ -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