1)Making naiveencoder and encoding graph use tuner 2)Adding timeout to the sat solver...
[satune.git] / src / Tuner / autotuner.cc
1 #include "autotuner.h"
2 #include "csolver.h"
3 #include "searchtuner.h"
4 #include <math.h>
5 #include <stdlib.h>
6 #include <float.h>
7
8 #define UNSETVALUE -1
9 #define TIMEOUTSEC 60
10 AutoTuner::AutoTuner(uint _budget) :
11         budget(_budget), result(UNSETVALUE) {
12 }
13
14 void AutoTuner::addProblem(CSolver *solver) {
15         solvers.push(solver);
16 }
17
18 long long AutoTuner::evaluate(CSolver *problem, SearchTuner *tuner) {
19         CSolver *copy = problem->clone();
20         copy->setTuner(tuner);
21         copy->setSatSolverTimeout(TIMEOUTSEC);
22         model_print("**********************\n");
23         int sat = copy->solve();
24         if (result == UNSETVALUE && sat != IS_INDETER)
25                 result = sat;
26         else if (result != sat && sat != IS_INDETER) {
27                 model_print("&&&&&&&&&&&&&&&&&& Result has changed &&&&&&&&&&&&&\n");
28                 copy->printConstraints();
29         }
30         long long metric = copy->getElapsedTime();
31         delete copy;
32         return metric;
33 }
34
35 double AutoTuner::evaluateAll(SearchTuner *tuner) {
36         double product = 1;
37         for (uint i = 0; i < solvers.getSize(); i++) {
38                 CSolver *problem = solvers.get(i);
39                 double score = evaluate(problem, tuner);
40                 product *= score;
41         }
42         return pow(product, 1 / ((double)solvers.getSize()));
43 }
44
45 SearchTuner *AutoTuner::mutateTuner(SearchTuner *oldTuner, uint k) {
46         SearchTuner *newTuner = oldTuner->copyUsed();
47         uint numSettings = oldTuner->getSize();
48         uint settingsToMutate = (uint)(AUTOTUNERFACTOR * (((double)numSettings) * (budget - k)) / (budget));
49         if (settingsToMutate < 1)
50                 settingsToMutate = 1;
51         model_print("Mutating %u settings\n", settingsToMutate);
52         while (settingsToMutate-- != 0) {
53                 newTuner->randomMutate();
54         }
55         return newTuner;
56 }
57
58
59 void AutoTuner::tune() {
60         SearchTuner *bestTuner = NULL;
61         double bestScore = DBL_MAX;
62
63         SearchTuner *oldTuner = new SearchTuner();
64         double base_temperature = evaluateAll(oldTuner);
65         double oldScore = base_temperature;
66
67         for (uint i = 0; i < budget; i++) {
68                 SearchTuner *newTuner = mutateTuner(oldTuner, i);
69                 double newScore = evaluateAll(newTuner);
70                 newTuner->printUsed();
71                 model_print("Received score %f\n", newScore);
72                 double scoreDiff = newScore - oldScore; //smaller is better
73                 if (newScore < bestScore) {
74                         if (bestTuner != NULL)
75                                 delete bestTuner;
76                         bestScore = newScore;
77                         bestTuner = newTuner->copyUsed();
78                 }
79
80                 double acceptanceP;
81                 if (scoreDiff < 0) {
82                         acceptanceP = 1;
83                 } else {
84                         double currTemp = base_temperature * (((double)budget - i) / budget);
85                         acceptanceP = exp(-scoreDiff / currTemp);
86                 }
87                 double ran = ((double)random()) / RAND_MAX;
88                 if (ran <= acceptanceP) {
89                         delete oldTuner;
90                         oldScore = newScore;
91                         oldTuner = newTuner;
92                 } else {
93                         delete newTuner;
94                 }
95         }
96         model_print("Best tuner:\n");
97         bestTuner->print();
98         bestTuner->serialize();
99         model_print("Received score %f\n", bestScore);
100         if (bestTuner != NULL)
101                 delete bestTuner;
102         delete oldTuner;
103 }