Updated smt, minizinc and results

.gitignore

@@ -1,3 +1,6 @@
 *.dzn
 instances
 .ipynb_checkpoints
+out_2
+out
+out_rotation

Minizinc/VLSI_Solver.py

@@ -21,17 +21,37 @@ def plot_result(result):
 
     plt.xticks(range(w+1))
     plt.yticks(range(max([ys[i]+dims[i][1] for i in range(len(ys))])+1))
-    #plt.grid(b=True, which='major', color='#666666', linestyle='-')
     plt.show()
 
 
+def read_instance(instance_id):
+    filepath = "../instances/ins-" + str(instance_id) + ".txt"
+    with open(filepath, "r") as f_in:
+        f = f_in.readlines()
+        for i in range(len(f)):
+            if not f[i][-1].isnumeric():
+                f[i] = f[i][:-1]
+
+        W = int(f[0])
+        n = int(f[1])
+        dims_line = f[2].split(" ")    
+        dims = [[int(dims_line[0]), int(dims_line[1])]]
+        for i in range(1, int(f[1])-1):
+            dims_line = f[2 + i].split(" ")
+            dims.append([int(dims_line[0]), int(dims_line[1])])
+        dims_line = f[-1].split(" ")
+        dims.append([int(dims_line[0]), int(dims_line[1])])
+
+    return dims, W, n
+
+
 def solve_instance(instance_id):
     # Load model from file
-    model = Model("./model_2.mzn")
-    print("Model 2")
+    model = Model("./model_rotation.mzn")
+    print("Model Rotation")
 
     # Find the MiniZinc solver configuration for Gecode
-    solver = Solver.lookup("chuffed")
+    solver = Solver.lookup("gecode")
 
     # Assign data
     model.add_file("./instances/ins-" + str(instance_id) + ".dzn")
@@ -40,7 +60,6 @@ def solve_instance(instance_id):
     instance = Instance(solver, model)
 
     timeout = datetime.timedelta(seconds=300)
-    #return instance.solve(timeout=timeout, nogood="true")
     return instance.solve(timeout=timeout)
 
 
@@ -50,16 +69,22 @@ def solve_all(max_instance):
     for i in range(1, max_instance+1):
         print("Solving: ", i)
         res = solve_instance(i)
-        #results.append({"obj": res["objective"], "sol": res["sol"], "dims": res["dims_v"], "w": res["w_v"]})
-        #times.append(res.statistics["solveTime"].total_seconds())
         print("\tObj: ", res["objective"])
         print("\tTime: ", res.statistics["solveTime"].total_seconds())
         print("\tFailures: ", res.statistics["failures"])
         print("Solved: ", i)
-
-    #times = np.array(times)
-    #plt.plot(range(1, max_instance+1), times, 'o')
-    #plt.show() 
+
+        dims, W, n = read_instance(i)
+
+        f = open("out_rotation/out-" + str(i) + ".txt", "w")
+        f.write(str(W) + " " + str(res["objective"]) + "\n")
+        f.write(str(n) + "\n")
+        for i in range(n):
+            if i < n-1:
+                f.write(str(dims[i][0]) + " " + str(dims[i][1]) + " " + str(res["sol"][i][0]) + " " + str(res["sol"][i][1]) + "\n")
+            else:
+                f.write(str(dims[i][0]) + " " + str(dims[i][1]) + " " + str(res["sol"][i][0]) + " " + str(res["sol"][i][1]))
+        f.close()
 
 
 if __name__ == "__main__":

Minizinc/model_2.mzn

@@ -2,7 +2,6 @@ include "lex_lesseq.mzn";
 include "cumulative.mzn";
 include "diffn.mzn";
 include "arg_sort.mzn";
-include "gecode.mzn";
 
 %% Inputs
 int: w;  % Width of plate
@@ -39,7 +38,7 @@ constraint cumulative(sol_ver, dim_ver, dim_hor, max_width);  % Cumulative on y
 constraint cumulative(sol_hor, dim_hor, dim_ver, obj);  % Cumulative on x
 
 % Avoid symmetries
-constraint sol_tmp[1, 1] <= 1+(w-dims[per[1], 1])/2 /\ sol_tmp[1, 2] <= 1+(obj-dims[per[1], 2])/2;
+constraint sol_tmp[1, 1] <= 1+(w-dims[per[1], 1])/2 /\ sol_tmp[1, 2] <= 1+(max_height-dims[per[1], 2])/2;
 
 % Not covered by cumulatives
 constraint forall(c in CIRCUITS)(sol_tmp[c, 1] <= max_width - dims[per[c], 1]);  % Constraint on max width
@@ -64,19 +63,14 @@ constraint forall(c in CIRCUITS)(sol[per[c],1] == sol_tmp[c, 1] /\ sol[per[c],2]
 %% Search
 ann: search_ann;
 ann: search_ann1;
-%search_ann = int_search(q, input_order, indomain_min);
-%search_ann = int_search(q, first_fail, indomain_min);
 search_ann = int_search(sol_hor, input_order, indomain_random);
 search_ann1 = int_search(sol_ver, input_order, indomain_random);
-%search_ann = int_search(q, input_order, indomain_random);
-%search_ann = int_search(sol_tmp, dom_w_deg, indomain_min);
 
 %% Solve & output
 solve
   :: search_ann
   :: search_ann1
   :: restart_luby(250) % L = 250
-  %:: relax_and_reconstruct(array1d(sol_ver), 80)
   minimize obj;
 
 output [
@@ -85,4 +79,4 @@ output [
   show(sol_hor),
   show(sol_ver), "\n",
   "Permutation: ", show(per)
-];
+];

Minizinc/model_rotation.mzn

@@ -2,7 +2,6 @@ include "lex_lesseq.mzn";
 include "cumulative.mzn";
 include "diffn.mzn";
 include "arg_sort.mzn";
-%include "gecode.mzn";
 
 %% Inputs
 int: w;  % Width of plate
@@ -13,7 +12,7 @@ array[CIRCUITS, 1..2] of int: dims;  % Dimensions xy for each circuit
 
 % Utilities
 int: max_width = min(w, sum(c in CIRCUITS)(dims[c, 1]));
-int: max_height = sum(c in CIRCUITS)(dims[c, 2]);
+int: max_height = 2*max(max([dims[c, 2] | c in CIRCUITS]), min_height);
 array[CIRCUITS] of float: areas = [1/(dims[c, 1]*dims[c, 2]) | c in CIRCUITS];  % area for each circuit
 array[CIRCUITS] of CIRCUITS: per = arg_sort(areas); % Sorting areas from biggest to smallest
 int: min_height = floor(sum(c in CIRCUITS)(dims[c, 1]*dims[c, 2]) / w); % Minimum height (objective) computed from minimum area
@@ -41,13 +40,13 @@ constraint cumulative(sol_ver, dim_ver, dim_hor, max_width);  % Cumulative on y
 constraint cumulative(sol_hor, dim_hor, dim_ver, obj);  % Cumulative on x
 
 % Implicit
-constraint forall(c in CIRCUITS)(sol_tmp[c, 1] <= max_width - dims_r[per[taken[c]], 1]);  % Implicit constraint on max width
-constraint forall(c in CIRCUITS)(sol_tmp[c, 2] <= max_height - dims_r[per[taken[c]], 2]);  % Implicit constraint on max height
+constraint forall(c in CIRCUITS)(sol_tmp[c, 1] <= max_width - dims_r[per[taken[c]], 1]);  % Constraint on max width
+constraint forall(c in CIRCUITS)(sol_tmp[c, 2] <= max_height - dims_r[per[taken[c]], 2]);  % Constraint on max height
 
 % Equal shape horizontal & vertical
-constraint forall(c1 in CIRCUITS)(lex_lesseq([sol_hor[c2] | c2 in c1..n where [dims[per[c1], 1], dims[per[c1], 2]] == [dims[per[c2], 1], dims[per[c2], 2]]], reverse([sol_hor[c2] | c2 in c1..n where [dims[per[c1], 1], dims[per[c1], 2]] == [dims[per[c2], 1], dims[per[c2], 2]]])));  % horizontal
+constraint forall(c1 in CIRCUITS)(symmetry_breaking_constraint(lex_lesseq([sol_hor[c2] | c2 in c1..n where [dims[per[c1], 1], dims[per[c1], 2]] == [dims[per[c2], 1], dims[per[c2], 2]]], reverse([sol_hor[c2] | c2 in c1..n where [dims[per[c1], 1], dims[per[c1], 2]] == [dims[per[c2], 1], dims[per[c2], 2]]]))));  % horizontal
 
-constraint forall(c1 in CIRCUITS)(lex_lesseq([sol_ver[c2] | c2 in c1..n where [dims[per[c1], 1], dims[per[c1], 2]] == [dims[per[c2], 1], dims[per[c2], 2]]], reverse([sol_ver[c2] | c2 in c1..n where [dims[per[c1], 1], dims[per[c1], 2]] == [dims[per[c2], 1], dims[per[c2], 2]]])));  % vertical
+constraint forall(c1 in CIRCUITS)(symmetry_breaking_constraint(lex_lesseq([sol_ver[c2] | c2 in c1..n where [dims[per[c1], 1], dims[per[c1], 2]] == [dims[per[c2], 1], dims[per[c2], 2]]], reverse([sol_ver[c2] | c2 in c1..n where [dims[per[c1], 1], dims[per[c1], 2]] == [dims[per[c2], 1], dims[per[c2], 2]]]))));  % vertical
 
 constraint forall(c1, c2 in CIRCUITS where c1 <= c2 /\ dims[per[c1], 1] == dims[per[c2], 1])(symmetry_breaking_constraint(sol_hor[c1]==sol_hor[c2] -> sol_ver[c1,]<=sol_ver[c2]));  % horizontal
 
@@ -67,19 +66,14 @@ constraint forall(c in CIRCUITS)(sol_tmp[c, 1] = sol_r[taken[c], 1] /\ sol_tmp[c
 %% Search
 ann: search_ann;
 ann: search_ann1;
-%search_ann = int_search(q, input_order, indomain_min);
-%search_ann = int_search(q, first_fail, indomain_min);
-search_ann = int_search(sol_hor, input_order, indomain_min);
-search_ann1 = int_search(sol_ver, input_order, indomain_min);
-%search_ann = int_search(q, input_order, indomain_random);
-%search_ann = int_search(sol_tmp, dom_w_deg, indomain_random);
+search_ann = int_search(sol_hor, input_order, indomain_random);
+search_ann1 = int_search(sol_ver, input_order, indomain_random);
 
 %% Solve & output
 solve
   :: search_ann
   :: search_ann1
   :: restart_luby(250) % L = 250
-  %:: relax_and_reconstruct(array1d(sol_tmp), 45)
   minimize obj;
 
 output [

SMT/Solver_smt.ipynb

@@ -118,78 +118,129 @@
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "Solving time (s):  0.009374141693115234\n",
+      "Solving time (s):  0.014328718185424805\n",
+      "Solving time (s):  0.024621009826660156\n",
+      "Solving time (s):  0.028209209442138672\n",
+      "Solving time (s):  0.07618522644042969\n",
+      "Solving time (s):  0.15516924858093262\n",
+      "Solving time (s):  0.15819120407104492\n",
+      "Solving time (s):  0.3341343402862549\n",
+      "Solving time (s):  0.3040497303009033\n",
+      "Solving time (s):  0.8251326084136963\n",
+      "Solving time (s):  300.07866168022156\n",
+      "Solving time (s):  3.523998737335205\n",
+      "Solving time (s):  2.9443681240081787\n",
+      "Solving time (s):  8.441926002502441\n",
+      "Solving time (s):  5.417858123779297\n",
+      "Solving time (s):  300.080806016922\n",
+      "Solving time (s):  43.99270558357239\n",
+      "Solving time (s):  111.48133659362793\n",
+      "Solving time (s):  300.0904107093811\n",
+      "Solving time (s):  300.0841541290283\n",
+      "Solving time (s):  292.5991497039795\n",
+      "Solving time (s):  300.09914469718933\n",
+      "Solving time (s):  187.03631019592285\n",
+      "Solving time (s):  57.761428356170654\n",
+      "Solving time (s):  300.11377573013306\n",
+      "Solving time (s):  300.1019456386566\n",
+      "Solving time (s):  127.26807236671448\n",
+      "Solving time (s):  300.0920970439911\n",
+      "Solving time (s):  300.0991711616516\n",
+      "Solving time (s):  300.1152501106262\n",
+      "Solving time (s):  44.87674117088318\n"
+     ]
+    }
+   ],
    "source": [
-    "dims, W, n = read_instance(11)\n",
-    "# Solver\n",
-    "opt = Optimize()\n",
-    "\n",
-    "sol = [[Int(\"x_%s\" % (i)), Int(\"y_%s\" % (i))] for i in range(n)]\n",
-    "\n",
-    "# overlapping\n",
-    "for i in range(n):\n",
-    "    for j in range(n):\n",
-    "        if i != j:\n",
-    "            opt.add(Or(sol[i][0] + dims[i][0] <= sol[j][0],\n",
-    "                       sol[j][0] + dims[j][0] <= sol[i][0],\n",
-    "                       sol[i][1] + dims[i][1] <= sol[j][1],\n",
-    "                       sol[j][1] + dims[j][1] <= sol[i][1]))\n",
-    "\n",
-    "# width\n",
-    "for i in range(n):\n",
-    "    opt.add(sol[i][0] + dims[i][0] <= W)\n",
-    "    opt.add(sol[i][0] >= 0) # min\n",
-    "    opt.add(sol[i][0] <= W - min([dims[i][0] for i in range(n)])) # max\n",
-    "    \n",
-    "# height min\n",
-    "for i in range(n):\n",
-    "    opt.add(sol[i][1] >= 0)\n",
-    "\n",
-    "# Symmetry breaking\n",
-    "flags = [False for i in range(n)]\n",
-    "for i in range(n):\n",
-    "    equal_hor = []\n",
-    "    equal_ver = []\n",
-    "    for j in range(n):\n",
-    "        if i<=j and dims[i][0] == dims[j][0] and dims[i][1] == dims[j][1] and not flags[j]:\n",
-    "            equal_hor.append(sol[j][0])\n",
-    "            flags[j] = True\n",
-    "            equal_ver.append(sol[j][1])\n",
-    "            \n",
-    "    if len(equal_hor) > 1:\n",
-    "        opt = alphaMEncoding(opt, equal_hor, [equal_hor[len(equal_hor)-1-k] for k in range(len(equal_hor))])\n",
-    "        opt = alphaMEncoding(opt, equal_ver, [equal_ver[len(equal_ver)-1-k] for k in range(len(equal_ver))])\n",
-    "    \n",
-    "for i in range(n):\n",
-    "    for j in range(n):\n",
-    "        if i<j and dims[i][0] == dims[j][0]:\n",
-    "            opt.add(Implies(sol[i][0]==sol[j][0], sol[i][1]<=sol[j][1]))\n",
-    "        if i<j and dims[i][1] == dims[j][1]:\n",
-    "            opt.add(Implies(sol[i][1]==sol[j][1], sol[i][0]<=sol[j][0]))\n",
-    "\n",
-    "height_opt = Int('height_opt')\n",
-    "\n",
-    "# Biggest rectangle\n",
-    "opt.add(And(sol[0][0] <= 1+(W-dims[0][0])/2, sol[0][1] <= 1+(height_opt-dims[0][1])/2))\n",
-    "\n",
-    "opt.add(height_opt <= 2*max(max([dims[i][1] for i in range(n)]), min_height)) # upper bound\n",
-    "opt.add(height_opt >= int(sum([dims[i][1]*dims[i][0] for i in range(n)])/W)) # lower bound\n",
-    "objective = height_opt == max_z3([sol[i][1] + dims[i][1] for i in range(n)])\n",
-    "opt.add(objective)\n",
-    "opt.minimize(height_opt)\n",
-    "\n",
-    "start_time = time.time()\n",
-    "opt.check()\n",
-    "m = opt.model()\n",
-    "print(\"Solving time (s): \", time.time()-start_time)\n",
-    "\n",
-    "ys = []\n",
-    "xs = []\n",
-    "for i in range(n):\n",
-    "    xs.append(int(m.evaluate(sol[i][0]).as_string()))\n",
-    "    ys.append(int(m.evaluate(sol[i][1]).as_string()))\n",
+    "for instance_m in range(1, 41): \n",
+    "    dims, W, n = read_instance(instance_m)\n",
+    "    # Solver\n",
+    "    opt = Optimize()\n",
+    "\n",
+    "    sol = [[Int(\"x_%s\" % (i)), Int(\"y_%s\" % (i))] for i in range(n)]\n",
+    "\n",
+    "    # overlapping\n",
+    "    for i in range(n):\n",
+    "        for j in range(n):\n",
+    "            if i != j:\n",
+    "                opt.add(Or(sol[i][0] + dims[i][0] <= sol[j][0],\n",
+    "                           sol[j][0] + dims[j][0] <= sol[i][0],\n",
+    "                           sol[i][1] + dims[i][1] <= sol[j][1],\n",
+    "                           sol[j][1] + dims[j][1] <= sol[i][1]))\n",
+    "\n",
+    "    # width\n",
+    "    for i in range(n):\n",
+    "        opt.add(sol[i][0] + dims[i][0] <= W)\n",
+    "        opt.add(sol[i][0] >= 0) # min\n",
+    "        opt.add(sol[i][0] <= W - min([dims[i][0] for i in range(n)])) # max\n",
+    "\n",
+    "    # height min\n",
+    "    for i in range(n):\n",
+    "        opt.add(sol[i][1] >= 0)\n",
+    "\n",
+    "    # Symmetry breaking\n",
+    "    #flags = [False for i in range(n)]\n",
+    "    #for i in range(n):\n",
+    "    #    equal_hor = []\n",
+    "    #    equal_ver = []\n",
+    "    #    for j in range(n):\n",
+    "    #        if i<=j and dims[i][0] == dims[j][0] and dims[i][1] == dims[j][1] and not flags[j]:\n",
+    "    #            equal_hor.append(sol[j][0])\n",
+    "    #            flags[j] = True\n",
+    "    #            equal_ver.append(sol[j][1])\n",
+    "\n",
+    "    #    if len(equal_hor) > 1:\n",
+    "    #        opt = alphaMEncoding(opt, equal_hor, [equal_hor[len(equal_hor)-1-k] for k in range(len(equal_hor))])\n",
+    "    #        opt = alphaMEncoding(opt, equal_ver, [equal_ver[len(equal_ver)-1-k] for k in range(len(equal_ver))])\n",
+    "\n",
+    "    for i in range(n):\n",
+    "        for j in range(n):\n",
+    "            if i<j and dims[i][0] == dims[j][0]:\n",
+    "                opt.add(Implies(sol[i][0]==sol[j][0], sol[i][1]<=sol[j][1]))\n",
+    "            if i<j and dims[i][1] == dims[j][1]:\n",
+    "                opt.add(Implies(sol[i][1]==sol[j][1], sol[i][0]<=sol[j][0]))\n",
+    "\n",
+    "    height_opt = Int('height_opt')\n",
+    "\n",
+    "    # Biggest rectangle\n",
+    "    opt.add(And(sol[0][0] <= 1+(W-dims[0][0])/2, sol[0][1] <= 1+(height_opt-dims[0][1])/2))\n",
+    "\n",
+    "    min_height = int(sum([dims[i][1]*dims[i][0] for i in range(n)])/W)\n",
+    "\n",
+    "    opt.add(height_opt <= 2*max(max([dims[i][1] for i in range(n)]), min_height)) # upper bound\n",
+    "    opt.add(height_opt >= min_height) # lower bound\n",
+    "    objective = height_opt == max_z3([sol[i][1] + dims[i][1] for i in range(n)])\n",
+    "    opt.add(objective)\n",
+    "    opt.minimize(height_opt)\n",
     "    \n",
-    "plot_result(dims, W, ys, xs)"
+    "    opt.set(\"timeout\", 300*1000)  # 5 minutes timeout\n",
+    "\n",
+    "    start_time = time.time()\n",
+    "    opt.check()\n",
+    "    m = opt.model()\n",
+    "    print(\"Solving time (s): \", time.time()-start_time)\n",
+    "\n",
+    "    ys = []\n",
+    "    xs = []\n",
+    "    for i in range(n):\n",
+    "        xs.append(int(m.evaluate(sol[i][0]).as_string()))\n",
+    "        ys.append(int(m.evaluate(sol[i][1]).as_string()))\n",
+    "\n",
+    "    f = open(\"out/out-\" + str(instance_m) + \".txt\", \"w\")\n",
+    "    f.write(str(W) + \" \" + m.evaluate(height_opt).as_string() + \"\\n\")\n",
+    "    f.write(str(n) + \"\\n\")\n",
+    "    for i in range(n):\n",
+    "        if i < n-1:\n",
+    "            f.write(str(dims[i][0]) + \" \" + str(dims[i][1]) + \" \" + m.evaluate(sol[i][0]).as_string() + \" \" + m.evaluate(sol[i][1]).as_string() + \"\\n\")\n",
+    "        else:\n",
+    "            f.write(str(dims[i][0]) + \" \" + str(dims[i][1]) + \" \" + m.evaluate(sol[i][0]).as_string() + \" \" + m.evaluate(sol[i][1]).as_string())\n",
+    "    f.close()"
    ]
   },
   {