Proofdoku Saturation.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In this notebook, I half-heartedly try to explain the use of a *saturation* encoding in [Proofdoku](http://proofdoku.com/). In Proofdoku, the player uses logic based on the rules of Sudoku to make arguments for the unique value of unfilled cells. An argument is valid if, when constructing a puzzle board from just the given evidence cells, the value of the conclusion cell is unambiguous (other cells may be ambiguous / have multiple valid fills)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Basic Rules\n",
    "The program below describes the primary rules of Sudoku. On a 9x9 board, each cell contains a number between 1 and 9. Numbers are not repeated within a row, column, or 3x3 cage. Clue cells, provided at the start of the puzzle, must be filled in the way specified."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Overwriting board.lp\n"
     ]
    }
   ],
   "source": [
    "%%file board.lp\n",
    "\n",
    "num(1..9).\n",
    "  \n",
    "cage(I,J, ((((I-1) / 3) * 3) + ((J-1) / 3)) + 1) :- num(I); num(J).\n",
    "              \n",
    "1 { fill(I,J, D): num(D) } 1 :- num(I); num(J). % one per cell\n",
    "1 { fill(I,J, D): num(I) } 1 :- num(D); num(J). % one per row\n",
    "1 { fill(I,J, D): num(J) } 1 :- num(I); num(D). % one per col\n",
    "1 { fill(I,J, D): cage(I,J,C) } 1 :- num(C); num(D). % one per cage\n",
    "              \n",
    "fill(I,J, D) :- clue(I,J, D)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Puzzle Instance\n",
    "The program below specifies the 38 clues that define a specific easy-difficulty puzzle."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Overwriting clues.lp\n"
     ]
    }
   ],
   "source": [
    "%%file clues.lp\n",
    "clue(1,1,1).\n",
    "clue(1,4,3).\n",
    "clue(1,5,2).\n",
    "clue(1,6,9).\n",
    "clue(1,7,6).\n",
    "clue(2,2,8).\n",
    "clue(2,3,9).\n",
    "clue(2,4,1).\n",
    "clue(2,5,6).\n",
    "clue(2,8,7).\n",
    "clue(3,1,6).\n",
    "clue(3,3,2).\n",
    "clue(3,7,4).\n",
    "clue(3,9,9).\n",
    "clue(4,2,7).\n",
    "clue(4,3,8).\n",
    "clue(4,5,1).\n",
    "clue(4,6,6).\n",
    "clue(5,1,4).\n",
    "clue(5,4,7).\n",
    "clue(5,7,1).\n",
    "clue(5,8,6).\n",
    "clue(6,1,3).\n",
    "clue(6,8,5).\n",
    "clue(6,9,8).\n",
    "clue(7,1,9).\n",
    "clue(7,3,3).\n",
    "clue(7,6,1).\n",
    "clue(7,7,8).\n",
    "clue(7,9,6).\n",
    "clue(8,2,2).\n",
    "clue(8,3,1).\n",
    "clue(8,5,9).\n",
    "clue(8,8,4).\n",
    "clue(9,3,4).\n",
    "clue(9,4,2).\n",
    "clue(9,5,8).\n",
    "clue(9,6,3)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Basic Puzzle Solving\n",
    "Combining the problem instance with the Sudoku rules, we have a Sudoku solver which will find a legal filling for all 81 cells."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "clingo version 5.2.0\r\n",
      "Reading from board.lp ...\r\n",
      "Solving...\r\n",
      "Answer: 1\r\n",
      "fill(1,1,1) fill(8,3,1) fill(2,4,1) fill(4,5,1) fill(7,6,1) fill(5,7,1) fill(8,2,2) fill(3,3,2) fill(9,4,2) fill(1,5,2) fill(6,1,3) fill(7,3,3) fill(1,4,3) fill(9,6,3) fill(5,1,4) fill(9,3,4) fill(3,7,4) fill(8,8,4) fill(6,8,5) fill(3,1,6) fill(2,5,6) fill(4,6,6) fill(1,7,6) fill(5,8,6) fill(7,9,6) fill(4,2,7) fill(5,4,7) fill(2,8,7) fill(2,2,8) fill(4,3,8) fill(9,5,8) fill(7,7,8) fill(6,9,8) fill(7,1,9) fill(2,3,9) fill(8,5,9) fill(1,6,9) fill(3,9,9) fill(2,1,5) fill(4,1,2) fill(8,1,8) fill(9,1,7) fill(1,2,4) fill(3,2,3) fill(5,2,9) fill(6,2,1) fill(7,2,5) fill(9,2,6) fill(1,3,7) fill(5,3,5) fill(6,3,6) fill(3,4,8) fill(4,4,5) fill(6,4,9) fill(7,4,4) fill(8,4,6) fill(3,5,5) fill(5,5,3) fill(6,5,4) fill(7,5,7) fill(2,6,4) fill(3,6,7) fill(5,6,8) fill(6,6,2) fill(8,6,5) fill(2,7,2) fill(4,7,9) fill(6,7,7) fill(8,7,3) fill(9,7,5) fill(1,8,8) fill(3,8,1) fill(4,8,3) fill(7,8,2) fill(9,8,9) fill(1,9,5) fill(2,9,3) fill(4,9,4) fill(5,9,2) fill(8,9,7) fill(9,9,1)\r\n",
      "SATISFIABLE\r\n",
      "\r\n",
      "Models       : 1\r\n",
      "Calls        : 1\r\n",
      "Time         : 0.021s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)\r\n",
      "CPU Time     : 0.021s\r\n"
     ]
    }
   ],
   "source": [
    "!echo \"#show fill/3.\" > show-fill.lp\n",
    "!clingo board.lp clues.lp show-fill.lp"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Argument Definition\n",
    "We should now model the idea that a Proofdoku argument consists of one or more premise cells (taken from the available clues) and exactly one conclusion cell (not a clue cell)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Overwriting argument-definition.lp\n"
     ]
    }
   ],
   "source": [
    "%%file argument-definition.lp\n",
    "\n",
    "clued(I,J) :- clue(I,J,D).\n",
    "\n",
    "% guess a premise set and conclusion cell\n",
    "1 { premise(I,J): clued(I,J) }. \n",
    "1 { conclusion(I,J): num(I), num(J), not clued(I,J) } 1.\n",
    "\n",
    "#show conclusion/2.\n",
    "#show premise/2."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "With this, we can generate many arguments that are syntactically valid but semanitically unsound (they don't contain enough evidence or the right evidence to uniquely define the fill of the conclusion cell). Intuitively, there's no valid argument that involves less than four premises, and some of the arguments below don't even have that."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {
    "scrolled": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "clingo version 5.2.0\r\n",
      "Reading from clues.lp ...\r\n",
      "Solving...\r\n",
      "Answer: 1\r\n",
      "premise(1,4) conclusion(2,1)\r\n",
      "Answer: 2\r\n",
      "premise(1,5) conclusion(2,1)\r\n",
      "Answer: 3\r\n",
      "premise(1,4) premise(1,5) conclusion(2,1)\r\n",
      "Answer: 4\r\n",
      "premise(1,6) conclusion(2,1)\r\n",
      "Answer: 5\r\n",
      "premise(1,5) premise(1,6) conclusion(2,1)\r\n",
      "Answer: 6\r\n",
      "premise(1,4) premise(1,6) conclusion(2,1)\r\n",
      "Answer: 7\r\n",
      "premise(1,4) premise(1,5) premise(1,6) conclusion(2,1)\r\n",
      "Answer: 8\r\n",
      "premise(1,7) conclusion(2,1)\r\n",
      "Answer: 9\r\n",
      "premise(1,6) premise(1,7) conclusion(2,1)\r\n",
      "Answer: 10\r\n",
      "premise(1,4) premise(1,7) conclusion(2,1)\r\n",
      "SATISFIABLE\r\n",
      "\r\n",
      "Models       : 10+\r\n",
      "Calls        : 1\r\n",
      "Time         : 0.021s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)\r\n",
      "CPU Time     : 0.021s\r\n"
     ]
    }
   ],
   "source": [
    "!clingo clues.lp board.lp argument-definition.lp 10"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Argument Validity by Saturation\n",
    "In this program, we'll check that the argument was valid by exhausting the space of counterarguments that would defeat it.\n",
    "\n",
    "A counterargument here consists of an alternative way of filling in the board that satisfies three conditions:\n",
    "- It *agrees* with all of the premises in the candidate argument.\n",
    "- It *disagrees* with the conclusion.\n",
    "- It follows the normal rules for a valid Sudoku board.\n",
    "\n",
    "We'll use disjunctive rules to attempt to describe that alternate board. If the counterargument is invalid, we'll intentionally blow it up into a maximal description by putting every number in every cell -- saturating it. If an argument is invalid, it will admit a set of fills which is a subset of the saturated set. The disjunctive solver will ensure we don't see the saturated case if it was avoidable. Finally, we'll use an integrity constraint to ensure we see the saturated case. This will filter the available arguments to just those that don't admit a counterargument."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Overwriting argument-validity.lp\n"
     ]
    }
   ],
   "source": [
    "%%file argument-validity.lp\n",
    "\n",
    "% Use a disjunctive rule to generate an alternative board\n",
    "alt_fill(I,J,D): num(D) :- num(I); num(J).\n",
    "\n",
    "% The board is not a counterargument if it doesn't agree with the premises\n",
    "bot :- alt_fill(I,J,D); premise(I,J); not fill(I,J,D).\n",
    "    \n",
    "% Or if it does agree with the conclusion\n",
    "bot :- alt_fill(I,J,D); conclusion(I,J); fill(I,J,D). \n",
    "\n",
    "% Or it violates one of the traditional Sudoku rules\n",
    "bot :- 2 { alt_fill(I,J,D): num(D) }; num(I); num(J).\n",
    "bot :- 2 { alt_fill(I,J,D): num(I) }; num(D); num(J).\n",
    "bot :- 2 { alt_fill(I,J,D): num(J) }; num(I); num(D).\n",
    "bot :- 2 { alt_fill(I,J,D): cage(I,J,C) }; num(C); num(D).\n",
    "\n",
    "% If it was a broken counterargument for any reason, saturate it\n",
    "alt_fill(I,J,D) :- bot; num(I); num(J); num(D).\n",
    "\n",
    "% Only show solutions which are saturated\n",
    ":- not bot."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "clingo version 5.2.0\n",
      "Reading from clues.lp ...\n",
      "Solving...\n",
      "Answer: 1\n",
      "conclusion(8,1) premise(6,9) premise(3,9) premise(8,8) premise(6,8) premise(5,8) premise(7,7) premise(5,7) premise(3,7) premise(1,7) premise(7,6) premise(9,5) premise(8,5) premise(4,5) premise(9,4) premise(9,3) premise(4,3) premise(2,2) premise(6,1) premise(3,1)\n",
      "SATISFIABLE\n",
      "\n",
      "Models       : 1+\n",
      "Calls        : 1\n",
      "Time         : 0.207s (Solving: 0.08s 1st Model: 0.08s Unsat: 0.00s)\n",
      "CPU Time     : 0.206s\n"
     ]
    }
   ],
   "source": [
    "!clingo clues.lp board.lp argument-definition.lp argument-validity.lp"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Argument Minimization\n",
    "The formulation above allows sound arguments that might contain more evidence than necessary. It might be natural to ask for an example of the smallest valid argument (in a counting sense of smallness). We can accomplish this with a basic `#minimize` directive or weight constraints (\"`:~`\"). The formulation with a weak constraint below finds a solution involving just four points of evidence (premise cells)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {
    "scrolled": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "clingo version 5.2.0\n",
      "Reading from clues.lp ...\n",
      "Solving...\n",
      "Answer: 19\n",
      "conclusion(7,8) premise(7,9) premise(7,7) premise(9,4) premise(8,2)\n",
      "Optimization: 4\n",
      "OPTIMUM FOUND\n",
      "\n",
      "Models       : 19\n",
      "  Optimum    : yes\n",
      "Optimization : 4\n",
      "Calls        : 1\n",
      "Time         : 1.259s (Solving: 1.14s 1st Model: 0.15s Unsat: 0.07s)\n",
      "CPU Time     : 1.256s\n"
     ]
    }
   ],
   "source": [
    "!echo \":~ premise(I,J). [1,I,J]\" > min-premises.lp\n",
    "!clingo clues.lp board.lp argument-definition.lp argument-validity.lp min-premises.lp --quiet=1"
   ]
  }
 ],
 "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.6.1"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}