Fixing the anyvalue heuristic for binaryIndex

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index 2f93d21ea1dac6edbb7533b5a3819ffe1fe57a68..3cd2c1c70b9385e032d7cf4ba99e446f2829f212 100644 (file)
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -7,6 +7,7 @@
 #include "predicate.h"
 #include "csolver.h"
 #include "tunable.h"
 #include "predicate.h"
 #include "csolver.h"
 #include "tunable.h"

+#include <cmath>

 
 void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool &memo) {
        uint numParents = elem->parents.getSize();
 
 void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool &memo) {
        uint numParents = elem->parents.getSize();


@@ -226,7 +227,8 @@ void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
        if (encoding->element->anyValue) {
                uint setSize = encoding->element->getRange()->getSize();
                uint encArraySize = encoding->encArraySize;
        if (encoding->element->anyValue) {
                uint setSize = encoding->element->getRange()->getSize();
                uint encArraySize = encoding->encArraySize;

-               if (setSize < encArraySize * (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex) / 10) {
+               double metric = encArraySize == setSize?setSize:setSize/(encArraySize-setSize);
+               if ( log(metric) <  pow(1.9, (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex) - 4)) {

                        generateAnyValueBinaryIndexEncodingPositive(encoding);
                } else {
                        generateAnyValueBinaryIndexEncoding(encoding);
                        generateAnyValueBinaryIndexEncodingPositive(encoding);
                } else {
                        generateAnyValueBinaryIndexEncoding(encoding);

diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h
index a7ab4e970ca5457ba0da265ec8963321550e141a..22660fb30c72e29e4cf296b09fa55d78e6761d97 100644 (file)
--- a/src/Tuner/tunable.h
+++ b/src/Tuner/tunable.h
@@ -39,9 +39,9 @@ public:
 static TunableDesc onoff(0, 1, 1);
 static TunableDesc offon(0, 1, 0);
 static TunableDesc proxyparameter(1, 5, 2);
 static TunableDesc onoff(0, 1, 1);
 static TunableDesc offon(0, 1, 0);
 static TunableDesc proxyparameter(1, 5, 2);

-static TunableDesc mustValueBinaryIndex(5, 9, 8);
+static TunableDesc mustValueBinaryIndex(0, 6, 3);

 static TunableDesc NodeEncodingDesc(ELEM_UNASSIGNED, BINARYINDEX, ELEM_UNASSIGNED);
 static TunableDesc NodeEncodingDesc(ELEM_UNASSIGNED, BINARYINDEX, ELEM_UNASSIGNED);

-static TunableDesc NaiveEncodingDesc(ONEHOT, BINARYINDEX, ONEHOT);
+static TunableDesc NaiveEncodingDesc(ONEHOT, BINARYINDEX, BINARYINDEX);

 static TunableDesc boolVarOrderingDesc(CONSTRAINTORDERING, REVERSEORDERING, REVERSEORDERING);
 
 enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT,
 static TunableDesc boolVarOrderingDesc(CONSTRAINTORDERING, REVERSEORDERING, REVERSEORDERING);
 
 enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT,