Supporting at-most-one constraint for One Hot encoding

diff --git a/src/AST/astops.h b/src/AST/astops.h
index 04b4c839e034e0bd6017a61dabd61f7deb3cee2b..0cb308b0634617260889bd20155872f75546344f 100644 (file)
--- a/src/AST/astops.h
+++ b/src/AST/astops.h
@@ -28,6 +28,11 @@ typedef enum ElementEncodingType ElementEncodingType;
 enum BooleanVarOrdering {CONSTRAINTORDERING=0, ELEMENTORDERING=1, REVERSEORDERING=2};
 typedef enum BooleanVarOrdering BooleanVarOrdering;
 
+enum AMOOneHot {
+       ONEHOT_BINOMIAL, ONEHOT_COMMANDER, ONEHOT_SEQ_COUNTER 
+};
+typedef enum AMOOneHot AMOOneHot;
+
 Polarity negatePolarity(Polarity This);
 bool impliesPolarity(Polarity curr, Polarity goal);
 

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index ed04630770b73b494faa9bee0d297e3ff2691d49..9a698e0e1f56b7230ac5a4e860b33dc214a5a31a 100644 (file)
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -258,14 +258,112 @@ void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
        }
 }
 
+void SATEncoder::generateOneHotAtMostOne(ElementEncoding *encoding) {
+       if(encoding->numVars <= 1){
+               return;
+       }
+       AMOOneHot enc = (AMOOneHot)solver->getTuner()->getVarTunable(encoding->element->getRange()->getType(), ONEHOTATMOSTONE, &OneHotAtMostOneDesc);
+       switch (enc)
+       {
+       case ONEHOT_BINOMIAL:
+               model_print("Encode using bionomial encoding\n");
+               model_print("size = %u\n", encoding->numVars);
+               generateOneHotBinomialAtMostOne(encoding->variables, encoding->numVars);
+               break;
+       case ONEHOT_COMMANDER:
+               generateOneHotCommanderEncodingVars(encoding);
+               break;
+       case ONEHOT_SEQ_COUNTER:
+               generateOneHotSequentialAtMostOne(encoding);
+               break;
+       default:
+               ASSERT(0);
+               break;
+       }
+}
+
+void SATEncoder::generateOneHotBinomialAtMostOne(Edge *array, uint size, uint offset) {
+       for (uint i = offset; i < offset + size; i++) {
+               for (uint j = i + 1; j < offset + size; j++) {
+                       addConstraintCNF(cnf, constraintNegate(constraintAND2(cnf, array[i], array[j])));
+               }
+       }
+}
+
+void SATEncoder::generateOneHotCommanderAtMostOneRecursive(Edge *array, uint size) {
+       ASSERT(size > 1);
+       if (size <= SEQ_COUNTER_GROUP_SIZE) {
+               //Using binomial encoding
+               generateOneHotBinomialAtMostOne(array, size);
+       } else {
+               Edge commanders[size/SEQ_COUNTER_GROUP_SIZE + 1];
+               uint commanderSize = 0;
+               for(uint index = 0; index < size; index += SEQ_COUNTER_GROUP_SIZE) {
+                       uint groupSize = 0;
+                       if( (index + SEQ_COUNTER_GROUP_SIZE) < size) {
+                               groupSize = SEQ_COUNTER_GROUP_SIZE;
+                       } else {// The last group
+                               groupSize = size - index;
+                       }
+
+                       if(groupSize == 1) {
+                               commanders[commanderSize++] = array[index];
+                       } else {
+                               // 1. binomial encoding for items in the group
+                               generateOneHotBinomialAtMostOne(array, groupSize, index);
+                               // 2. if commander is true at least one item in the group is true
+                               Edge c = getNewVarSATEncoder();
+                               Edge carray[groupSize + 1];
+                               uint carraySize = 0;
+                               carray[carraySize++] = constraintNegate(c);
+                               for(uint i =index; i < index + groupSize; i++ ){
+                                       carray[carraySize++] = array[i];
+                               }
+                               addConstraintCNF(cnf, constraintOR(cnf, carraySize, carray));
+                               // 3. if commander is false, non of the items in the group can be true
+                               for(uint i =index; i < index + groupSize; i++ ){
+                                       addConstraintCNF(cnf, constraintOR2(cnf, constraintNegate(array[i]), c));
+                               }
+                               commanders[commanderSize++] = c;
+                       } 
+               }
+               ASSERT(commanderSize <= (size/SEQ_COUNTER_GROUP_SIZE + 1));
+               if(commanderSize > 1) {
+                       generateOneHotCommanderAtMostOneRecursive(commanders, commanderSize);
+               }
+       }
+}
+
+void SATEncoder::generateOneHotSequentialAtMostOne(ElementEncoding *encoding) {
+       model_print("At-Most-One constraint using sequential counter\n");
+       model_print("size = %u\n", encoding->numVars);
+       // for more information, look at "Towards an Optimal CNF Encoding of Boolean Cardinality Constraints" paper
+       ASSERT(encoding->numVars > 1);
+       Edge *array = encoding->variables;
+       uint size = encoding->numVars;
+       Edge s [size -1 ];
+       getArrayNewVarsSATEncoder(size-1, s);
+       addConstraintCNF(cnf, constraintOR2(cnf, constraintNegate(array[0]), s[0]));
+       addConstraintCNF(cnf, constraintOR2(cnf, constraintNegate(s[size-2]), constraintNegate(array[size-1])));
+       for (uint i=1; i < size -1 ; i++){
+               addConstraintCNF(cnf, constraintOR2(cnf, constraintNegate(array[i]), s[i]));
+               addConstraintCNF(cnf, constraintOR2(cnf, constraintNegate(s[i-1]), s[i]));
+               addConstraintCNF(cnf, constraintOR2(cnf, constraintNegate(array[i]), constraintNegate(s[i-1])));
+       }
+}
+
+void SATEncoder::generateOneHotCommanderEncodingVars(ElementEncoding *encoding) {
+       //For more detail look at paper "Efficient CNF Encoding for Selecting 1 from N Objects"
+       model_print("At-Most-One constraint using commander\n");
+       model_print("size = %u\n", encoding->numVars);
+       ASSERT(encoding->numVars > 1);
+       generateOneHotCommanderAtMostOneRecursive(encoding->variables, encoding->numVars);
+}
+
 void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) {
        allocElementConstraintVariables(encoding, encoding->encArraySize);
        getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
-       for (uint i = 0; i < encoding->numVars; i++) {
-               for (uint j = i + 1; j < encoding->numVars; j++) {
-                       addConstraintCNF(cnf, constraintNegate(constraintAND2(cnf, encoding->variables[i], encoding->variables[j])));
-               }
-       }
+       generateOneHotAtMostOne(encoding);
        if (encoding->element->anyValue)
                addConstraintCNF(cnf, constraintOR(cnf, encoding->numVars, encoding->variables));
 }

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 11387a8b6c937f8e61f9d5e8b03812447df021b7..20683c545bc2ad10263e9a66da33f4d5c8389200 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -38,6 +38,11 @@ private:
        Edge getElementValueBinaryIndexConstraint(Element *element, Polarity p, uint64_t value);
        Edge getElementValueBinaryValueConstraint(Element *element, Polarity p, uint64_t value);
        Edge getElementValueConstraint(Element *element, Polarity p, uint64_t value);
+       void generateOneHotAtMostOne(ElementEncoding *encoding);
+       void generateOneHotBinomialAtMostOne(Edge *array, uint size, uint offset = 0);
+       void generateOneHotCommanderAtMostOneRecursive(Edge *array, uint size);
+       void generateOneHotSequentialAtMostOne(ElementEncoding *encoding);
+       void generateOneHotCommanderEncodingVars(ElementEncoding *encoding);
        void generateOneHotEncodingVars(ElementEncoding *encoding);
        void generateUnaryEncodingVars(ElementEncoding *encoding);
        void generateBinaryIndexEncodingVars(ElementEncoding *encoding);

diff --git a/src/Test/anyvaluetest.cc b/src/Test/anyvaluetest.cc
index 1b101e3f0e9bb1bbd80a4082b0c97ab0a1ec8755..5b59f22664a91933c1035e084f732c27e3f5fd7c 100644 (file)
--- a/src/Test/anyvaluetest.cc
+++ b/src/Test/anyvaluetest.cc
@@ -3,10 +3,10 @@
 
 int main(int numargs, char **argv) {
        CSolver *solver = new CSolver();
-       uint64_t set1[] = {10, 8, 18};
-       uint64_t set2[] = {10, 13, 7};
-       Set *s1 = solver->createSet(0, set1, 3);
-       Set *s2 = solver->createSet(1, set2, 3);
+       uint64_t set1[] = {10, 8, 18, 20, 21, 22, 23, 24, 25, 26};
+       uint64_t set2[] = {10, 13, 7, 30, 31, 32};
+       Set *s1 = solver->createSet(0, set1, 10);
+       Set *s2 = solver->createSet(1, set2, 6);
        Element *e1 = solver->getElementVar(s1);
        Element *e2 = solver->getElementVar(s2);
        solver->mustHaveValue(e1);

diff --git a/src/Test/serializestatictuner.cc b/src/Test/serializestatictuner.cc
index 07a3c7206fcd888f8c8116fcad3ef4d438aa21a7..c23f18d3e374c5ea0dc0ac5a64b028839acbfba1 100644 (file)
--- a/src/Test/serializestatictuner.cc
+++ b/src/Test/serializestatictuner.cc
@@ -38,8 +38,10 @@ int main(int argc, char **argv) {
                elem_onehot->setTunable(NAIVEENCODER, &NaiveEncodingDesc, ONEHOT);
                elem_unary->setTunable(NAIVEENCODER, &NaiveEncodingDesc, UNARY);
                elem_bin->serialize("binarytuner.conf");
-               elem_onehot->serialize("onehottuner.conf");
                elem_unary->serialize("unarytuner.conf");
+               elem_onehot->serialize("onehottuner.conf");
+               elem_onehot->setTunable(ONEHOTATMOSTONE, &OneHotAtMostOneDesc, ONEHOT_COMMANDER);
+               elem_onehot->serialize("onehottunercommander.conf");
                elem_bin->setTunable(ENCODINGGRAPHOPT, &offon, 1);
                elem_onehot->setTunable(ENCODINGGRAPHOPT, &offon, 1);
                elem_unary->setTunable(ENCODINGGRAPHOPT, &offon, 1);

diff --git a/src/Tuner/tunable.cc b/src/Tuner/tunable.cc
index 9d45407a21c2b0dba44409e368fe29ebac298f3a..a149984c17d496ef342149587e1c2fdc623019ac 100644 (file)
--- a/src/Tuner/tunable.cc
+++ b/src/Tuner/tunable.cc
@@ -51,6 +51,8 @@ const char *tunableParameterToString(Tunables tunable) {
                return "MUSTVALUE";
        case VARIABLEORDER:
                return "VARIABLEORDER";
+       case ONEHOTATMOSTONE:
+               return "ONEHOTATMOSTONE";
        default:
                ASSERT(0);
        }

diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h
index 22660fb30c72e29e4cf296b09fa55d78e6761d97..fc7ef8a00624e58c0900b098e114f4eba274d399 100644 (file)
--- a/src/Tuner/tunable.h
+++ b/src/Tuner/tunable.h
@@ -2,6 +2,7 @@
 #define TUNABLE_H
 #include "classlist.h"
 #include "common.h"
+#define SEQ_COUNTER_GROUP_SIZE 3
 
 class Tuner {
 public:
@@ -38,14 +39,15 @@ public:
 
 static TunableDesc onoff(0, 1, 1);
 static TunableDesc offon(0, 1, 0);
-static TunableDesc proxyparameter(1, 5, 2);
+static TunableDesc proxyparameter(1, 5, 1);
 static TunableDesc mustValueBinaryIndex(0, 6, 3);
 static TunableDesc NodeEncodingDesc(ELEM_UNASSIGNED, BINARYINDEX, ELEM_UNASSIGNED);
-static TunableDesc NaiveEncodingDesc(ONEHOT, BINARYINDEX, BINARYINDEX);
+static TunableDesc NaiveEncodingDesc(ONEHOT, BINARYINDEX, ONEHOT);
 static TunableDesc boolVarOrderingDesc(CONSTRAINTORDERING, REVERSEORDERING, REVERSEORDERING);
+static TunableDesc OneHotAtMostOneDesc(ONEHOT_BINOMIAL, ONEHOT_SEQ_COUNTER, ONEHOT_SEQ_COUNTER);
 
 enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT,
-                                                        ENCODINGGRAPHOPT, ELEMENTOPTSETS, PROXYVARIABLE, MUSTVALUE, NAIVEENCODER, VARIABLEORDER};
+                                                        ENCODINGGRAPHOPT, ELEMENTOPTSETS, PROXYVARIABLE, MUSTVALUE, NAIVEENCODER, VARIABLEORDER, ONEHOTATMOSTONE};
 typedef enum Tunables Tunables;
 
 const char *tunableParameterToString(Tunables tunable);