From: Hamed Gorjiara Date: Thu, 27 Aug 2020 05:19:19 +0000 (-0700) Subject: Supporting at-most-one constraint for One Hot encoding X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=f013286b990f6905d0630f4c5b876baca47a8996;p=satune.git Supporting at-most-one constraint for One Hot encoding --- diff --git a/src/AST/astops.h b/src/AST/astops.h index 04b4c83..0cb308b 100644 --- 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 ed04630..9a698e0 100644 --- 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 11387a8..20683c5 100644 --- 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 1b101e3..5b59f22 100644 --- 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 07a3c72..c23f18d 100644 --- 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 9d45407..a149984 100644 --- 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 22660fb..fc7ef8a 100644 --- 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);