Optimal_Sudoku_SAT_encoding.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "f0dd02cb-249b-475d-b574-3c6ae86f939f",
   "metadata": {},
   "source": [
    "# HW 5 Sudoku SAT\n",
    "In this homework, you are to build a sat-based Sudoku solver for $n^2xn^2$ problems."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "fde3ed9e-76cb-4a12-9590-a43afd683ae1",
   "metadata": {},
   "source": [
    "To get you started (and verify function) here are some Sudoku puzzles, 0 is use to indicate a settable square. (Remember, in Sudoko, you need to enter digits at every 0 location so that only one of the values is present on a row or column or in the 3x3 subgrind (for 9x9a)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "e05fa644-fd69-4ceb-9d0d-a4da8b0fb951",
   "metadata": {},
   "outputs": [],
   "source": [
    "# get the sat solver...\n",
    "import pycosat"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "6e734937-bdd5-4a39-9355-1d5561757e64",
   "metadata": {},
   "outputs": [],
   "source": [
    "s1 = [[0,0,2,0,0,4,0,0,1],\n",
    "      [0,5,0,0,3,0,0,9,0],\n",
    "      [3,0,0,8,0,0,5,0,0],\n",
    "      [4,0,0,1,0,0,7,0,0],\n",
    "      [0,1,0,0,8,0,0,5,0],\n",
    "      [0,0,8,0,0,7,0,0,9],\n",
    "      [0,0,9,0,0,2,0,0,7],\n",
    "      [0,3,0,0,4,0,0,6,0],\n",
    "      [8,0,0,9,0,0,1,0,0]]\n",
    "s2 = [[0, 0, 0, 2],\n",
    "      [0, 0, 3, 0],\n",
    "      [0, 2, 0, 3],\n",
    "      [0, 1, 0, 0]]\n",
    "s3 = [[0,0,0,16,14,17,0,0,0,0,0,10,0,11,24,0,0,0,2,0,0,0,0,0,0],\n",
    "      [0,6,0,0,0,0,0,0,16,0,0,0,0,0,18,21,0,0,0,0,0,0,7,0,0],\n",
    "      [0,0,0,0,0,0,0,0,25,12,0,0,0,0,0,0,15,0,0,0,0,0,0,11,0],\n",
    "      [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,3,0,0,0,0,0,0,20,0,18],\n",
    "      [0,0,0,0,0,0,21,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],\n",
    "      \n",
    "      [0,0,0,0,0,18,17,0,20,5,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],      \n",
    "      [0,0,0,0,25,0,0,0,0,16,0,0,15,0,0,24,21,10,0,0,22,0,0,0,0],\n",
    "      [0,0,0,0,0,12,0,6,0,0,0,0,0,0,16,0,0,15,0,0,0,0,0,23,0],\n",
    "      [0,0,0,0,0,0,22,0,0,0,0,0,0,0,0,0,3,0,0,0,18,17,0,0,5],\n",
    "      [0,0,17,0,0,0,0,0,0,0,0,22,0,8,7,0,0,0,0,0,14,0,9,0,16],\n",
    "      \n",
    "      [0,14,0,0,0,5,18,0,0,0,11,0,0,10,0,0,0,4,8,7,0,1,0,0,0],\n",
    "      [25,0,1,0,0,16,0,0,0,0,0,0,0,0,0,11,0,21,10,23,2,0,0,0,0],\n",
    "      [0,0,22,0,8,0,0,1,6,19,0,0,3,9,0,0,18,0,0,0,0,0,0,0,0],\n",
    "      [0,0,0,0,0,0,0,0,0,0,0,0,0,0,19,16,0,0,0,0,5,0,0,0,0],\n",
    "      [20,0,0,0,0,0,0,0,0,0,0,2,0,0,0,0,0,0,0,0,16,0,3,0,0],\n",
    "      \n",
    "      [0,0,0,0,0,0,0,18,17,15,0,0,0,0,0,0,0,0,0,0,0,0,0,6,0],\n",
    "      [19,0,0,0,0,0,0,14,0,0,0,5,0,17,0,0,0,0,21,0,0,2,22,0,0],\n",
    "      [0,7,2,0,0,0,0,12,0,0,0,0,0,3,0,0,0,0,0,0,0,0,0,21,0],\n",
    "      [10,23,11,0,0,8,0,2,0,0,0,0,12,0,0,0,0,0,0,0,0,0,0,17,0],\n",
    "      [15,0,0,0,0,0,0,11,0,0,0,0,0,0,0,19,0,0,0,0,13,16,14,0,0],\n",
    "      \n",
    "      [0,13,16,14,0,0,0,5,0,0,0,23,0,0,0,0,0,0,0,0,0,0,0,0,6],\n",
    "      [6,0,0,0,1,0,0,16,0,3,0,0,0,18,0,0,0,0,0,0,0,0,2,0,0],\n",
    "      [0,0,0,0,0,0,19,0,0,1,0,0,0,0,0,0,0,5,0,0,0,0,0,24,0],\n",
    "      [0,0,0,0,0,0,8,0,2,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0],\n",
    "      [0,15,20,0,0,21,0,23,11,0,0,0,0,2,22,0,19,0,0,0,0,0,0,14,0]]\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "a47f67f0-fb35-4fef-8627-4bd719b0c640",
   "metadata": {},
   "outputs": [],
   "source": [
    "# Import Pandas, numpy and Networkx\n",
    "import numpy as np\n",
    "import pandas as pd\n",
    "import networkx as nx\n",
    "import scipy as sp\n",
    "import math\n",
    "import time"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "8dff75af-b8bf-4287-af37-cdb6524c76ec",
   "metadata": {},
   "source": [
    "### Prob 1\n",
    "Build a Sudoku solver and run it on the samples above. All are assumed to be $n^2xn^2$, When solved, print out the values as a square grid to simplify interpretation. I would use the encoding $xijv$ i denotes the row, j means column, and v is the alphabet character."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "69b6a61b-4928-41bb-946e-de9f57b5e794",
   "metadata": {},
   "outputs": [],
   "source": [
    "def makecnf(s, n):\n",
    "    # Mapping to SAT\n",
    "    n_block = math.floor(math.sqrt(n))\n",
    "    cnf1= []    \n",
    "\n",
    "    # Add clauses related to fixed entries\n",
    "    for i in range(0,n):\n",
    "        for j in range(0,n):\n",
    "            v = s[i][j]\n",
    "            if v>0:\n",
    "                cnf1.append([i*n**2 + j*n +v])\n",
    "\n",
    "\n",
    "    print(\"Initial clauses are\", cnf1, \"\\n\")\n",
    "    # Definedness clauses per cell\n",
    "    for i in range(0,n):\n",
    "        for j in range (0,n):            \n",
    "            cnf1.append([i*n**2 + j*n +v  for v in range(1,n+1)])\n",
    "\n",
    "    # Uniqueness clause per cell\n",
    "    for i in range(0,n):\n",
    "        for j in range (0,n):\n",
    "            for vi in range(1,n+1):\n",
    "                for vj in range(vi+1,n+1):\n",
    "                    cnf1.append([-(i*n**2 + j*n + vi),-(i*n**2 + j*n + vj)])\n",
    "\n",
    "\n",
    "    # Definedness clause for each value through a column\n",
    "    for i in range(0,n):\n",
    "        for v in range(1, n+1):\n",
    "                cnf1.append([i*n**2 + j*n +v  for j in range(0,n)])\n",
    "\n",
    "    # Uniqueness clause for each value in a column\n",
    "    for i in range(0,n):\n",
    "            for v in range(1,n+1):\n",
    "                for j1 in range (0,n):\n",
    "                    for j2 in range (j1+1,n):\n",
    "                        cnf1.append([-(i*n**2 + j1*n + v),-(i*n**2 + j2*n + v)])\n",
    "\n",
    "    # Definedness clause for each value through a row\n",
    "    for j in range(0,n):\n",
    "        for v in range(1, n+1):\n",
    "                cnf1.append([i*n**2 + j*n +v  for i in range(0,n)])\n",
    "\n",
    "\n",
    "    # Uniqueness clause for each value in a row\n",
    "    for j in range(0,n):\n",
    "            for v in range(1,n+1):\n",
    "                for i1 in range (0,n):\n",
    "                    for i2 in range (i1+1,n):\n",
    "                        cnf1.append([-(i1*n**2 + j*n + v),-(i2*n**2 + j*n + v)])\n",
    "\n",
    "    # Definedness clause for each value through a block\n",
    "    for r_offset in range(0,n_block):\n",
    "        for c_offset in range(0,n_block):\n",
    "            for v in range(1,n+1):\n",
    "                cnf1.append([int(r_offset*n_block*(n**2) + c_offset*n_block*n + i*n**2 + j*n +v) for i in range(0,n_block) for j in range(0,n_block)])\n",
    "\n",
    "\n",
    "    # Uniqueness clause for each value through a block\n",
    "    for r_offset in range(0,n_block):\n",
    "        for c_offset in range(0,n_block):\n",
    "            for v in range(1,n+1):\n",
    "                for i1 in range(0,n_block):\n",
    "                    for j1 in range(0,n_block):\n",
    "                        for i2 in range(0,n_block):\n",
    "                            for j2 in range(0,n_block):\n",
    "                                if i1!=i2 or j1!=j2:\n",
    "                                    cnf1.append([-int(r_offset*n_block*(n**2) + c_offset*n_block*n + i1*n**2 + j1*n +v), -int(r_offset*n_block*(n**2) + c_offset*n_block*n + i2*n**2 + j2*n +v) ])\n",
    "\n",
    "\n",
    "\n",
    "    return cnf1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "62a22367-b65e-45d3-9a31-ed4eaaf0bafb",
   "metadata": {},
   "outputs": [],
   "source": [
    "def printsudoku(s,n):\n",
    "    n_block = math.sqrt(n)\n",
    "    print(\"\\n\")\n",
    "    for i in range(0,n):\n",
    "        line = \"\"\n",
    "        if i%n_block == 0:\n",
    "            print(\"---------------------\")\n",
    "        for j in range(0,n):\n",
    "            if j>0 and j%n_block == 0:\n",
    "                line += \"| \"\n",
    "            line += str(s[i][j])+\" \"\n",
    "        print(line)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "d5361252-d139-4629-9702-33217319bf8c",
   "metadata": {},
   "outputs": [],
   "source": [
    "def cnfsolver(cnf):\n",
    "    import time\n",
    "    start = time.time()\n",
    "    soln = pycosat.solve(cnf)\n",
    "    # print(\"SAT Solution is\", soln)\n",
    "    exec_time = time.time() - start\n",
    "    return exec_time, soln\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "70c0d1d5-3c60-464e-b6ff-3679d726fa63",
   "metadata": {},
   "outputs": [],
   "source": [
    "# Decoding SAT solution\n",
    "\n",
    "def Sudokumapper(s, soln, n):\n",
    "    for val in soln:\n",
    "        # Row value is int(val/n**2)\n",
    "        if val > 0:\n",
    "            i = int((val-1)/n**2)\n",
    "            j = int( int((val-1)%n**2)/n  )\n",
    "            # print(\"i,j\", i, j)\n",
    "            temp = val%(n)\n",
    "            if temp == 0:\n",
    "                s[i][j] = temp + n\n",
    "            else:\n",
    "                s[i][j] = temp\n",
    "    return s"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "5e1ccdac-f2ca-4f84-9b51-a0e246701e0c",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Initial clauses are [[20], [49], [73], [95], [120], [153], [165], [197], [221], [247], [271], [304], [334], [368], [392], [431], [457], [486], [513], [533], [565], [579], [607], [636], [656], [684], [703]] \n",
      "\n",
      "Execution time is 0.001994609832763672\n",
      "Sudoku Solution is\n",
      "\n",
      "\n",
      "---------------------\n",
      "9 8 2 | 5 7 4 | 6 3 1 \n",
      "1 5 7 | 2 3 6 | 4 9 8 \n",
      "3 4 6 | 8 9 1 | 5 7 2 \n",
      "---------------------\n",
      "4 9 5 | 1 2 3 | 7 8 6 \n",
      "7 1 3 | 6 8 9 | 2 5 4 \n",
      "6 2 8 | 4 5 7 | 3 1 9 \n",
      "---------------------\n",
      "5 6 9 | 3 1 2 | 8 4 7 \n",
      "2 3 1 | 7 4 8 | 9 6 5 \n",
      "8 7 4 | 9 6 5 | 1 2 3 \n"
     ]
    }
   ],
   "source": [
    "# Define the grid\n",
    "\n",
    "n = len(s1[0])\n",
    "n_block = math.sqrt(n)\n",
    "cnf = []\n",
    "soln = []\n",
    "cnf = makecnf(s1,n)\n",
    "\n",
    "# print(\" Cnf is\", cnf)\n",
    "exec_time, soln = cnfsolver(cnf)\n",
    "print(\"Execution time is\", exec_time)\n",
    "\n",
    "# Sudoku Solution mapper call\n",
    "s1 = Sudokumapper(s1, soln, n)\n",
    "print(\"Sudoku Solution is\")\n",
    "printsudoku(s1, n)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "2cb94f1c-7794-434a-b2c6-85fa1047b004",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Initial clauses are [[14], [27], [38], [47], [53]] \n",
      "\n",
      "Execution time is 0.0\n",
      "Sudoku Solution is\n",
      "\n",
      "\n",
      "---------------------\n",
      "1 3 | 4 2 \n",
      "2 4 | 3 1 \n",
      "---------------------\n",
      "4 2 | 1 3 \n",
      "3 1 | 2 4 \n"
     ]
    }
   ],
   "source": [
    "# Define the grid\n",
    "\n",
    "n = len(s2[0])\n",
    "cnf = []\n",
    "soln = []\n",
    "cnf = makecnf(s2,n)\n",
    "# print(\" Cnf is\", cnf)\n",
    "exec_time, soln = cnfsolver(cnf)\n",
    "print(\"Execution time is\", exec_time)\n",
    "\n",
    "# Sudoku Solution mapper call\n",
    "s2 = Sudokumapper(s2, soln, n)\n",
    "print(\"Sudoku Solution is\")\n",
    "printsudoku(s2, n)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "c3386170-ae7d-4504-975b-7587412108a8",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Initial clauses are [[91], [114], [142], [285], [336], [374], [452], [656], [841], [993], [1021], [1182], [1475], [1487], [1665], [1836], [2253], [2445], [2493], [2671], [3268], [3292], [3345], [3355], [3875], [3991], [4065], [4149], [4171], [4185], [4272], [4512], [4556], [4741], [4815], [4973], [5172], [5403], [5518], [5542], [5605], [5692], [5922], [5958], [5982], [6139], [6184], [6241], [6289], [6380], [6418], [6511], [6585], [6679], [6708], [6732], [6776], [6900], [6926], [7016], [7261], [7321], [7335], [7373], [7377], [7572], [7608], [7676], [7706], [7744], [7803], [7834], [7918], [8494], [8516], [8630], [8770], [9027], [9266], [9303], [9568], [9592], [9615], [9956], [10019], [10189], [10280], [10342], [10471], [10527], [10572], [10657], [10677], [10812], [10953], [11221], [11260], [11298], [11311], [11383], [11427], [11562], [11842], [11890], [12061], [12269], [12388], [12416], [12439], [12538], [12566], [12589], [12680], [12798], [13106], [13131], [13226], [13316], [13353], [13468], [13677], [13919], [13976], [14180], [14349], [14533], [14577], [14726], [15040], [15070], [15146], [15198], [15211], [15327], [15372], [15419], [15589]] \n",
      "\n",
      "Execution time is 0.11569046974182129\n",
      "Sudoku Solution is\n",
      "\n",
      "\n",
      "---------------------\n",
      "23 25 21 16 14 | 17 20 22 19 18 | 15 10 13 11 24 | 12 9 7 2 8 | 6 5 4 3 1 \n",
      "24 6 19 22 20 | 23 15 13 16 14 | 25 3 17 12 18 | 21 11 1 5 4 | 10 9 7 8 2 \n",
      "18 17 13 10 9 | 24 7 3 25 12 | 8 1 2 5 4 | 23 15 22 20 6 | 19 21 16 11 14 \n",
      "12 11 15 8 7 | 10 5 4 1 2 | 23 21 22 6 9 | 3 25 19 16 14 | 17 24 20 13 18 \n",
      "5 4 3 1 2 | 11 21 9 8 6 | 20 19 16 7 14 | 18 24 17 13 10 | 25 23 15 22 12 \n",
      "---------------------\n",
      "22 24 23 21 19 | 18 17 25 20 5 | 14 13 11 4 12 | 9 16 8 7 2 | 15 10 6 1 3 \n",
      "14 20 18 13 25 | 9 23 8 7 16 | 19 17 15 1 3 | 24 21 10 6 5 | 22 12 11 2 4 \n",
      "11 10 9 7 5 | 12 24 6 3 4 | 2 20 18 25 16 | 22 17 15 14 1 | 8 19 13 23 21 \n",
      "16 12 8 2 4 | 1 22 15 14 13 | 9 6 23 21 10 | 25 3 20 19 11 | 18 17 24 7 5 \n",
      "3 1 17 15 6 | 2 11 19 21 10 | 24 22 5 8 7 | 13 23 18 4 12 | 14 25 9 20 16 \n",
      "---------------------\n",
      "21 14 24 23 3 | 5 18 20 22 25 | 11 16 6 10 17 | 15 2 4 8 7 | 12 1 19 9 13 \n",
      "25 19 1 18 17 | 16 3 24 15 9 | 22 14 20 13 5 | 11 12 21 10 23 | 2 6 8 4 7 \n",
      "13 16 22 12 8 | 14 2 1 6 19 | 7 4 3 9 25 | 5 18 24 17 20 | 23 15 21 10 11 \n",
      "9 2 10 6 15 | 7 12 21 4 11 | 18 24 8 23 19 | 16 22 13 1 3 | 5 14 17 25 20 \n",
      "20 5 7 4 11 | 13 10 17 23 8 | 12 2 1 15 21 | 14 6 25 9 19 | 16 22 3 18 24 \n",
      "---------------------\n",
      "8 22 14 25 24 | 20 16 18 17 15 | 21 11 10 19 23 | 7 5 2 12 13 | 4 3 1 6 9 \n",
      "19 18 6 20 16 | 25 13 14 24 7 | 4 5 9 17 8 | 10 1 3 21 15 | 11 2 22 12 23 \n",
      "1 7 2 5 13 | 19 4 12 9 23 | 16 25 24 3 6 | 8 14 11 22 17 | 20 18 10 21 15 \n",
      "10 23 11 3 21 | 8 1 2 5 22 | 13 15 12 14 20 | 6 4 16 18 9 | 24 7 25 17 19 \n",
      "15 9 4 17 12 | 3 6 11 10 21 | 1 18 7 22 2 | 19 20 23 24 25 | 13 16 14 5 8 \n",
      "---------------------\n",
      "17 13 16 14 22 | 4 25 5 12 24 | 10 23 19 20 11 | 2 7 9 3 21 | 1 8 18 15 6 \n",
      "6 8 5 11 1 | 22 14 16 13 3 | 17 9 21 18 15 | 20 10 12 23 24 | 7 4 2 19 25 \n",
      "2 3 25 9 10 | 15 19 7 18 1 | 6 12 14 16 13 | 4 8 5 11 22 | 21 20 23 24 17 \n",
      "4 21 12 19 23 | 6 8 10 2 20 | 3 7 25 24 1 | 17 13 14 15 18 | 9 11 5 16 22 \n",
      "7 15 20 24 18 | 21 9 23 11 17 | 5 8 4 2 22 | 1 19 6 25 16 | 3 13 12 14 10 \n"
     ]
    }
   ],
   "source": [
    "# Define the grid\n",
    "\n",
    "n = len(s3[0])\n",
    "cnf = []\n",
    "soln = []\n",
    "cnf = makecnf(s3,n)\n",
    "# print(\" Cnf is\", cnf)\n",
    "exec_time, soln = cnfsolver(cnf)\n",
    "print(\"Execution time is\", exec_time)\n",
    "\n",
    "# Sudoku Solution mapper call\n",
    "s3 = Sudokumapper(s3, soln, n)\n",
    "print(\"Sudoku Solution is\")\n",
    "printsudoku(s3, n)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "624de00f-5e6b-4f08-9c18-32523b85e543",
   "metadata": {},
   "source": [
    "### Prob 2\n",
    "The Sudoku solver performance can be improved substantially by simplifying the cnf (removing clauses) that are obviated when the unsettable squares are filled. (Some clauses become tautologies, some have many false literals and many serve no more purpose). Use this to simplify the cnf and speed-up the solver."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "cbe093f3-b03c-42da-98c8-7f83cd7baed2",
   "metadata": {},
   "outputs": [],
   "source": [
    "s1 = [[0,0,2,0,0,4,0,0,1],\n",
    "      [0,5,0,0,3,0,0,9,0],\n",
    "      [3,0,0,8,0,0,5,0,0],\n",
    "      [4,0,0,1,0,0,7,0,0],\n",
    "      [0,1,0,0,8,0,0,5,0],\n",
    "      [0,0,8,0,0,7,0,0,9],\n",
    "      [0,0,9,0,0,2,0,0,7],\n",
    "      [0,3,0,0,4,0,0,6,0],\n",
    "      [8,0,0,9,0,0,1,0,0]]\n",
    "s2 = [[0, 0, 0, 2],\n",
    "      [0, 0, 3, 0],\n",
    "      [0, 2, 0, 3],\n",
    "      [0, 1, 0, 0]]\n",
    "s3 = [[0,0,0,16,14,17,0,0,0,0,0,10,0,11,24,0,0,0,2,0,0,0,0,0,0],\n",
    "      [0,6,0,0,0,0,0,0,16,0,0,0,0,0,18,21,0,0,0,0,0,0,7,0,0],\n",
    "      [0,0,0,0,0,0,0,0,25,12,0,0,0,0,0,0,15,0,0,0,0,0,0,11,0],\n",
    "      [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,3,0,0,0,0,0,0,20,0,18],\n",
    "      [0,0,0,0,0,0,21,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],\n",
    "      \n",
    "      [0,0,0,0,0,18,17,0,20,5,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],      \n",
    "      [0,0,0,0,25,0,0,0,0,16,0,0,15,0,0,24,21,10,0,0,22,0,0,0,0],\n",
    "      [0,0,0,0,0,12,0,6,0,0,0,0,0,0,16,0,0,15,0,0,0,0,0,23,0],\n",
    "      [0,0,0,0,0,0,22,0,0,0,0,0,0,0,0,0,3,0,0,0,18,17,0,0,5],\n",
    "      [0,0,17,0,0,0,0,0,0,0,0,22,0,8,7,0,0,0,0,0,14,0,9,0,16],\n",
    "      \n",
    "      [0,14,0,0,0,5,18,0,0,0,11,0,0,10,0,0,0,4,8,7,0,1,0,0,0],\n",
    "      [25,0,1,0,0,16,0,0,0,0,0,0,0,0,0,11,0,21,10,23,2,0,0,0,0],\n",
    "      [0,0,22,0,8,0,0,1,6,19,0,0,3,9,0,0,18,0,0,0,0,0,0,0,0],\n",
    "      [0,0,0,0,0,0,0,0,0,0,0,0,0,0,19,16,0,0,0,0,5,0,0,0,0],\n",
    "      [20,0,0,0,0,0,0,0,0,0,0,2,0,0,0,0,0,0,0,0,16,0,3,0,0],\n",
    "      \n",
    "      [0,0,0,0,0,0,0,18,17,15,0,0,0,0,0,0,0,0,0,0,0,0,0,6,0],\n",
    "      [19,0,0,0,0,0,0,14,0,0,0,5,0,17,0,0,0,0,21,0,0,2,22,0,0],\n",
    "      [0,7,2,0,0,0,0,12,0,0,0,0,0,3,0,0,0,0,0,0,0,0,0,21,0],\n",
    "      [10,23,11,0,0,8,0,2,0,0,0,0,12,0,0,0,0,0,0,0,0,0,0,17,0],\n",
    "      [15,0,0,0,0,0,0,11,0,0,0,0,0,0,0,19,0,0,0,0,13,16,14,0,0],\n",
    "      \n",
    "      [0,13,16,14,0,0,0,5,0,0,0,23,0,0,0,0,0,0,0,0,0,0,0,0,6],\n",
    "      [6,0,0,0,1,0,0,16,0,3,0,0,0,18,0,0,0,0,0,0,0,0,2,0,0],\n",
    "      [0,0,0,0,0,0,19,0,0,1,0,0,0,0,0,0,0,5,0,0,0,0,0,24,0],\n",
    "      [0,0,0,0,0,0,8,0,2,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0],\n",
    "      [0,15,20,0,0,21,0,23,11,0,0,0,0,2,22,0,19,0,0,0,0,0,0,14,0]]\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "6f331f48-9c01-49e9-8641-7b8d222c6e71",
   "metadata": {},
   "outputs": [],
   "source": [
    "def makecnf_optim(s, n):\n",
    "    # Mapping to SAT\n",
    "\n",
    "                                \n",
    "    n_block = math.floor(math.sqrt(n))\n",
    "    cnf1= []    \n",
    "    uniq_lst = []\n",
    "    dfnd_lst =[]\n",
    "    fixed_literals = []\n",
    "    for i in range(0,n):   # row\n",
    "        for j in range(0,n):    # column\n",
    "            val = s[i][j]            \n",
    "            if val>0:             \n",
    "                fixed_literals.append([i, j, val, i*n**2 + j*n +val])\n",
    "                \n",
    "    # Add clauses related to fixed entries\n",
    "    for i in range(0,n):   # row\n",
    "        for j in range(0,n):    # column\n",
    "            val = s[i][j]\n",
    "            if val>0:                \n",
    "                # V+ constraints add\n",
    "                cnf1.append([i*n**2 + j*n +val])\n",
    "    # print(\"Initial clauses are\", cnf1, \"\\n\")\n",
    "\n",
    "    for i in range(0,n):\n",
    "        for j in range (0,n):\n",
    "            # Definedness clauses per cell\n",
    "            cnf1.append([i*n**2 + j*n +v  for v in range(1,n+1)])\n",
    "            dfnd_lst.append([i*n**2 + j*n +v  for v in range(1,n+1)])\n",
    "            \n",
    "    # Uniqueness clause per cell\n",
    "    for i in range(0,n):\n",
    "        for j in range (0,n):\n",
    "            for vi in range(1,n+1):\n",
    "                for vj in range(vi+1,n+1):\n",
    "                    cnf1.append([-(i*n**2 + j*n + vi),-(i*n**2 + j*n + vj)])\n",
    "                    uniq_lst.append([-(i*n**2 + j*n + vi),-(i*n**2 + j*n + vj)])\n",
    "\n",
    "    # Definedness clause for each value through a column\n",
    "    for i in range(0,n):\n",
    "        for v in range(1, n+1):\n",
    "                cnf1.append([i*n**2 + j*n +v  for j in range(0,n)])\n",
    "                dfnd_lst.append([i*n**2 + j*n +v  for j in range(0,n)])\n",
    "\n",
    "    # Uniqueness clause for each value in a column\n",
    "    for i in range(0,n):\n",
    "            for v in range(1,n+1):\n",
    "                for j1 in range (0,n):\n",
    "                    for j2 in range (j1+1,n):\n",
    "                        cnf1.append([-(i*n**2 + j1*n + v),-(i*n**2 + j2*n + v)])\n",
    "                        uniq_lst.append([-(i*n**2 + j1*n + v),-(i*n**2 + j2*n + v)])\n",
    "                        \n",
    "    # Definedness clause for each value through a row\n",
    "    for j in range(0,n):\n",
    "        for v in range(1, n+1):\n",
    "                cnf1.append([i*n**2 + j*n +v  for i in range(0,n)])\n",
    "                dfnd_lst.append([i*n**2 + j*n +v  for i in range(0,n)])\n",
    "\n",
    "    # Uniqueness clause for each value in a row\n",
    "    for j in range(0,n):\n",
    "            for v in range(1,n+1):\n",
    "                for i1 in range (0,n):\n",
    "                    for i2 in range (i1+1,n):\n",
    "                        cnf1.append([-(i1*n**2 + j*n + v),-(i2*n**2 + j*n + v)])\n",
    "                        uniq_lst.append([-(i1*n**2 + j*n + v),-(i2*n**2 + j*n + v)])\n",
    "                        \n",
    "    # Definedness clause for each value through a block\n",
    "    for r_offset in range(0,n_block):\n",
    "        for c_offset in range(0,n_block):\n",
    "            for v in range(1,n+1):\n",
    "                cnf1.append([int(r_offset*n_block*(n**2) + c_offset*n_block*n + i*n**2 + j*n +v) for i in range(0,n_block) for j in range(0,n_block)])\n",
    "                dfnd_lst.append([int(r_offset*n_block*(n**2) + c_offset*n_block*n + i*n**2 + j*n +v) for i in range(0,n_block) for j in range(0,n_block)])\n",
    "                \n",
    "\n",
    "    # Uniqueness clause for each value through a block\n",
    "    for r_offset in range(0,n_block):\n",
    "        for c_offset in range(0,n_block):\n",
    "            for v in range(1,n+1):\n",
    "                for i1 in range(0,n_block):\n",
    "                    for j1 in range(0,n_block):\n",
    "                        for i2 in range(0,n_block):\n",
    "                            for j2 in range(0,n_block):\n",
    "                                if i1!=i2 or j1!=j2:\n",
    "                                    cnf1.append([-int(r_offset*n_block*(n**2) + c_offset*n_block*n + i1*n**2 + j1*n +v), -int(r_offset*n_block*(n**2) + c_offset*n_block*n + i2*n**2 + j2*n +v) ])\n",
    "                                    uniq_lst.append([-int(r_offset*n_block*(n**2) + c_offset*n_block*n + i1*n**2 + j1*n +v), -int(r_offset*n_block*(n**2) + c_offset*n_block*n + i2*n**2 + j2*n +v) ])\n",
    "\n",
    "    \n",
    "    cnf = []\n",
    "    # Remove redundant clauses\n",
    "    # temp = list(map(lambda x: tuple(sorted(x)),cnf1))\n",
    "    # cnf = [list(ele) for ele in temp]\n",
    "    \n",
    "    unique_lst = []\n",
    "    # Remove redundant clauses\n",
    "    temp1 = list(map(lambda x: tuple(sorted(x)),uniq_lst))\n",
    "    unique_lst = [list(ele) for ele in temp1]\n",
    "           \n",
    "    terminate_list = []\n",
    "    # V- variable list: literals that are false\n",
    "    for i in range(0,n):   # row\n",
    "        for j in range(0,n):    # column\n",
    "            val = s[i][j]            \n",
    "            if val>0:             \n",
    "                # Same cell\n",
    "                for v in range(1,n+1):\n",
    "                    if v!=val:\n",
    "                        terminate_list.append(i*n**2 + j*n +v)             \n",
    "                # Same row              \n",
    "                for c in range(0,n):\n",
    "                    if c!= j:\n",
    "                        terminate_list.append(i*n**2 + c*n +val)  \n",
    "                        \n",
    "                # Same col\n",
    "                for r in range(0,n):\n",
    "                    if r!=i:\n",
    "                        terminate_list.append(r*n**2 + j*n +val)       \n",
    "                        \n",
    "                # Same block\n",
    "                r_offset = int(i/n_block)\n",
    "                c_offset = int(j/n_block)\n",
    "                for ii in range(0,n_block):\n",
    "                    for jj in range(0,n_block):\n",
    "                        if ii!=(i%n_block) or jj!=(j%n_block):\n",
    "                            terminate_list.append(int(r_offset*n_block*(n**2) + c_offset*n_block*n + ii*n**2 + jj*n +val) )\n",
    "                \n",
    "                terminate_list = list(set(terminate_list))\n",
    "                \n",
    "    # print(\"Terminate List is\")\n",
    "    # print(terminate_list)\n",
    "                \n",
    "    \n",
    "    # Remove uniqueness constraints containing V- variables   \n",
    "    for entry in terminate_list:       \n",
    "        # print(\"Removed Item are\")\n",
    "        for item in unique_lst:\n",
    "            if (-entry in item):\n",
    "                unique_lst.remove(item)\n",
    "                #  print(item)\n",
    "      \n",
    "    # Remove  V- literals from definedeness list\n",
    "        # print(\"Modified Defined list is\")\n",
    "        for item in dfnd_lst:\n",
    "            if (entry in item):\n",
    "                item.remove(entry)\n",
    "                #  print(item)\n",
    "\n",
    "    cnf = unique_lst + dfnd_lst \n",
    "    \n",
    "    return cnf, unique_lst, dfnd_lst"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "8d35fd5f-703a-461c-93d5-40e85fac68b5",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'\\ndef clause_destroyer(literal, unique_lst, dfnd_lst):\\n    \\n    temp = int(literal/n)\\n    val = literal%n\\n    if literal%n ==0:\\n        temp = temp -1 \\n        val = n  # This value\\n    i = temp%n   # Row retrieval\\n    j = int(temp/n)    # Column Retrieval\\n\\n    for v in range(1,n+1):\\n        if v!=val:\\n                terminate_list.append(i*n**2 + j*n +v)             \\n        # Same row              \\n        for c in range(0,n):\\n            if c!= j:\\n                terminate_list.append(i*n**2 + c*n +val)  \\n\\n        # Same col\\n        for r in range(0,n):\\n            if r!=i:\\n                terminate_list.append(r*n**2 + j*n +val)       \\n\\n        # Same block\\n        r_offset = int(i/n_block)\\n        c_offset = int(j/n_block)\\n        for ii in range(0,n_block):\\n            for jj in range(0,n_block):\\n                if ii!=(i%n_block) or jj!=(j%n_block):\\n                    terminate_list.append(int(r_offset*n_block*(n**2) + c_offset*n_block*n + ii*n**2 + jj*n +val) )\\n\\n        terminate_list = list(set(terminate_list))\\n\\n\\n    # Remove uniqueness constraints containing V- variables \\n    print(\"Removed Item are\")\\n    for entry in terminate_list:           \\n        for item in unique_lst:\\n            if (-entry in item):\\n                unique_lst.remove(item)\\n                print(item)\\n\\n        # Remove  V- literals from definedeness list\\n        print(\"Modified Defined list is\")\\n        for item in dfnd_lst:\\n            if (entry in item):\\n                item.remove(entry)\\n                print(item)\\n\\n    cnf = unique_lst + dfnd_lst \\n\\n    return cnf, unique_lst, dfnd_lst\\n    \\n'"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "'''\n",
    "def clause_destroyer(literal, unique_lst, dfnd_lst):\n",
    "    \n",
    "    temp = int(literal/n)\n",
    "    val = literal%n\n",
    "    if literal%n ==0:\n",
    "        temp = temp -1 \n",
    "        val = n  # This value\n",
    "    i = temp%n   # Row retrieval\n",
    "    j = int(temp/n)    # Column Retrieval\n",
    "\n",
    "    for v in range(1,n+1):\n",
    "        if v!=val:\n",
    "                terminate_list.append(i*n**2 + j*n +v)             \n",
    "        # Same row              \n",
    "        for c in range(0,n):\n",
    "            if c!= j:\n",
    "                terminate_list.append(i*n**2 + c*n +val)  \n",
    "\n",
    "        # Same col\n",
    "        for r in range(0,n):\n",
    "            if r!=i:\n",
    "                terminate_list.append(r*n**2 + j*n +val)       \n",
    "\n",
    "        # Same block\n",
    "        r_offset = int(i/n_block)\n",
    "        c_offset = int(j/n_block)\n",
    "        for ii in range(0,n_block):\n",
    "            for jj in range(0,n_block):\n",
    "                if ii!=(i%n_block) or jj!=(j%n_block):\n",
    "                    terminate_list.append(int(r_offset*n_block*(n**2) + c_offset*n_block*n + ii*n**2 + jj*n +val) )\n",
    "\n",
    "        terminate_list = list(set(terminate_list))\n",
    "\n",
    "\n",
    "    # Remove uniqueness constraints containing V- variables \n",
    "    print(\"Removed Item are\")\n",
    "    for entry in terminate_list:           \n",
    "        for item in unique_lst:\n",
    "            if (-entry in item):\n",
    "                unique_lst.remove(item)\n",
    "                print(item)\n",
    "\n",
    "        # Remove  V- literals from definedeness list\n",
    "        print(\"Modified Defined list is\")\n",
    "        for item in dfnd_lst:\n",
    "            if (entry in item):\n",
    "                item.remove(entry)\n",
    "                print(item)\n",
    "\n",
    "    cnf = unique_lst + dfnd_lst \n",
    "\n",
    "    return cnf, unique_lst, dfnd_lst\n",
    "    \n",
    "'''"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "11b76070-da90-4ed3-a1a7-27aa3ebc5a46",
   "metadata": {},
   "outputs": [],
   "source": [
    "def cnfsolver_optim(cnf, n, unique_lst, dfnd_lst):\n",
    "    \n",
    "    import time\n",
    "    start = time.time()\n",
    "    term_list = [i for i in range(1,n*n*n + 1)]\n",
    "    soln = pycosat.solve(cnf)\n",
    "    #for soln in pycosat.itersolve(cnf):\n",
    "    #    if (soln in term_list):\n",
    "    #        cnf, unique_lst, dfnd_lst = clause_destroyer(soln, cnf, unique_lst, dfnd_lst)\n",
    "            # solns.append(frozenset(map(self.vars.lookupNum, filter(lambda x: x > 0, soln))))\n",
    "        # print(\"SAT Solution is\", soln)  \n",
    "        \n",
    "    exec_time = time.time() - start\n",
    "    return exec_time, soln"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "1bead5c4-2434-4eaa-a413-1e53d17f3fe8",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      " Cnf is [[-3, -1], [-4, -1], [-4, -2], [-4, -3], [-7, -5], [-8, -6], [-8, -7], [-12, -9], [-12, -10], [-15, -14], [-18, -17], [-20, -17], [-20, -18], [-24, -22], [-27, -25], [-28, -27], [-32, -29], [-32, -30], [-36, -34], [-39, -38], [-44, -41], [-44, -42], [-47, -45], [-48, -47], [-51, -49], [-52, -50], [-52, -51], [-56, -54], [-59, -58], [-60, -58], [-64, -62], [-9, -1], [-13, -5], [-14, -6], [-7, -3], [-15, -7], [-8, -4], [-12, -4], [-12, -8], [-29, -17], [-29, -21], [-30, -22], [-27, -19], [-24, -20], [-32, -20], [-32, -24], [-41, -33], [-42, -38], [-47, -39], [-44, -36], [-48, -40], [-57, -53], [-58, -50], [-63, -55], [-60, -52], [-64, -52], [-64, -56], [-64, -60], [-17, -1], [-49, -17], [-34, -18], [-51, -3], [-51, -19], [-20, -4], [-36, -4], [-52, -4], [-36, -20], [-52, -20], [-52, -36], [-53, -21], [-38, -6], [-55, -23], [-24, -8], [-56, -24], [-41, -9], [-57, -25], [-58, -26], [-43, -27], [-44, -12], [-60, -12], [-60, -28], [-60, -44], [-45, -29], [-62, -30], [-47, -15], [-48, -32], [-64, -32], [-17, -1], [-17, -1], [-17, -5], [-21, -1], [-18, -2], [-18, -6], [-22, -18], [-7, -3], [-7, -3], [-19, -7], [-23, -7], [-8, -4], [-20, -4], [-24, -4], [-8, -4], [-20, -8], [-24, -8], [-20, -4], [-20, -8], [-24, -20], [-24, -4], [-24, -8], [-24, -20], [-29, -9], [-25, -13], [-29, -9], [-14, -10], [-26, -14], [-27, -11], [-27, -15], [-31, -27], [-31, -27], [-32, -12], [-16, -12], [-28, -16], [-32, -12], [-49, -37], [-53, -49], [-38, -34], [-50, -38], [-54, -38], [-51, -35], [-51, -39], [-55, -51], [-52, -36], [-52, -36], [-52, -40], [-56, -36], [-45, -41], [-57, -45], [-58, -42], [-58, -46], [-62, -58], [-62, -58], [-47, -43], [-59, -47], [-63, -47], [-60, -44], [-64, -44], [-60, -44], [-60, -48], [-64, -60], [-64, -44], [-64, -60], [1, 3, 4], [7, 8], [9, 12], [14], [17, 18, 20], [24], [27], [29, 32], [36], [38], [41, 44], [47], [51, 52], [53], [58, 60], [64], [1, 9], [14], [3, 7], [4, 8, 12], [17, 29], [18], [27], [20, 24, 32], [41], [38], [47], [36, 44], [53], [58], [51], [52, 60, 64], [1, 17], [18], [3, 51], [4, 20, 36, 52], [53], [38], [7], [8, 24], [9, 41], [58], [27], [12, 44, 60], [29], [14], [47], [32, 64], [1, 17], [18], [3, 7], [4, 8, 20, 24], [9, 29], [14], [27], [12, 32], [53], [38], [51], [36, 52], [41], [58], [47], [44, 60, 64]]\n",
      "Execution time is 0.0\n",
      "Sudoku Solution is\n",
      "\n",
      "\n",
      "---------------------\n",
      "1 3 | 4 2 \n",
      "2 4 | 3 1 \n",
      "---------------------\n",
      "4 2 | 1 3 \n",
      "3 1 | 2 4 \n"
     ]
    }
   ],
   "source": [
    "# Define the grid\n",
    "\n",
    "n = len(s2[0])\n",
    "cnf = []\n",
    "unique_lst = []\n",
    "dfnd_lst = []\n",
    "soln = []\n",
    "cnf, unique_lst, dfnd_lst = makecnf_optim(s2,n)\n",
    "print(\" Cnf is\", cnf)\n",
    "exec_time, soln = cnfsolver_optim(cnf, n, unique_lst, dfnd_lst)\n",
    "print(\"Execution time is\", exec_time)\n",
    "\n",
    "# Sudoku Solution mapper call\n",
    "s2 = Sudokumapper(s2, soln, n)\n",
    "print(\"Sudoku Solution is\")\n",
    "printsudoku(s2, n)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "fa7335cd-df9f-458c-b184-04f595920e13",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Execution time is 0.0019948482513427734\n",
      "Sudoku Solution is\n",
      "\n",
      "\n",
      "---------------------\n",
      "9 8 2 | 5 7 4 | 6 3 1 \n",
      "1 5 7 | 2 3 6 | 4 9 8 \n",
      "3 4 6 | 8 9 1 | 5 7 2 \n",
      "---------------------\n",
      "4 9 5 | 1 2 3 | 7 8 6 \n",
      "7 1 3 | 6 8 9 | 2 5 4 \n",
      "6 2 8 | 4 5 7 | 3 1 9 \n",
      "---------------------\n",
      "5 6 9 | 3 1 2 | 8 4 7 \n",
      "2 3 1 | 7 4 8 | 9 6 5 \n",
      "8 7 4 | 9 6 5 | 1 2 3 \n"
     ]
    }
   ],
   "source": [
    "# Define the grid\n",
    "n = len(s1[0])\n",
    "cnf = []\n",
    "unique_lst = []\n",
    "dfnd_lst = []\n",
    "soln = []\n",
    "cnf, unique_lst, dfnd_lst = makecnf_optim(s1,n)\n",
    "# print(\" Cnf is\", cnf)\n",
    "exec_time, soln = cnfsolver_optim(cnf, n, unique_lst, dfnd_lst)\n",
    "print(\"Execution time is\", exec_time)\n",
    "\n",
    "# Sudoku Solution mapper call\n",
    "s1 = Sudokumapper(s1, soln, n)\n",
    "print(\"Sudoku Solution is\")\n",
    "printsudoku(s1, n)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "792bc730-c61e-48d1-9af1-18b001b28c7d",
   "metadata": {},
   "outputs": [],
   "source": [
    "# Define the grid\n",
    "\n",
    "n = len(s3[0])\n",
    "cnf = []\n",
    "unique_lst = []\n",
    "dfnd_lst = []\n",
    "soln = []\n",
    "start = time.time()\n",
    "cnf, unique_lst, dfnd_lst = makecnf_optim(s3,n)\n",
    "build_time = time.time() - start\n",
    "print(\"build time for CNF is\", build_time)\n",
    "# print(\" Cnf is\", cnf)\n",
    "exec_time, soln = cnfsolver(cnf)\n",
    "print(\"Execution time is\", exec_time)\n",
    "\n",
    "# Sudoku Solution mapper call\n",
    "s3 = Sudokumapper(s3, soln, n)\n",
    "print(\"Sudoku Solution is\")\n",
    "printsudoku(s3, n)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b3331b85-f6f2-4c1a-90d5-f3d2fd8e539c",
   "metadata": {},
   "source": [
    "### Prob 3 (Optional)\n",
    "Use BreakID (provided on the Gauchospace page) to build symmetry-breaking additional clauses for your cnf. Do you get additional speedup?"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "5d99af00-f0dd-4ce5-8bb3-8ec8fd89ea21",
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.8.8"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}