Update smt

carlo98 · Jul 19, 2021 · c8c55d9 · c8c55d9
1 parent f6f16a9
commit c8c55d9
Showing 1 changed file with 28 additions and 6 deletions.
diff --git a/SMT/Solver_smt.ipynb b/SMT/Solver_smt.ipynb
@@ -2,6 +2,7 @@
  "cells": [
   {
    "cell_type": "markdown",
+   "id": "19870b26",
    "metadata": {},
    "source": [
     "# SMT Solver for VLSI"
@@ -10,6 +11,7 @@
   {
    "cell_type": "code",
    "execution_count": 1,
+   "id": "de772736",
    "metadata": {
     "pycharm": {
      "name": "#%%\n"
@@ -28,6 +30,7 @@
   {
    "cell_type": "code",
    "execution_count": 2,
+   "id": "57a07be3",
    "metadata": {},
    "outputs": [],
    "source": [
@@ -48,6 +51,7 @@
   {
    "cell_type": "code",
    "execution_count": 3,
+   "id": "e736e3f7",
    "metadata": {},
    "outputs": [],
    "source": [
@@ -61,6 +65,7 @@
   {
    "cell_type": "code",
    "execution_count": 4,
+   "id": "c8fca11a",
    "metadata": {},
    "outputs": [],
    "source": [
@@ -90,6 +95,7 @@
   {
    "cell_type": "code",
    "execution_count": 5,
+   "id": "6615e7e8",
    "metadata": {},
    "outputs": [],
    "source": [
@@ -116,9 +122,23 @@
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 6,
+   "id": "ed4c3055",
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "ename": "FileNotFoundError",
+     "evalue": "[Errno 2] No such file or directory: '../instances/ins-16.txt'",
+     "output_type": "error",
+     "traceback": [
+      "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
+      "\u001b[0;31mFileNotFoundError\u001b[0m                         Traceback (most recent call last)",
+      "\u001b[0;32m<ipython-input-6-4d10902f581f>\u001b[0m in \u001b[0;36m<module>\u001b[0;34m\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0mdims\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mW\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mn\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mread_instance\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;36m16\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m      2\u001b[0m \u001b[0;31m# Solver\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m      3\u001b[0m \u001b[0mopt\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mOptimize\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m      4\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m      5\u001b[0m \u001b[0msol\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0;34m[\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0mInt\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"x_%s\"\u001b[0m \u001b[0;34m%\u001b[0m \u001b[0;34m(\u001b[0m\u001b[0mi\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mInt\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"y_%s\"\u001b[0m \u001b[0;34m%\u001b[0m \u001b[0;34m(\u001b[0m\u001b[0mi\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m]\u001b[0m \u001b[0;32mfor\u001b[0m \u001b[0mi\u001b[0m \u001b[0;32min\u001b[0m \u001b[0mrange\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mn\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
+      "\u001b[0;32m<ipython-input-4-fb9f656e29d0>\u001b[0m in \u001b[0;36mread_instance\u001b[0;34m(instance_id)\u001b[0m\n\u001b[1;32m      1\u001b[0m \u001b[0;32mdef\u001b[0m \u001b[0mread_instance\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0minstance_id\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m      2\u001b[0m     \u001b[0mfilepath\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0;34m\"../instances/ins-\"\u001b[0m \u001b[0;34m+\u001b[0m \u001b[0mstr\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0minstance_id\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;34m+\u001b[0m \u001b[0;34m\".txt\"\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m----> 3\u001b[0;31m     \u001b[0;32mwith\u001b[0m \u001b[0mopen\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilepath\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m\"r\"\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;32mas\u001b[0m \u001b[0mf_in\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m      4\u001b[0m         \u001b[0mf\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mf_in\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mreadlines\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m      5\u001b[0m         \u001b[0;32mfor\u001b[0m \u001b[0mi\u001b[0m \u001b[0;32min\u001b[0m \u001b[0mrange\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mlen\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mf\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
+      "\u001b[0;31mFileNotFoundError\u001b[0m: [Errno 2] No such file or directory: '../instances/ins-16.txt'"
+     ]
+    }
+   ],
    "source": [
     "dims, W, n = read_instance(16)\n",
     "# Solver\n",
@@ -144,9 +164,6 @@
     "# height min\n",
     "for i in range(n):\n",
     "    opt.add(sol[i][1] >= 0)\n",
-    "    \n",
-    "# Biggest rectangle in (0, 0)\n",
-    "opt.add(And(sol[0][0] ==0, sol[0][1] ==0))\n",
     "\n",
     "# Symmetry breaking\n",
     "flags = [False for i in range(n)]\n",
@@ -171,6 +188,10 @@
     "            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 <= sum([dims[i][1] for i in range(n)])) # 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",
@@ -194,6 +215,7 @@
   {
    "cell_type": "code",
    "execution_count": null,
+   "id": "4445fb57",
    "metadata": {},
    "outputs": [],
    "source": []
@@ -215,7 +237,7 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.6.9"
+   "version": "3.8.3"
   }
  },
  "nbformat": 4,