Merge branch 'TACAS2021' of https://github.com/nikhilpim/medley_tool …

…into TACAS2021

medleysolver/classifiers.py

@@ -1,43 +1,52 @@
 import numpy as np, random, dill
 from collections import OrderedDict
 from sklearn.neural_network import MLPClassifier
-from medleysolver.constants import SOLVERS, is_solved
+from medleysolver.constants import SOLVERS, is_solved, ERROR_RESULT
 from medleysolver.distributions import ThompsonDist
 from more_itertools import unique_everseen
+from medleysolver.dispatch import output2result
+
+import csv 
 
 class ClassifierInterface(object):
-    def get_ordering(self, point, count):
+    def __init__(self, time_k):
+        self.time_k = time_k
+        self.solved = []
+
+    def get_ordering(self, point, count, problem):
         raise NotImplementedError
 
     def get_nearby_times(self, point, count):
-        return []
+        positions = sorted(self.solved, key=lambda entry: np.linalg.norm(entry.datapoint - point))[:self.time_k]
+        positions = [(x.solve_method, x.time) for x in positions]
+        return positions
 
     def update(self, solved_prob, rewards):
-        raise NotImplementedError
+        #TODO: Implement pruning
+        if is_solved(solved_prob.result):
+            self.solved.append(solved_prob)
 
     def save(self, filename):
         with open(filename, "wb") as f:
             dill.dump(self, f)
 
 class Random(ClassifierInterface):
-    def get_ordering(self, point, count):
+    def get_ordering(self, point, count, problem):
         order = list(SOLVERS.keys())
         np.random.shuffle(order)
         return order
 
-    def update(self, solved_prob, rewards):
-        return
-
 
 class NearestNeighbor(ClassifierInterface):
-    def __init__(self, epsilon, decay, kind):
+    def __init__(self, epsilon, decay, kind, time_k):
         self.solved = []
         self.epsilon = epsilon
         self.decay = decay
         self.counter = 0
         self.kind = kind
+        super(NearestNeighbor, self).__init__(time_k)
 
-    def get_ordering(self, point, count):
+    def get_ordering(self, point, count, problem):
         if self.kind == "greedy":
             if np.random.rand() >= self.epsilon * (self.decay ** count) and self.solved:
                 #first sort based on distance to inputted point
@@ -50,7 +59,7 @@ def get_ordering(self, point, count):
                 random.shuffle(remaining)
                 order = order + remaining
             else:
-                order = Random.get_ordering(self, point, count)
+                order = Random.get_ordering(self, point, count, problem)
         elif self.kind == "single":
             if np.random.rand() >= self.epsilon * (self.decay ** count) and self.solved:
                 #first sort based on distance to inputted point
@@ -60,7 +69,7 @@ def get_ordering(self, point, count):
                 random.shuffle(remaining)
                 order = order + remaining
             else:
-                order = Random.get_ordering(self, point, count)
+                order = Random.get_ordering(self, point, count, problem)
         else:
             candidate = sorted(self.solved, key=lambda entry: np.linalg.norm(entry.datapoint - point))
             order = list(OrderedDict((x.solve_method, True) for x in candidate).keys())
@@ -69,19 +78,16 @@ def get_ordering(self, point, count):
             order = order + remaining
 
         return list(unique_everseen(order))
-
-    def update(self, solved_prob, rewards):
-        #TODO: Implement pruning
-        if is_solved(solved_prob.result):
-            self.solved.append(solved_prob)
+
 
 class Exp3(ClassifierInterface):
-    def __init__(self, gamma):
+    def __init__(self, gamma, time_k):
         self.gamma = gamma
         self.w = [1 for _ in SOLVERS]
         self.p = [0 for _ in SOLVERS]
+        super(Exp3, self).__init__(time_k)
 
-    def get_ordering(self, point, count):
+    def get_ordering(self, point, count, problem):
         for i, _ in enumerate(SOLVERS):
             self.p[i] = (1-self.gamma) * self.w[i] / sum(self.w) + self.gamma / len(SOLVERS)
 
@@ -94,12 +100,17 @@ def update(self, solved_prob, rewards):
                 reward = reward / self.p[i]
                 self.w[i] = self.w[i] * np.exp(self.gamma * reward / len(SOLVERS))
 
+        #TODO: Implement pruning
+        if is_solved(solved_prob.result):
+            self.solved.append(solved_prob)
+
 class MLP(ClassifierInterface):
-    def __init__(self):
+    def __init__(self, time_k):
         self.clf = MLPClassifier()
         self.fitted = False
+        super(MLP, self).__init__(time_k)
 
-    def get_ordering(self, point, count):
+    def get_ordering(self, point, count, problem):
         point = np.array(point).reshape(1, -1)
         if self.fitted:
             scores = self.clf.predict_proba(point)
@@ -122,12 +133,17 @@ def update(self, solved_prob, rewards):
             self.clf.partial_fit(X, y, classes=np.unique(list(range(len(SOLVERS)))))
         self.fitted = True
 
+        #TODO: Implement pruning
+        if is_solved(solved_prob.result):
+            self.solved.append(solved_prob)
+
 class Thompson(ClassifierInterface):
-    def __init__(self, kind):
+    def __init__(self, kind, time_k):
         self.dist = ThompsonDist(len(SOLVERS))
         self.kind = kind
+        super(Thompson, self).__init__(time_k)
 
-    def get_ordering(self, point, count):
+    def get_ordering(self, point, count, problem):
         if self.kind == "single":
             t_order = self.dist.get_ordering()
             order = [[list(SOLVERS.keys())[int(choice)] for choice in t_order][0]]
@@ -147,11 +163,14 @@ def update(self, solved_prob, rewards):
                 self.dist.update(i, 0)
             else:
                 pass
+        if is_solved(solved_prob.result):
+            self.solved.append(solved_prob)
 
 class LinearBandit(ClassifierInterface):
-    def __init__(self, alpha=2.358):
+    def __init__(self, time_k, alpha=2.358):
         self.initialized = False
         self.alpha = alpha
+        super(LinearBandit, self).__init__(time_k)
 
     def initialize(self, d):
         self.A_0 = np.identity(d)
@@ -160,7 +179,7 @@ def initialize(self, d):
         self.Bs = [np.zeros((d, 1)) for _ in SOLVERS]
         self.Cs = [np.zeros((d, d)) for _ in SOLVERS]
 
-    def get_ordering(self, point, count):
+    def get_ordering(self, point, count, problem):
         if not self.initialized:
             self.initialize(len(point))
         point = point.reshape((len(point), 1))
@@ -191,43 +210,64 @@ def update(self, solved_prob, rewards):
                 self.A_0 += point @ point.T - self.Cs[i].T @ np.linalg.inv(self.As[i]) @ self.Cs[i]
                 self.B_0 += r * point - self.Cs[i].T @ np.linalg.inv(self.As[i]) @ self.Bs[i]
 
+        #TODO: Implement pruning
+        if is_solved(solved_prob.result):
+            self.solved.append(solved_prob)
+
 
 class Preset(ClassifierInterface):
     def __init__(self, solver):
         self.solver = solver
 
-    def get_ordering(self, point, count):
+    def get_ordering(self, point, count, problem):
         return [self.solver]
 
     def update(self, solved_prob, rewards):
         pass
 
+class PerfectSelector(ClassifierInterface):
+
+    def get_ordering(self, point, count, problem):
+
+        instance = problem.split("/")[-1]
+        directory = problem[:-len(instance)]
+
+        time_solver = {s:60 for s in SOLVERS}
+
+        for solver in SOLVERS:
+            try:
+                with open(directory+"/"+solver+".csv") as csvfile:
+                    results = list(csv.reader(csvfile))
+                    results = list(filter(lambda s: s[0] == problem, results))
+                    assert(len(results) == 1)
+                    output = results[0][4]
+                    output = output2result(problem, output)
+                    elapsed = float(results[0][3])
+            except:
+                output   = ERROR_RESULT,
+                elapsed  = 60
+
+            time_solver[solver] = elapsed if output != ERROR_RESULT else 60
+
+        sorted_solvers = sorted(time_solver.keys(), key=lambda x: time_solver[x])
+        return sorted_solvers
+
 class KNearest(ClassifierInterface):
     def __init__(self, k, epsilon, decay, time_k):
         self.k = k
-        self.time_k = time_k
         self.epsilon = epsilon
         self.decay = decay
         self.solved = []
         self.counter = 0
+        super(KNearest, self).__init__(time_k)
 
-    def get_nearby_times(self, point, count):
-        positions = sorted(self.solved, key=lambda entry: np.linalg.norm(entry.datapoint - point))[:self.time_k]
-        positions = [(x.solve_method, x.time) for x in positions]
-        return positions
-
-    def get_ordering(self, point, count):
+    def get_ordering(self, point, count, problem):
         if np.random.rand() >= self.epsilon * (self.decay ** count) and self.solved:
             candidates = sorted(self.solved, key=lambda entry: np.linalg.norm(entry.datapoint - point))[:self.k]
             methods = [x.solve_method for x in candidates]
             ss = list(SOLVERS.keys())
             np.random.shuffle(ss)
             order = sorted(ss, key= lambda x: -1 * methods.count(x))
         else:
-            order = Random.get_ordering(self, point, count)
-        return order
-
-    def update(self, solved_prob, rewards):
-        #TODO: Implement pruning
-        if is_solved(solved_prob.result):
-            self.solved.append(solved_prob)
+            order = Random.get_ordering(self, point, count, problem)
+        return order

medleysolver/runner.py

@@ -17,7 +17,7 @@ def execute(problems, output, classifier, time_manager, timeout, feature_setting
         mean = (c - 1) / c * mean + 1 / c * point
         point = point / (mean+1e-9)
 
-        order = classifier.get_ordering(point, c)
+        order = classifier.get_ordering(point, c, prob)
         times = classifier.get_nearby_times(point, c)
         end = time.time()
 
@@ -35,7 +35,7 @@ def apply_ordering(problem, order, timeout, time_manager, extra_time_to_first, t
     time_spent = []
     timeout = int(timeout)
 
-    budgets = [int(time_manager.get_timeout(solver, times, point))+1 for solver in order]
+    budgets = [int(time_manager.get_timeout(solver, times, problem, point))+1 for solver in order]
 
     for i in range(len(budgets)):
         budgets[i] = min(budgets[i], max(0, int(timeout - sum(budgets[:i]))))

medleysolver/timers.py

@@ -1,9 +1,12 @@
 from medleysolver.distributions import ExponentialDist
-from medleysolver.constants import SOLVERS
+from medleysolver.constants import SOLVERS, ERROR_RESULT, SAT_RESULT, UNSAT_RESULT
 from sklearn.linear_model import SGDRegressor
+from medleysolver.dispatch import output2result
+
+import csv
 
 class TimerInterface(object):
-    def get_timeout(self, solver, times, point):
+    def get_timeout(self, solver, position, problem, point):
         raise NotImplementedError
 
     def update(self, solver, time, success, error, point):
@@ -13,7 +16,7 @@ class Constant(TimerInterface):
     def __init__(self, const):
         self.const = const
 
-    def get_timeout(self, solver, times, point):
+    def get_timeout(self, solver, position, problem, point):
         return self.const
 
     def update(self, solver, time, timeout, success, error, point):
@@ -23,7 +26,7 @@ class Exponential(TimerInterface):
     def __init__(self, init_lambda, confidence, T):
         self.timers = {solver:ExponentialDist(init_lambda, confidence, T) for solver in SOLVERS}
 
-    def get_timeout(self, solver, times, point):
+    def get_timeout(self, solver, position, problem, point):
         return self.timers[solver].get_cutoff()
 
     def update(self, solver, time, timeout, success, error, point):
@@ -41,8 +44,11 @@ def __init__(self, init_lambda, confidence, T):
         self.init_lambda = init_lambda
         self.confidence = confidence
         self.T = T
+        self.naughtylist = set()
 
-    def get_timeout(self, solver, times, point):
+    def get_timeout(self, solver, times, problem, point):
+        if solver in self.naughtylist:
+            return 0
         # want time based on times for same solver at nearby points
         timer = ExponentialDist(self.init_lambda, self.confidence, self.T)
         for (s, t) in times:
@@ -51,14 +57,16 @@ def get_timeout(self, solver, times, point):
         return timer.get_cutoff()
 
     def update(self, solver, time, timeout, success, error, point):
-        pass
+        assert(not success or not error)
+        if error:
+            self.naughtylist.add(solver)
 
 class SGD(TimerInterface):
     def __init__(self, init_lambda, confidence, T):
         self.fitted = [False for _ in SOLVERS]
         self.models = [SGDRegressor() for _ in SOLVERS]
 
-    def get_timeout(self, solver, times, point):
+    def get_timeout(self, solver, times, problem, point):
         if not self.fitted[solver]: return 60
         clf = self.models[solver]
         return clf.predict(point)
@@ -69,4 +77,26 @@ def update(self, solver, time, timeout, success, error, point):
             clf.partial_fit(point, time)
         else:
             clf.fit(point, time)
-
+
+class PerfectTimer(TimerInterface):
+    def get_timeout(self, solver, position, problem, point):
+        instance = problem.split("/")[-1]
+        directory = problem[:-len(instance)]
+        try:
+            with open(directory+"/"+solver+".csv") as csvfile:
+                results = list(csv.reader(csvfile))
+                results = list(filter(lambda s: s[0] == problem, results))
+                assert(len(results) == 1)
+                output = results[0][4]
+                output = output2result(problem, output)
+                elapsed = float(results[0][3])
+        except:
+            output   = ERROR_RESULT,
+            elapsed  = 0
+
+        time = elapsed+1 if output == SAT_RESULT or output == UNSAT_RESULT else 0
+
+        return time
+
+    def update(self, solver, time, timeout, success, error):
+        pass