this repo has no description
dekker.one
1#!/usr/bin/env python3
2import os
3import sys
4import time
5import csv
6
7MZNR_HOME = os.getcwd() + "/software/install/minizinc/bin"
8os.environ["PATH"] = MZNR_HOME + ":" + os.environ["PATH"]
9os.environ["MZN_SOLVER_PATH"] = (
10 os.getcwd() + "/software/install/gecode/share/minizinc/solvers"
11)
12import minizinc
13
14MZA_HOME = os.getcwd() + "/software/mza"
15sys.path.append(MZA_HOME)
16
17mza_lib = os.getcwd() + "/software/install/mza/lib"
18if sys.platform == "linux" or sys.platform == "linux2":
19 rerun = True
20 if not "LD_LIBRARY_PATH" in os.environ:
21 os.environ["LD_LIBRARY_PATH"] = mza_lib
22 elif not mza_lib in os.environ.get("LD_LIBRARY_PATH"):
23 os.environ["LD_LIBRARY_PATH"] += ":" + mza_lib
24 else:
25 rerun = False
26 if rerun:
27 os.execve(os.path.realpath(__file__), sys.argv, os.environ)
28
29import mza
30from mza import Instance
31
32mza.DEBUG = False
33
34SOLVER = "gecode_presolver"
35PROTO_MODEL = "gbac/proto.uzn"
36RESTART_MODEL = "gbac/on_restart.mzn"
37DATA = [
38 "gbac/reduced_UD4-gbac.dzn",
39 "gbac/UD2-gbac.dzn",
40 "gbac/UD4-gbac.dzn",
41 "gbac/UD5-gbac.dzn",
42 "gbac/UD8-gbac.dzn",
43]
44FN_ID = "f_lex_obj_i"
45N_NBH = 2
46ROUNDS = 1000
47RUNS = 1
48
49
50def gbac_restart(data_file):
51 os.environ["MZN_STDLIB_DIR"] = (
52 os.getcwd() + "/software/install/minizinc/share/minizinc"
53 )
54 gecode = minizinc.Solver.lookup("gecode")
55 inst = minizinc.Instance(gecode, minizinc.Model(RESTART_MODEL))
56 inst.add_file(data_file)
57
58 args = {
59 "--restart": "constant",
60 "--restart-scale": 500,
61 "--restart-limit": ROUNDS,
62 }
63 res = inst.solve(**args)
64
65 return (
66 res.statistics["flatTime"].total_seconds(),
67 (res.statistics["initTime"] + res.statistics["solveTime"]).total_seconds(),
68 )
69
70
71def gbac_incr(data_file):
72 os.environ["MZN_STDLIB_DIR"] = os.getcwd() + "/software/mza/share/minizinc"
73 compile_time = 0.0
74 solve_time = 0.0
75
76 incumbent = None
77 start = time.perf_counter()
78 mza.set_rnd_seed(0)
79 inst = Instance(PROTO_MODEL, data_file, "gecode_presolver")
80 compile_time += time.perf_counter() - start
81
82 start = time.perf_counter()
83 status, sol = inst.solve()
84 solve_time += time.perf_counter() - start
85 # print(f"{status}: {sol}")
86 assert status in ["SAT", "OPT"]
87 incumbent = sol
88 for i in range(1, ROUNDS):
89 mza.set_rnd_seed(i)
90 inst.set_limit(500)
91 with inst.branch() as child:
92 start = time.perf_counter()
93 child.add_call("f_LNS_i", i % 2)
94 compile_time += time.perf_counter() - start
95
96 start = time.perf_counter()
97 status, sol = child.solve()
98 solve_time += time.perf_counter() - start
99 # print(f"{status}: {sol}")
100 if status == "SAT" or status == "OPT":
101 incumbent = sol
102 assert status != "ERROR"
103 return compile_time, solve_time
104
105
106def gbac_redo(data_file):
107 os.environ["MZN_STDLIB_DIR"] = os.getcwd() + "/software/mza/share/minizinc"
108 compile_time = 0.0
109 solve_time = 0.0
110
111 incumbent = None
112 for i in range(ROUNDS):
113 start = time.perf_counter()
114 mza.set_rnd_seed(i)
115 inst = Instance(PROTO_MODEL, data_file, "gecode_presolver")
116 inst.output_dict(True)
117 limit = 0
118 if i > 0:
119 inst.set_limit(500)
120 assert incumbent is not None
121 limit = 500
122 inst.set_incumbent(incumbent)
123 inst.add_call("f_LNS_i", i % 2)
124 compile_time += time.perf_counter() - start
125
126 start = time.perf_counter()
127 status, sol = inst.solve()
128 solve_time += time.perf_counter() - start
129 # print(
130 # f"{i} {status}: [{ ', '.join([str(v) for k, v in sol.items()]) if isinstance(sol, dict) else sol}]"
131 # )
132 if status == "SAT" or status == "OPT":
133 incumbent = sol
134 elif status == "ERROR":
135 print("ERROR!!!!")
136 exit(0)
137 return compile_time, solve_time
138
139
140if __name__ == "__main__":
141 fieldnames = ["Configuration", "Data", "Compile Time (s)", "Solve Time (s)"]
142 writer = csv.writer(sys.stdout)
143 writer.writerow(fieldnames)
144
145 # --- Run Restart based strategy
146 for d in DATA:
147 t1, t2 = 0, 0
148 for i in range(RUNS):
149 ct, st = gbac_restart(d)
150 t1 += ct
151 t2 += st
152 writer.writerow(["RBS", d, t1 / RUNS, t2 / RUNS])
153 # --- Run incremental rewriting
154 for d in DATA:
155 t1, t2 = 0, 0
156 for i in range(RUNS):
157 ct, st = gbac_incr(d)
158 t1 += ct
159 t2 += st
160 writer.writerow(["Incr.", d, t1 / RUNS, t2 / RUNS])
161 # --- Run baseline
162 for d in DATA:
163 t1, t2 = 0, 0
164 for i in range(RUNS):
165 ct, st = gbac_redo(d)
166 t1 += ct * 10
167 t2 += st * 10
168 writer.writerow(["Base", d, t1 / RUNS, t2 / RUNS])