SAT_applications.ipynb

sat_applications.ipynb

{
  "nbformat": 4,
  "nbformat_minor": 0,
  "metadata": {
    "colab": {
      "name": "SAT_applications.ipynb",
      "provenance": [],
      "collapsed_sections": [],
      "include_colab_link": true
    },
    "kernelspec": {
      "name": "python3",
      "display_name": "Python 3"
    }
  },
  "cells": [
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "view-in-github",
        "colab_type": "text"
      },
      "source": [
        "<a href=\"https://colab.research.google.com/gist/rummanwaqar/4985fb5b5eebacf18ce5b0e0949fb1e8/sat_applications.ipynb\" target=\"_parent\"><img src=\"https://colab.research.google.com/assets/colab-badge.svg\" alt=\"Open In Colab\"/></a>"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "bZl3o0Ubpv3O",
        "colab_type": "text"
      },
      "source": [
        "# Applications of Satisfiability "
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "jnyK52KeGfrn",
        "colab_type": "code",
        "outputId": "80c2ad82-a147-4540-a809-dad3d8f2c0a5",
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 34
        }
      },
      "source": [
        "# install pycosat (SAT solver)\n",
        "!pip install pycosat"
      ],
      "execution_count": 1,
      "outputs": [
        {
          "output_type": "stream",
          "text": [
            "Requirement already satisfied: pycosat in /usr/local/lib/python3.6/dist-packages (0.6.3)\n"
          ],
          "name": "stdout"
        }
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "pQg5vY9NGhi5",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "import pycosat"
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "hgSG1CBSp7pS",
        "colab_type": "text"
      },
      "source": [
        "## Problem A\n",
        "Check if p = (x₁ ∧ (¬x₁ ∨ x₂) ∧ x₃) is satisfiable."
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "CnYJvyNWp7RF",
        "colab_type": "code",
        "outputId": "686daf0c-992a-46de-c310-189f2d3cc7a6",
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 34
        }
      },
      "source": [
        "p = [[1], [-1, 2], [3]]\n",
        "print(pycosat.solve(p))"
      ],
      "execution_count": 3,
      "outputs": [
        {
          "output_type": "stream",
          "text": [
            "[1, 2, 3]\n"
          ],
          "name": "stdout"
        }
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "833o09hrJ65S",
        "colab_type": "text"
      },
      "source": [
        "## Problem B - Row problem\n",
        "\n",
        "Given a list of size 4 with some unknown values, find a set of unique numbers between 1–4 such that each number only appears once in the list.\n",
        "\n",
        "**Let p(i, n) be a proposition that is true when number n is in cell i**. Since we have 4 cells and each cell can have 4 possible values we have 16 different variables.\n",
        "\n",
        "1. For each cell with known value, we assert `p(i, n) = true`.\n",
        "2. Assert that the row contains all n numbers $\\bigwedge\\limits_{n=1}^4 \\bigvee\\limits_{i=1}^4 p(i, n)$\n",
        "3. Assert that no cell contains more than one number by taking conjuction over all n, n', i from 1 to 4 where $n\\neq n'$ if $p(i, n) \\implies \\neg p(i, n')$."
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "WZs_o4y8Ngne",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "def row_problem(input_list):\n",
        "\n",
        "  def p(i, n):\n",
        "    # returns variable number for a given cell / value combination\n",
        "    return 4 * (i-1) + n\n",
        "\n",
        "  clauses = []\n",
        "\n",
        "  # step 1\n",
        "  for i in range(1, 5):\n",
        "    # lists in python are 0 indexed\n",
        "    digit = sample_input[i - 1]\n",
        "    if digit:\n",
        "      clauses.append([p(i, digit)])\n",
        "\n",
        "  # step 2\n",
        "  for n in range(1, 5):\n",
        "  # q(n) = list contains number n\n",
        "    q = []\n",
        "    for i in range(1, 5):\n",
        "      q.append(p(i, n))\n",
        "    clauses.append(q)\n",
        "\n",
        "  # step 3\n",
        "  for i in range(1, 5):\n",
        "    for n in range(1, 5):\n",
        "      for n_not in range(1, 5):\n",
        "        if n == n_not:\n",
        "          continue\n",
        "        clauses.append([-p(i, n), -p(i, n_not)])\n",
        "\n",
        "  sols = []\n",
        "  for sol in pycosat.itersolve(clauses):\n",
        "    sols.append(sol)\n",
        "  return sols\n",
        "\n",
        "def convert_list(soln):\n",
        "  output = []\n",
        "  for i in soln:\n",
        "    if i > 0:\n",
        "      number = i % 4\n",
        "      if number == 0:\n",
        "        number = 4\n",
        "      output.append(number)\n",
        "  return output"
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "Dk0IJo24M5Vg",
        "colab_type": "code",
        "outputId": "80d16925-9d82-4205-dfd4-bc11f783daf5",
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 85
        }
      },
      "source": [
        "sample_input = [0, 3, 0, 1]\n",
        "solns = row_problem(sample_input)\n",
        "\n",
        "for i, soln in enumerate(solns):\n",
        "  print(\"soln {}:\".format(i + 1))\n",
        "  print(convert_list(soln))"
      ],
      "execution_count": 5,
      "outputs": [
        {
          "output_type": "stream",
          "text": [
            "soln 1:\n",
            "[4, 3, 2, 1]\n",
            "soln 2:\n",
            "[2, 3, 4, 1]\n"
          ],
          "name": "stdout"
        }
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "PLRzC_28mYI_",
        "colab_type": "text"
      },
      "source": [
        "## Problem C - Sudoku Puzzle"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "dZv5RuKjuBeO",
        "colab_type": "text"
      },
      "source": [
        "\n",
        "### Retrieve sudoku from http://websudoku.*com*\n",
        "\n"
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "kDvD81d2hq37",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "import urllib.request\n",
        "from bs4 import BeautifulSoup\n",
        "\n",
        "def getHtml(url):\n",
        "  '''\n",
        "  returns HTML source for given URL\n",
        "  '''\n",
        "  fp = urllib.request.urlopen(url)\n",
        "  data = fp.read()\n",
        "\n",
        "  mystr = data.decode(\"utf8\")\n",
        "  fp.close()\n",
        "\n",
        "  return mystr\n",
        "\n",
        "def getSudokuPuzzle():\n",
        "  '''\n",
        "  Gets a random sudoku puzzle from websudoku.com\n",
        "  returns puzzle, solved answer\n",
        "  '''\n",
        "  src = getHtml(\"http://grid.websudoku.com\")\n",
        "  soup = BeautifulSoup(src)\n",
        "\n",
        "  getInputValue = lambda id : soup.find(\"input\", {\"id\": id}).get('value')\n",
        "  solved = getInputValue(\"cheat\")\n",
        "  mask = getInputValue(\"editmask\")\n",
        "  puzzle = []\n",
        "  for i in range(len(mask)):\n",
        "    if mask[i] == \"0\":\n",
        "      puzzle.append(solved[i])\n",
        "    elif mask[i] == \"1\":\n",
        "      puzzle.append(\"0\")\n",
        "  puzzle = ''.join(puzzle)\n",
        "\n",
        "  return [int(x) for x in puzzle], solved\n",
        "\n",
        "def displaySudoku(puzzle, mask = None):\n",
        "  '''\n",
        "  displays a sudoku puzzle on stdout\n",
        "  '''\n",
        "  output = []\n",
        "  for i in range(9):\n",
        "    if i == 3 or i == 6:\n",
        "      output.append('------+-------+------\\n')\n",
        "    for j in range(9):\n",
        "      if j == 3 or j == 6:\n",
        "        output.append('| ')\n",
        "      output.append(str(puzzle[9 * i + j]) + ' ')\n",
        "    output.append('\\n')\n",
        "  print(''.join(output))"
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "qJ5udB35vSxX",
        "colab_type": "code",
        "outputId": "1210caa8-4298-462a-e9c2-4f3d6343c5c5",
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 238
        }
      },
      "source": [
        "puzzle, solved = getSudokuPuzzle()\n",
        "print(\"PUZZLE:\")\n",
        "displaySudoku(puzzle)"
      ],
      "execution_count": 7,
      "outputs": [
        {
          "output_type": "stream",
          "text": [
            "PUZZLE:\n",
            "5 0 3 | 9 0 4 | 1 0 0 \n",
            "2 0 0 | 0 3 0 | 0 0 0 \n",
            "0 8 1 | 7 0 5 | 0 2 0 \n",
            "------+-------+------\n",
            "8 0 7 | 0 0 0 | 3 0 0 \n",
            "0 9 0 | 3 0 1 | 0 4 0 \n",
            "0 0 2 | 0 0 0 | 5 0 1 \n",
            "------+-------+------\n",
            "0 2 0 | 5 0 9 | 6 3 0 \n",
            "0 0 0 | 0 7 0 | 0 0 5 \n",
            "0 0 9 | 8 0 6 | 2 0 7 \n",
            "\n"
          ],
          "name": "stdout"
        }
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "zV2DB_IuYO3C",
        "colab_type": "text"
      },
      "source": [
        "**Let p(i, j, n) be a proposition that is true when number n is in cell ith row, jth column.**\n",
        "\n",
        "Here are the constraints:\n",
        "1. For each cell with known value, we assert `p(i, j, n) = true`.\n",
        "2. Assert that every row contains every number $\\bigwedge\\limits_{i=1}^9\\bigwedge\\limits_{n=1}^9 \\bigvee\\limits_{j=1}^9 p(i, j, n)$.\n",
        "3. Assert that every column contains every number $\\bigwedge\\limits_{j=1}^9\\bigwedge\\limits_{n=1}^9 \\bigvee\\limits_{i=1}^9 p(i, j, n)$.\n",
        "4. Assert that each 3x3 block contains every number $\\bigwedge\\limits_{r=0}^2\\bigwedge\\limits_{s=0}^2\\bigwedge\\limits_{n=1}^9\\bigvee\\limits_{i=1}^3\\bigvee\\limits_{j=1}^3 p(3r + i, 3s + j, n)$\n",
        "3. Assert that no cell contains more than one number by taking conjuction over all n, n', i, j from 1 to 9 where $n\\neq n'$ if $p(i, n) \\implies \\neg p(i, n')$.\n",
        "\n",
        "We have 9x9x9 = 729 variables"
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "uixOTebec5VM",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "def solve_sudoku(puzzle):\n",
        "\n",
        "  def p(i, j, n):\n",
        "    # each cell has 9 associated values\n",
        "    return 81 * (i-1) + 9 * (j-1) + n\n",
        "    \n",
        "  clauses = []\n",
        "\n",
        "  # step 1\n",
        "  for i in range(1, 10):\n",
        "    for j in range(1, 10):\n",
        "      digit = puzzle[9 * (i-1) + j - 1]\n",
        "      if digit:\n",
        "        clauses.append([p(i, j, digit)])\n",
        "\n",
        "  # step 2\n",
        "  for i in range(1, 10):\n",
        "    for n in range(1, 10):\n",
        "      q = []\n",
        "      for j in range(1, 10):\n",
        "        q.append(p(i, j, n))\n",
        "      clauses.append(q)\n",
        "\n",
        "  # step 3\n",
        "  for j in range(1, 10):\n",
        "    for n in range(1, 10):\n",
        "      q = []\n",
        "      for i in range(1, 10):\n",
        "        q.append(p(i, j, n))\n",
        "      clauses.append(q)\n",
        "\n",
        "  # step 4\n",
        "  for r in range(3):\n",
        "    for s in range(3):\n",
        "      for n in range(1, 10):\n",
        "        q = []\n",
        "        for i in range(1, 4):\n",
        "          for j in range(1, 4):\n",
        "            q.append(p(3 * r + i, 3 * s + j, n))\n",
        "        clauses.append(q)\n",
        "\n",
        "  # step 5\n",
        "  for i in range(1, 10):\n",
        "    for j in range(1, 10):\n",
        "      for n in range(1, 10):\n",
        "        for n_not in range(1, 10):\n",
        "          if n == n_not:\n",
        "            continue\n",
        "          clauses.append([-p(i, j, n), -p(i, j, n_not)])\n",
        "\n",
        "  sol = pycosat.solve(clauses)\n",
        "\n",
        "  # convert to sudoku list\n",
        "  output = []\n",
        "  for i in sol:\n",
        "    if i > 0:\n",
        "      number = i % 9\n",
        "      if number == 0:\n",
        "        number = 9\n",
        "      output.append(number)\n",
        "  return output"
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "62XN-la0qY_e",
        "colab_type": "code",
        "outputId": "bc9a9773-9b75-43db-fd9b-239be71b95eb",
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 221
        }
      },
      "source": [
        "solution = solve_sudoku(puzzle)\n",
        "displaySudoku(solution)"
      ],
      "execution_count": 9,
      "outputs": [
        {
          "output_type": "stream",
          "text": [
            "5 6 3 | 9 2 4 | 1 7 8 \n",
            "2 7 4 | 1 3 8 | 9 5 6 \n",
            "9 8 1 | 7 6 5 | 4 2 3 \n",
            "------+-------+------\n",
            "8 1 7 | 4 5 2 | 3 6 9 \n",
            "6 9 5 | 3 8 1 | 7 4 2 \n",
            "4 3 2 | 6 9 7 | 5 8 1 \n",
            "------+-------+------\n",
            "7 2 8 | 5 1 9 | 6 3 4 \n",
            "1 4 6 | 2 7 3 | 8 9 5 \n",
            "3 5 9 | 8 4 6 | 2 1 7 \n",
            "\n"
          ],
          "name": "stdout"
        }
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "PZmyJPjh2QNn",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "assert(solved == ''.join([str(x) for x in solution]))"
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "W42SeWHh2EHn",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        ""
      ],
      "execution_count": 0,
      "outputs": []
    }
  ]
}