bug fix
[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 5000
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 void AutoTuner::tune() {
59         SearchTuner *bestTuner = NULL;
60         double bestScore = DBL_MAX;
61
62         SearchTuner *oldTuner = new SearchTuner();
63         double base_temperature = evaluateAll(oldTuner);
64         double oldScore = base_temperature;
65
66         for (uint i = 0; i < budget; i++) {
67                 SearchTuner *newTuner = mutateTuner(oldTuner, i);
68                 double newScore = evaluateAll(newTuner);
69                 newTuner->printUsed();
70                 model_print("Received score %f\n", newScore);
71                 double scoreDiff = newScore - oldScore; //smaller is better
72                 if (newScore < bestScore) {
73                         if (bestTuner != NULL)
74                                 delete bestTuner;
75                         bestScore = newScore;
76                         bestTuner = newTuner->copyUsed();
77                 }
78
79                 double acceptanceP;
80                 if (scoreDiff < 0) {
81                         acceptanceP = 1;
82                 } else {
83                         double currTemp = base_temperature * (((double)budget - i) / budget);
84                         acceptanceP = exp(-scoreDiff / currTemp);
85                 }
86                 double ran = ((double)random()) / RAND_MAX;
87                 if (ran <= acceptanceP) {
88                         delete oldTuner;
89                         oldScore = newScore;
90                         oldTuner = newTuner;
91                 } else {
92                         delete newTuner;
93                 }
94         }
95         model_print("Best tuner:\n");
96         bestTuner->print();
97         bestTuner->serialize("TUNER.conf");
98         model_print("Received score %f\n", bestScore);
99         if (bestTuner != NULL)
100                 delete bestTuner;
101         delete oldTuner;
102 }