Release 1.3

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-1.2-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-1.3-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>1.2</version>
+  <version>1.3</version>
 </dependency>
 ```
 to you Maven POM.
@@ -59,6 +59,12 @@ final Tristate result = miniSat.sat();
 The library is released under the Apache License and therefore is free to use in any private, educational, or commercial projects.  Commercial support is available.  Please contact Christoph Zengler at [email protected] for further details.
 
 ## Changelog
+### Version 1.3 (Release October 2017)
+* MiniSat and Glucose have a new option for proof tracing.  A DRUP implementation stores all the necessary information for generating a proof for unsatisfiable formulas after solving them.  The new method can be found in the SAT solver class: `unsatCore()`
+* Unsat Cores are now parametrized with the proposition type
+* A new simplifier which applies the distributive law was added: `DistributiveSimplifier`
+* Some minor bug-fixes in handling corner cases of cardinality and pseudo-Boolean constraints 
+
 ### Version 1.2 (Release July 2017)
 * Introduced an extended formula factory which is able to return to a previously saved state and delete old formulas (and get them garbage collected)
 * A simple data structure for generic graphs including algorithms for connected components and maximal cliques
@@ -69,5 +75,5 @@ The library is released under the Apache License and therefore is free to use in
 
 ### Version 1.1 (Release August 2016)
 * Implemented cardinality constraint encodings and pseudo-Boolean constraints encodings of PBLib
-* Incremental cardinality constraints, including the possibility to add cardinaliy constraints to the solver without introducing new formula factory variables 
+* Incremental cardinality constraints, including the possibility to add cardinaliy constraints to the solver without introducing new formula factory variables
 * Different MUS algorithms

pom.xml

@@ -26,7 +26,7 @@
   <modelVersion>4.0.0</modelVersion>
   <groupId>org.logicng</groupId>
   <artifactId>logicng</artifactId>
-  <version>1.2</version>
+  <version>1.3</version>
   <packaging>jar</packaging>
 
   <name>LogicNG</name>
@@ -130,13 +130,6 @@
               <rules>
                 <rule>
                   <element>BUNDLE</element>
-                  <limits>
-                    <limit>
-                      <counter>COMPLEXITY</counter>
-                      <value>COVEREDRATIO</value>
-                      <minimum>0.8</minimum>
-                    </limit>
-                  </limits>
                 </rule>
               </rules>
             </configuration>

src/main/java/org/logicng/cardinalityconstraints/CCAMOBimander.java

@@ -58,18 +58,18 @@
 
 /**
  * Encodes that at most one variable is assigned value true.  Uses the bimander encoding due to Hölldobler and Nguyen.
- * @version 1.1
+ * @version 1.3
  * @since 1.1
  */
 final class CCAMOBimander implements CCAtMostOne {
 
+  private final LNGVector<LNGVector<Literal>> groups;
+  private final LNGVector<Literal> bits;
+  private final int m;
   private EncodingResult result;
-  private LNGVector<LNGVector<Literal>> groups;
-  private LNGVector<Literal> bits;
   private int numberOfBits;
   private int twoPowNBits;
   private int k;
-  private int m;
 
   /**
    * Constructs the bimander AMO encoder with a given number of groups.

src/main/java/org/logicng/cardinalityconstraints/CCAMOCommander.java

@@ -58,16 +58,16 @@
 
 /**
  * Encodes that at most one variable is assigned value true.  Uses the commander encoding due to Klieber & Kwon.
- * @version 1.1
+ * @version 1.3
  * @since 1.1
  */
 final class CCAMOCommander implements CCAtMostOne {
 
+  private final int k;
+  private final LNGVector<Literal> literals;
+  private final LNGVector<Literal> nextLiterals;
+  private final LNGVector<Literal> currentLiterals;
   private EncodingResult result;
-  private int k;
-  private LNGVector<Literal> literals;
-  private LNGVector<Literal> nextLiterals;
-  private LNGVector<Literal> currentLiterals;
 
   /**
    * Constructs the commander AMO encoder with a given group size.

src/main/java/org/logicng/cardinalityconstraints/CCAMONested.java

@@ -58,12 +58,12 @@
 
 /**
  * Encodes that at most one variable is assigned value true.  Uses the nested encoding.
- * @version 1.1
+ * @version 1.3
  * @since 1.1
  */
 final class CCAMONested implements CCAtMostOne {
 
-  private int groupSize;
+  private final int groupSize;
   private EncodingResult result;
 
   /**

src/main/java/org/logicng/cardinalityconstraints/CCEncoder.java

@@ -33,16 +33,12 @@
 import org.logicng.configurations.ConfigurationType;
 import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.FType;
-import org.logicng.formulas.Formula;
 import org.logicng.formulas.FormulaFactory;
 import org.logicng.formulas.Literal;
 import org.logicng.formulas.PBConstraint;
 import org.logicng.formulas.Variable;
 import org.logicng.util.Pair;
 
-import java.util.ArrayList;
-import java.util.List;
-
 /**
  * An encoder for cardinality constraints.
  * <p>
@@ -55,7 +51,7 @@
  * has no associated cardinality constraint encoder configuration.  If you change the configuration in the factory,
  * all encoders constructed for this factory will be affected.</li>
  * </ol>
- * @version 1.1
+ * @version 1.3
  * @since 1.1
  */
 public class CCEncoder {
@@ -237,42 +233,41 @@ private void encodeConstraint(final PBConstraint cc, final EncodingResult result
    * Encodes an at-most-one constraint.
    * @param result the result
    * @param vars   the variables of the constraint
-   * @return the CNF encoding of the constraint
    */
-  private List<Formula> amo(final EncodingResult result, final Variable... vars) {
+  private void amo(final EncodingResult result, final Variable... vars) {
     if (vars.length <= 1)
-      return new ArrayList<>();
+      return;
     switch (this.config().amoEncoder) {
       case PURE:
         if (this.amoPure == null)
           this.amoPure = new CCAMOPure();
         this.amoPure.build(result, vars);
-        return result.result();
+        break;
       case LADDER:
         if (this.amoLadder == null)
           this.amoLadder = new CCAMOLadder();
         this.amoLadder.build(result, vars);
-        return result.result();
+        break;
       case PRODUCT:
         if (this.amoProduct == null)
           this.amoProduct = new CCAMOProduct(this.config().productRecursiveBound);
         this.amoProduct.build(result, vars);
-        return result.result();
+        break;
       case NESTED:
         if (this.amoNested == null)
           this.amoNested = new CCAMONested(this.config().nestingGroupSize);
         this.amoNested.build(result, vars);
-        return result.result();
+        break;
       case COMMANDER:
         if (this.amoCommander == null)
           this.amoCommander = new CCAMOCommander(this.config().commanderGroupSize);
         this.amoCommander.build(result, vars);
-        return result.result();
+        break;
       case BINARY:
         if (this.amoBinary == null)
           this.amoBinary = new CCAMOBinary();
         this.amoBinary.build(result, vars);
-        return result.result();
+        break;
       case BIMANDER:
         if (this.config().bimanderGroupSize != CCConfig.BIMANDER_GROUP_SIZE.FIXED || this.amoBimander == null) {
           int groupSize;
@@ -292,10 +287,10 @@ private List<Formula> amo(final EncodingResult result, final Variable... vars) {
           this.amoBimander = new CCAMOBimander(groupSize);
         }
         this.amoBimander.build(result, vars);
-        return result.result();
+        break;
       case BEST:
         this.bestAMO(vars.length).build(result, vars);
-        return result.result();
+        break;
       default:
         throw new IllegalStateException("Unknown at-most-one encoder: " + this.config().amoEncoder);
     }

src/main/java/org/logicng/cardinalityconstraints/CCModularTotalizer.java

@@ -57,15 +57,15 @@
 
 /**
  * Modular Totalizer.
- * @version 1.1
+ * @version 1.3
  * @since 1.0
  */
 final class CCModularTotalizer {
 
   private final Variable varUndef;
   private final Variable varError;
 
-  private Variable h0;
+  private final Variable h0;
   private LNGVector<Literal> inlits;
   private LNGVector<Literal> cardinalityUpOutvars;
   private LNGVector<Literal> cardinalityLwOutvars;

src/main/java/org/logicng/collections/LNGDoublePriorityQueue.java

@@ -54,14 +54,14 @@
 
 /**
  * A simple priority queue implementation for positive integer elements with double priorities taken from CleaneLing.
- * @version 1.1
+ * @version 1.3
  * @since 1.0
  */
 public final class LNGDoublePriorityQueue {
 
-  private LNGIntVector heap;
-  private LNGDoubleVector prior;
-  private LNGIntVector pos;
+  private final LNGIntVector heap;
+  private final LNGDoubleVector prior;
+  private final LNGIntVector pos;
 
   /**
    * Creates a new priority queue.

src/main/java/org/logicng/collections/LNGLongPriorityQueue.java

@@ -52,14 +52,14 @@
 
 /**
  * A simple priority queue implementation for elements with long priorities taken from CleaneLing.
- * @version 1.1
+ * @version 1.3
  * @since 1.0
  */
 public final class LNGLongPriorityQueue {
 
-  private LNGIntVector heap;
-  private LNGLongVector prior;
-  private LNGIntVector pos;
+  private final LNGIntVector heap;
+  private final LNGLongVector prior;
+  private final LNGIntVector pos;
 
   /**
    * Creates a new priority queue.

src/main/java/org/logicng/datastructures/EncodingAuxiliaryVariable.java

@@ -36,6 +36,8 @@
  * <p></p>
  * This variable is used, if the result is added directly to a solver.  In this case no variable on the factory has
  * to be created.
+ * @version 1.3
+ * @since 1.1
  */
 final class EncodingAuxiliaryVariable extends Variable {
 

src/main/java/org/logicng/datastructures/EncodingResult.java

@@ -48,7 +48,7 @@
  * in the formula factory and therefore polluting the factory and the heap.  This class can be used to connect an
  * encoding directly with a SAT solver and therefore introducing the variables only on the solver - not in the factory.
  * When working with many encodings, this can be a large performance gain.
- * @version 1.2
+ * @version 1.3
  * @since 1.1
  */
 public final class EncodingResult {
@@ -121,7 +121,7 @@ else if (this.miniSat != null) {
           litNum = lit.phase() ? index * 2 : (index * 2) ^ 1;
         clauseVec.push(litNum);
       }
-      this.miniSat.underlyingSolver().addClause(clauseVec);
+      this.miniSat.underlyingSolver().addClause(clauseVec, null);
       this.miniSat.setSolverToUndef();
     } else {
       for (Literal lit : literals) {
@@ -155,7 +155,7 @@ else if (this.miniSat != null) {
           litNum = lit.phase() ? index * 2 : (index * 2) ^ 1;
         clauseVec.push(litNum);
       }
-      this.miniSat.underlyingSolver().addClause(clauseVec);
+      this.miniSat.underlyingSolver().addClause(clauseVec, null);
       this.miniSat.setSolverToUndef();
     } else {
       for (Literal lit : literals) {

src/main/java/org/logicng/explanations/unsatcores/MUSGeneration.java

@@ -37,7 +37,7 @@
 
 /**
  * Computes a minimal unsatisfiable subset (MUS) of a given formula with different algorithms.
- * @version 1.1
+ * @version 1.3
  * @since 1.1
  */
 public final class MUSGeneration {
@@ -57,9 +57,10 @@ public MUSGeneration() {
    * Computes a MUS for the given propositions with the default algorithm and the default configuration.
    * @param propositions the propositions
    * @param f            the formula factory
+   * @param <T>          the type of the MUSes propositions
    * @return the MUS
    */
-  public UNSATCore computeMUS(final List<Proposition> propositions, final FormulaFactory f) {
+  public <T extends Proposition> UNSATCore<T> computeMUS(final List<T> propositions, final FormulaFactory f) {
     return this.computeMUS(propositions, f, new MUSConfig.Builder().build());
   }
 
@@ -68,9 +69,10 @@ public UNSATCore computeMUS(final List<Proposition> propositions, final FormulaF
    * @param propositions the propositions
    * @param f            the formula factory
    * @param config       the MUS configuration
+   * @param <T>          the type of the MUSes propositions
    * @return the MUS
    */
-  public UNSATCore computeMUS(final List<Proposition> propositions, final FormulaFactory f, final MUSConfig config) {
+  public <T extends Proposition> UNSATCore<T> computeMUS(final List<T> propositions, final FormulaFactory f, final MUSConfig config) {
     if (propositions.isEmpty())
       throw new IllegalArgumentException("Cannot generate a MUS for an empty list of propositions");
     switch (config.algorithm) {

src/main/java/org/logicng/explanations/unsatcores/UNSATCore.java

@@ -35,20 +35,21 @@
 
 /**
  * An unsatisfiable core (can be a minimal unsatisfiable sub-formula).
- * @version 1.1
+ * @param <T> the type of the core's propositions
+ * @version 1.3
  * @since 1.1
  */
-final public class UNSATCore {
+final public class UNSATCore<T extends Proposition> {
 
-  private final List<Proposition> propositions;
+  private final List<T> propositions;
   private final boolean isMUS;
 
   /**
    * Constructs a new unsatisfiable core.
    * @param propositions the propositions of the core
    * @param isMUS        {@code true} if it is a MUS, {@code false} otherwise
    */
-  public UNSATCore(final List<Proposition> propositions, boolean isMUS) {
+  public UNSATCore(final List<T> propositions, boolean isMUS) {
     this.propositions = propositions;
     this.isMUS = isMUS;
   }
@@ -57,7 +58,7 @@ public UNSATCore(final List<Proposition> propositions, boolean isMUS) {
    * Returns the propositions of this MUS.
    * @return the propositions of this MUS
    */
-  public List<Proposition> propositions() {
+  public List<T> propositions() {
     return this.propositions;
   }
 

src/main/java/org/logicng/explanations/unsatcores/algorithms/DeletionBasedMUS.java

@@ -41,14 +41,14 @@
 
 /**
  * A naive deletion-based MUS algorithm.
- * @version 1.1
+ * @version 1.3
  * @since 1.1
  */
 public final class DeletionBasedMUS extends MUSAlgorithm {
 
   @Override
-  public UNSATCore computeMUS(List<Proposition> propositions, final FormulaFactory f, final MUSConfig config) {
-    final List<Proposition> mus = new ArrayList<>(propositions.size());
+  public <T extends Proposition> UNSATCore<T> computeMUS(List<T> propositions, final FormulaFactory f, final MUSConfig config) {
+    final List<T> mus = new ArrayList<>(propositions.size());
     final List<SolverState> solverStates = new ArrayList<>(propositions.size());
     final MiniSat solver = MiniSat.miniSat(f);
     for (final Proposition proposition : propositions) {
@@ -64,6 +64,6 @@ public UNSATCore computeMUS(List<Proposition> propositions, final FormulaFactory
       if (solver.sat() == Tristate.TRUE)
         mus.add(propositions.get(i));
     }
-    return new UNSATCore(mus, true);
+    return new UNSATCore<>(mus, true);
   }
 }