Edits

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index 9a698e0e1f56b7230ac5a4e860b33dc214a5a31a..d70bd9a704edd0d601398467cb7dece7d2898ae5 100644 (file)
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -266,15 +266,13 @@ void SATEncoder::generateOneHotAtMostOne(ElementEncoding *encoding) {
        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);
+               generateOneHotCommanderAtMostOne(encoding->variables, encoding->numVars);
                break;
        case ONEHOT_SEQ_COUNTER:
-               generateOneHotSequentialAtMostOne(encoding);
+               generateOneHotSequentialAtMostOne(encoding->variables, encoding->numVars);
                break;
        default:
                ASSERT(0);
@@ -290,7 +288,8 @@ void SATEncoder::generateOneHotBinomialAtMostOne(Edge *array, uint size, uint of
        }
 }
 
-void SATEncoder::generateOneHotCommanderAtMostOneRecursive(Edge *array, uint size) {
+void SATEncoder::generateOneHotCommanderAtMostOne(Edge *array, uint size) {
+       //For more detail look at paper "Efficient CNF Encoding for Selecting 1 from N Objects"
        ASSERT(size > 1);
        if (size <= SEQ_COUNTER_GROUP_SIZE) {
                //Using binomial encoding
@@ -329,18 +328,14 @@ void SATEncoder::generateOneHotCommanderAtMostOneRecursive(Edge *array, uint siz
                }
                ASSERT(commanderSize <= (size/SEQ_COUNTER_GROUP_SIZE + 1));
                if(commanderSize > 1) {
-                       generateOneHotCommanderAtMostOneRecursive(commanders, commanderSize);
+                       generateOneHotCommanderAtMostOne(commanders, commanderSize);
                }
        }
 }
 
-void SATEncoder::generateOneHotSequentialAtMostOne(ElementEncoding *encoding) {
-       model_print("At-Most-One constraint using sequential counter\n");
-       model_print("size = %u\n", encoding->numVars);
+void SATEncoder::generateOneHotSequentialAtMostOne(Edge *array, uint size) {
        // 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;
+       ASSERT(size > 1);
        Edge s [size -1 ];
        getArrayNewVarsSATEncoder(size-1, s);
        addConstraintCNF(cnf, constraintOR2(cnf, constraintNegate(array[0]), s[0]));
@@ -352,14 +347,6 @@ void SATEncoder::generateOneHotSequentialAtMostOne(ElementEncoding *encoding) {
        }
 }
 
-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);

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 20683c545bc2ad10263e9a66da33f4d5c8389200..5b8af05ac2a2f0cefdbf98fb4530d99ca4176e17 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -40,9 +40,8 @@ private:
        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 generateOneHotCommanderAtMostOne(Edge *array, uint size);
+       void generateOneHotSequentialAtMostOne(Edge *array, uint size);
        void generateOneHotEncodingVars(ElementEncoding *encoding);
        void generateUnaryEncodingVars(ElementEncoding *encoding);
        void generateBinaryIndexEncodingVars(ElementEncoding *encoding);

diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h
index fc7ef8a00624e58c0900b098e114f4eba274d399..46a1412d45be8ff0334aa60e4ea0d8601bacaff4 100644 (file)
--- a/src/Tuner/tunable.h
+++ b/src/Tuner/tunable.h
@@ -44,7 +44,7 @@ static TunableDesc mustValueBinaryIndex(0, 6, 3);
 static TunableDesc NodeEncodingDesc(ELEM_UNASSIGNED, BINARYINDEX, ELEM_UNASSIGNED);
 static TunableDesc NaiveEncodingDesc(ONEHOT, BINARYINDEX, ONEHOT);
 static TunableDesc boolVarOrderingDesc(CONSTRAINTORDERING, REVERSEORDERING, REVERSEORDERING);
-static TunableDesc OneHotAtMostOneDesc(ONEHOT_BINOMIAL, ONEHOT_SEQ_COUNTER, ONEHOT_SEQ_COUNTER);
+static TunableDesc OneHotAtMostOneDesc(ONEHOT_BINOMIAL, ONEHOT_SEQ_COUNTER, ONEHOT_COMMANDER);
 
 enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT,
                                                         ENCODINGGRAPHOPT, ELEMENTOPTSETS, PROXYVARIABLE, MUSTVALUE, NAIVEENCODER, VARIABLEORDER, ONEHOTATMOSTONE};