reorganized cardinality constraints and made them configurable

logic-ng · May 26, 2016 · 3ef1b3c · 3ef1b3c
1 parent 810178e
commit 3ef1b3c
Show file tree

Hide file tree

Showing 35 changed files with 679 additions and 1,244 deletions.
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>1.0.1</version>
+  <version>1.1</version>
   <name>LogicNG</name>
   <packaging>jar</packaging>
 

diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCALKTotalizer.java b/src/main/java/org/logicng/cardinalityconstraints/CCALKTotalizer.java
@@ -49,32 +49,32 @@
 
 package org.logicng.cardinalityconstraints;
 
-import org.logicng.collections.ImmutableFormulaList;
+import org.logicng.formulas.Formula;
 import org.logicng.formulas.FormulaFactory;
 import org.logicng.formulas.Variable;
 
-import java.util.Collection;
+import java.util.List;
 
 /**
  * Encodes that at least 'rhs' variables are assigned value true.  Uses the totalizer encoding for
  * translating the cardinality constraint into CNF.
- * @version 1.0
+ * @version 1.1
  * @since 1.0
  */
-public final class CCALKTotalizer extends CCAtLeastK {
+final class CCALKTotalizer implements CCAtLeastK {
 
   private final CCTotalizer totalizer;
 
   /**
    * Constructs a new totalizer.
    * @param f the formula factory
    */
-  public CCALKTotalizer(final FormulaFactory f) {
+  CCALKTotalizer(final FormulaFactory f) {
     this.totalizer = new CCTotalizer(f);
   }
 
   @Override
-  public ImmutableFormulaList build(final Collection<Variable> vars, int rhs) {
+  public List<Formula> build(final Variable[] vars, int rhs) {
     return this.totalizer.buildALK(vars, rhs);
   }
 

diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMKCardinalityNetwork.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMKCardinalityNetwork.java
@@ -51,16 +51,13 @@
 
 package org.logicng.cardinalityconstraints;
 
-import org.logicng.collections.ImmutableFormulaList;
 import org.logicng.collections.LNGVector;
-import org.logicng.formulas.FType;
 import org.logicng.formulas.Formula;
 import org.logicng.formulas.FormulaFactory;
 import org.logicng.formulas.Literal;
 import org.logicng.formulas.Variable;
 
 import java.util.ArrayList;
-import java.util.Collection;
 import java.util.List;
 
 import static org.logicng.cardinalityconstraints.CCSorting.ImplicationDirection.INPUT_TO_OUTPUT;
@@ -72,38 +69,27 @@
  * @version 1.1
  * @since 1.1
  */
-public final class CCAMKCardinalityNetwork extends CCAtMostK {
+final class CCAMKCardinalityNetwork implements CCAtMostK {
 
   private final FormulaFactory f;
-  private List<Formula> result;
   private final CCSorting sorting;
 
   /**
    * Constructs a new cardinality encoder.
    * @param f the formula factory
    */
-  public CCAMKCardinalityNetwork(final FormulaFactory f) {
+  CCAMKCardinalityNetwork(final FormulaFactory f) {
     this.f = f;
-    this.result = new ArrayList<>();
     this.sorting = new CCSorting(f);
   }
 
   @Override
-  public ImmutableFormulaList build(final Collection<Variable> vars, int rhs) {
-    if (rhs < 0)
-      throw new IllegalArgumentException("Invalid right hand side of cardinality constraint: " + rhs);
-    this.result.clear();
-    if (rhs >= vars.size()) // there is no constraint
-      return new ImmutableFormulaList(FType.AND);
-    if (rhs == 0) { // no variable can be true
-      for (final Variable var : vars)
-        this.result.add(var.negate());
-      return new ImmutableFormulaList(FType.AND, this.result);
-    }
+  public List<Formula> build(final Variable[] vars, int rhs) {
+    List<Formula> result = new ArrayList<>();
     final LNGVector<Literal> input = new LNGVector<>();
     final LNGVector<Literal> output = new LNGVector<>();
-    if (rhs > vars.size() / 2) {
-      int geq = vars.size() - rhs;
+    if (rhs > vars.length / 2) {
+      int geq = vars.length - rhs;
       for (final Variable v : vars)
         input.push(v.negate());
       sorting.sort(geq, input, result, output, OUTPUT_TO_INPUT);
@@ -117,7 +103,7 @@ public ImmutableFormulaList build(final Collection<Variable> vars, int rhs) {
       result.add(f.clause(output.get(rhs).negate()));
     }
 
-    return new ImmutableFormulaList(FType.AND, this.result);
+    return result;
   }
 
   @Override

diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMKModularTotalizer.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMKModularTotalizer.java
@@ -49,25 +49,23 @@
 
 package org.logicng.cardinalityconstraints;
 
-import org.logicng.collections.ImmutableFormulaList;
 import org.logicng.collections.LNGVector;
-import org.logicng.formulas.FType;
 import org.logicng.formulas.Formula;
 import org.logicng.formulas.FormulaFactory;
 import org.logicng.formulas.Literal;
 import org.logicng.formulas.Variable;
 
-import java.util.Collection;
+import java.util.ArrayList;
 import java.util.LinkedList;
 import java.util.List;
 
 /**
  * Encodes that at most 'rhs' variables can be assigned value true.  Uses the modular totalizer encoding for
  * translating the cardinality constraint into CNF.
- * @version 1.0
+ * @version 1.1
  * @since 1.0
  */
-public final class CCAMKModularTotalizer extends CCAtMostK {
+final class CCAMKModularTotalizer implements CCAtMostK {
 
   private final FormulaFactory f;
   private final Variable varUndef;
@@ -84,7 +82,7 @@ public final class CCAMKModularTotalizer extends CCAtMostK {
    * Constructs a new modular totalizer.
    * @param f the formula factory
    */
-  public CCAMKModularTotalizer(final FormulaFactory f) {
+  CCAMKModularTotalizer(final FormulaFactory f) {
     this.f = f;
     this.varUndef = f.variable("RESERVED@VAR_UNDEF");
     this.varError = f.variable("RESERVED@VAR_ERROR");
@@ -93,43 +91,32 @@ public CCAMKModularTotalizer(final FormulaFactory f) {
     this.cardinalityInvars = new LNGVector<>();
     this.cardinalityUpOutvars = new LNGVector<>();
     this.cardinalityLwOutvars = new LNGVector<>();
-    this.result = new LinkedList<>();
   }
 
   @Override
-  public ImmutableFormulaList build(final Collection<Variable> vars, int rhs) {
-    if (rhs < 0)
-      throw new IllegalArgumentException("Invalid right hand side of cardinality constraint: " + rhs);
-    assert !vars.isEmpty();
-    this.result.clear();
+  public List<Formula> build(final Variable[] vars, int rhs) {
+    this.result = new ArrayList<>();
     this.cardinalityUpOutvars.clear();
     this.cardinalityLwOutvars.clear();
-    if (rhs >= vars.size())
-      return new ImmutableFormulaList(FType.AND);
-    if (rhs == 0) {
-      for (final Variable var : vars)
-        this.result.add(var.negate());
-      return new ImmutableFormulaList(FType.AND, this.result);
-    }
-    assert rhs >= 1 && rhs < vars.size();
+    assert rhs >= 1 && rhs < vars.length;
     int mod = (int) Math.ceil(Math.sqrt(rhs + 1.0));
-    this.cardinalityUpOutvars = new LNGVector<>(vars.size() / mod);
-    for (int i = 0; i < vars.size() / mod; i++)
+    this.cardinalityUpOutvars = new LNGVector<>(vars.length / mod);
+    for (int i = 0; i < vars.length / mod; i++)
       this.cardinalityUpOutvars.push(this.f.newCCVariable());
     this.cardinalityLwOutvars = new LNGVector<>(mod - 1);
     for (int i = 0; i < mod - 1; i++)
       this.cardinalityLwOutvars.push(this.f.newCCVariable());
-    this.cardinalityInvars = new LNGVector<>(vars.size());
+    this.cardinalityInvars = new LNGVector<>(vars.length);
     for (final Variable var : vars)
       this.cardinalityInvars.push(var);
     this.currentCardinalityRhs = rhs + 1;
     if (this.cardinalityUpOutvars.size() == 0)
       this.cardinalityUpOutvars.push(this.h0);
-    this.toCNF(mod, this.cardinalityUpOutvars, this.cardinalityLwOutvars, vars.size());
+    this.toCNF(mod, this.cardinalityUpOutvars, this.cardinalityLwOutvars, vars.length);
     assert this.cardinalityInvars.size() == 0;
     this.encodeOutput(rhs, mod);
     this.currentCardinalityRhs = rhs + 1;
-    return new ImmutableFormulaList(FType.AND, this.result);
+    return this.result;
   }
 
   private void encodeOutput(int rhs, int mod) {

diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMKTotalizer.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMKTotalizer.java
@@ -49,32 +49,33 @@
 
 package org.logicng.cardinalityconstraints;
 
-import org.logicng.collections.ImmutableFormulaList;
+import org.logicng.formulas.Formula;
 import org.logicng.formulas.FormulaFactory;
 import org.logicng.formulas.Variable;
 
-import java.util.Collection;
+import java.util.List;
 
 /**
  * Encodes that at most 'rhs' variables can be assigned value true.  Uses the totalizer encoding for
  * translating the cardinality constraint into CNF.
- * @version 1.0
+ * @version 1.1
  * @since 1.0
  */
-public final class CCAMKTotalizer extends CCAtMostK {
+final class CCAMKTotalizer implements CCAtMostK {
 
   private final CCTotalizer totalizer;
 
   /**
    * Constructs a new totalizer.
    * @param f the formula factory
    */
-  public CCAMKTotalizer(final FormulaFactory f) {
+  CCAMKTotalizer(final FormulaFactory f) {
     this.totalizer = new CCTotalizer(f);
   }
 
+
   @Override
-  public ImmutableFormulaList build(final Collection<Variable> vars, int rhs) {
+  public List<Formula> build(final Variable[] vars, int rhs) {
     return this.totalizer.buildAMK(vars, rhs);
   }
 

diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMOBimander.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMOBimander.java
@@ -51,9 +51,7 @@
 
 package org.logicng.cardinalityconstraints;
 
-import org.logicng.collections.ImmutableFormulaList;
 import org.logicng.collections.LNGVector;
-import org.logicng.formulas.FType;
 import org.logicng.formulas.Formula;
 import org.logicng.formulas.FormulaFactory;
 import org.logicng.formulas.Literal;
@@ -67,9 +65,7 @@
  * @version 1.1
  * @since 1.1
  */
-public final class CCAMOBimander extends CCAtMostOne {
-
-  //TODO configuration for group size (half, sqrt, fixed)
+final class CCAMOBimander implements CCAtMostOne {
 
   private final FormulaFactory f;
   private List<Formula> result;
@@ -84,29 +80,18 @@ public final class CCAMOBimander extends CCAtMostOne {
    * Constructs the bimander AMO encoder with a given number of groups.
    * @param f the formula factory
    */
-  public CCAMOBimander(final FormulaFactory f, int m) {
+  CCAMOBimander(final FormulaFactory f, int m) {
     this.f = f;
     this.m = m;
-    this.result = new ArrayList<>();
     this.groups = new LNGVector<>();
     this.bits = new LNGVector<>();
   }
 
-  /**
-   * Constructs the bimander AMO encoder with 3 groups.
-   * @param f the formula factory
-   */
-  public CCAMOBimander(final FormulaFactory f) {
-    this(f, 3);
-  }
-
   @Override
-  public ImmutableFormulaList build(final Variable... vars) {
-    this.result.clear();
-    if (vars.length <= 1)
-      return new ImmutableFormulaList(FType.AND, this.result);
+  public List<Formula> build(final Variable... vars) {
+    this.result = new ArrayList<>();
     this.encodeIntern(new LNGVector<Literal>(vars));
-    return new ImmutableFormulaList(FType.AND, this.result);
+    return this.result;
   }
 
   /**

diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMOBinary.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMOBinary.java
@@ -51,8 +51,6 @@
 
 package org.logicng.cardinalityconstraints;
 
-import org.logicng.collections.ImmutableFormulaList;
-import org.logicng.formulas.FType;
 import org.logicng.formulas.Formula;
 import org.logicng.formulas.FormulaFactory;
 import org.logicng.formulas.Variable;
@@ -66,25 +64,21 @@
  * @version 1.1
  * @since 1.1
  */
-public final class CCAMOBinary extends CCAtMostOne {
+final class CCAMOBinary implements CCAtMostOne {
 
   private final FormulaFactory f;
-  private List<Formula> result;
 
   /**
    * Constructs the binary AMO encoder.
    * @param f the formula factory
    */
-  public CCAMOBinary(final FormulaFactory f) {
+  CCAMOBinary(final FormulaFactory f) {
     this.f = f;
-    this.result = new ArrayList<>();
   }
 
   @Override
-  public ImmutableFormulaList build(final Variable... vars) {
-    this.result.clear();
-    if (vars.length <= 0)
-      return new ImmutableFormulaList(FType.AND, this.result);
+  public List<Formula> build(final Variable... vars) {
+    final List<Formula> result = new ArrayList<>();
     final int numberOfBits = (int) Math.ceil((Math.log(vars.length) / Math.log(2)));
     final int twoPowNBits = (int) Math.pow(2, numberOfBits);
     final int k = (twoPowNBits - vars.length) * 2;
@@ -103,9 +97,9 @@ public ImmutableFormulaList build(final Variable... vars) {
       for (int j = 0; j < numberOfBits; ++j)
         if ((gray_code & (1 << j)) == (next_gray & (1 << j))) {
           if ((gray_code & (1 << j)) != 0)
-            this.result.add(this.f.clause(vars[index].negate(), bits[j]));
+            result.add(this.f.clause(vars[index].negate(), bits[j]));
           else
-            this.result.add(this.f.clause(vars[index].negate(), bits[j].negate()));
+            result.add(this.f.clause(vars[index].negate(), bits[j].negate()));
         }
       i++;
     }
@@ -114,12 +108,12 @@ public ImmutableFormulaList build(final Variable... vars) {
       gray_code = i ^ (i >> 1);
       for (int j = 0; j < numberOfBits; ++j)
         if ((gray_code & (1 << j)) != 0)
-          this.result.add(this.f.clause(vars[index].negate(), bits[j]));
+          result.add(this.f.clause(vars[index].negate(), bits[j]));
         else
-          this.result.add(this.f.clause(vars[index].negate(), bits[j].negate()));
+          result.add(this.f.clause(vars[index].negate(), bits[j].negate()));
       i++;
     }
-    return new ImmutableFormulaList(FType.AND, this.result);
+    return result;
   }
 
   @Override