Nested encoding for AMO constraints

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

@@ -0,0 +1,122 @@
+///////////////////////////////////////////////////////////////////////////
+//                   __                _      _   ________               //
+//                  / /   ____  ____ _(_)____/ | / / ____/               //
+//                 / /   / __ \/ __ `/ / ___/  |/ / / __                 //
+//                / /___/ /_/ / /_/ / / /__/ /|  / /_/ /                 //
+//               /_____/\____/\__, /_/\___/_/ |_/\____/                  //
+//                           /____/                                      //
+//                                                                       //
+//               The Next Generation Logic Library                       //
+//                                                                       //
+///////////////////////////////////////////////////////////////////////////
+//                                                                       //
+//  Copyright 2015-2016 Christoph Zengler                                //
+//                                                                       //
+//  Licensed under the Apache License, Version 2.0 (the "License");      //
+//  you may not use this file except in compliance with the License.     //
+//  You may obtain a copy of the License at                              //
+//                                                                       //
+//  http://www.apache.org/licenses/LICENSE-2.0                           //
+//                                                                       //
+//  Unless required by applicable law or agreed to in writing, software  //
+//  distributed under the License is distributed on an "AS IS" BASIS,    //
+//  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or      //
+//  implied.  See the License for the specific language governing        //
+//  permissions and limitations under the License.                       //
+//                                                                       //
+///////////////////////////////////////////////////////////////////////////
+
+/**
+ * PBLib       -- Copyright (c) 2012-2013  Peter Steinke
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a
+ * copy of this software and associated documentation files (the
+ * "Software"), to deal in the Software without restriction, including
+ * without limitation the rights to use, copy, modify, merge, publish,
+ * distribute, sublicense, and/or sell copies of the Software, and to
+ * permit persons to whom the Software is furnished to do so, subject to
+ * the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included
+ * in all copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
+ * OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+ * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+ * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+ * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+ * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+ * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+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.List;
+
+/**
+ * Encodes that at most one variable is assigned value true.  Uses the nested encoding.
+ * @version 1.1
+ * @since 1.1
+ */
+public final class CCAMONested extends CCAtMostOne {
+
+  private final FormulaFactory f;
+  private List<Formula> result;
+
+  /**
+   * Constructs the nested AMO encoder.
+   * @param f the formula factory
+   */
+  public CCAMONested(final FormulaFactory f) {
+    this.f = f;
+    result = new ArrayList<>();
+  }
+
+  @Override
+  public ImmutableFormulaList build(final Variable... vars) {
+    result.clear();
+    if (vars.length <= 0)
+      return new ImmutableFormulaList(FType.AND, result);
+    encodeIntern(new LNGVector<Literal>(vars));
+    return new ImmutableFormulaList(FType.AND, result);
+  }
+
+  /**
+   * Internal recursive encoding.
+   * @param vars the variables of the constraint
+   */
+  private void encodeIntern(final LNGVector<Literal> vars) {
+    if (vars.size() <= 4)
+      for (int i = 0; i + 1 < vars.size(); i++)
+        for (int j = i + 1; j < vars.size(); j++)
+          result.add(f.clause(vars.get(i).negate(), vars.get(j).negate()));
+    else {
+      final LNGVector<Literal> l1 = new LNGVector<>(vars.size() / 2);
+      final LNGVector<Literal> l2 = new LNGVector<>(vars.size() / 2);
+      int i = 0;
+      for (; i < vars.size() / 2; ++i)
+        l1.push(vars.get(i));
+      for (; i < vars.size(); ++i)
+        l2.push(vars.get(i));
+      final Variable newVariable = f.newCCVariable();
+      l1.push(newVariable);
+      l2.push(newVariable.negate());
+      encodeIntern(l1);
+      encodeIntern(l2);
+    }
+  }
+
+  @Override
+  public String toString() {
+    return this.getClass().getSimpleName();
+  }
+}

src/test/java/org/logicng/cardinalityconstraints/CCAMOTest.java

@@ -54,6 +54,7 @@ public class CCAMOTest {
   private static final CCAtMostOne ladder = new CCAMOLadder(f);
   private static final CCAtMostOne product = new CCAMOProduct(f);
   private static final CCAtMostOne binary = new CCAMOBinary(f);
+  private static final CCAtMostOne nested = new CCAMONested(f);
 
 
   @Test
@@ -62,6 +63,7 @@ public void testCC0() {
     Assert.assertTrue(ladder.build(new LinkedList<Variable>()).empty());
     Assert.assertTrue(product.build(new LinkedList<Variable>()).empty());
     Assert.assertTrue(binary.build(new LinkedList<Variable>()).empty());
+    Assert.assertTrue(nested.build(new LinkedList<Variable>()).empty());
   }
 
   @Test
@@ -71,6 +73,7 @@ public void testCC1() {
     Assert.assertTrue(ladder.build(vars).empty());
     Assert.assertTrue(product.build(vars).empty());
     Assert.assertTrue(binary.build(vars).empty());
+    Assert.assertTrue(nested.build(vars).empty());
   }
 
   @Test
@@ -109,6 +112,15 @@ public void testBinary() {
     testCC(500, binary);
   }
 
+  @Test
+  public void testNested() {
+    testCC(2, nested);
+    testCC(10, nested);
+    testCC(100, nested);
+    testCC(250, nested);
+    testCC(500, nested);
+  }
+
   private void testCC(int numLits, final CCAtMostOne encoder) {
     final List<Variable> lits = new LinkedList<>();
     final Variable[] problemLits = new Variable[numLits];