Skip to content

Instantly share code, notes, and snippets.

@rummanwaqar

rummanwaqar/sat_applications.ipynb

Created October 17, 2019 04:53
Show Gist options
  • Save rummanwaqar/4985fb5b5eebacf18ce5b0e0949fb1e8 to your computer and use it in GitHub Desktop.
Save rummanwaqar/4985fb5b5eebacf18ce5b0e0949fb1e8 to your computer and use it in GitHub Desktop.
Download ZIP
SAT_applications.ipynb
Display the source blob
Display the rendered blob
Raw
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": []
}
]
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment