examples/3coloring-sat.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Solving the problem of 3-coloring using SAT\n",
    "\n",
    "This is a small example to show how you can encode the problem of [3-coloring](https://en.wikipedia.org/wiki/Graph_coloring#Vertex_coloring) into SAT and using a SAT solver to solve the problem.\n",
    "\n",
    "We will use the [pysat](https://pysathq.github.io/) Python library for this (see this [example](sat.ipynb) for details on how to set this up). Let's start by importing some relevant things, and to create a CNF formula."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "from pysat.formula import CNF\n",
    "from pysat.solvers import MinisatGH\n",
    "\n",
    "formula = CNF();"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 3-coloring\n",
    "\n",
    "In the problem of 3-coloring, you are given as input a finite (undirected) [graph](https://en.wikipedia.org/wiki/Graph_(discrete_mathematics)) $G = (V,E)$, consisting of a set $V$ of *vertices* (or *nodes*) and a set $E$ of *edges*. Each edge $e \\in E$ consists of a set $\\{v_1,v_2\\}$ of exactly two vertices in $V$.\n",
    "\n",
    "A *coloring* of a graph $G = (V,E)$ is a function $\\mu : V \\rightarrow C$ that assigns to each vertex $v \\in V$ a color $\\mu(v) \\in C$. The coloring $\\mu$ is called *proper* if for every edge $\\{v_1,v_2\\} \\in E$, the coloring assigns different colors to the two endpoints of the edge—that is, $\\mu(v_1) \\neq \\mu(v_2)$.\n",
    "\n",
    "In the problem of 3-coloring, the question is to decide if there exists a proper coloring $\\mu : V \\rightarrow \\{1,2,3\\}$ of the graph that only uses three colors.\n",
    "\n",
    "## Encoding the graph and colorings\n",
    "\n",
    "Take some graph $G = (V,E)$, that comprises an input for the 3-coloring problem.\n",
    "Suppose that the vertices $V = \\{ v_1,\\dotsc,v_n \\}$ are numbered from $1$ to $n$.\n",
    "\n",
    "We will encode this graph in Python in the following way.\n",
    "\n",
    "To explain this, take the following example graph $G = (V,E)$, where $V = \\{v_1,v_2,v_3,v_4\\}$ and $E = \\{ \\{v_1,v_2\\}, \\{v_1,v_3\\}, \\{v_2,v_3\\}, \\{v_2,v_4\\}, \\{v_3,v_4\\} \\}$. We encode the set of edges as a list of pairs, where each vertex is indicated by its index. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "num_vertices = 4;\n",
    "edges = [(1,2),(1,3),(2,3),(2,4),(3,4)];"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Then, we will have to represent the possible 3-colorings of the graph $G$ using propositional variables. We will do this as follows. For each vertex $v_i$ and each color $c$, we will have a propositional variable $p_{i,c}$ that indicates whether $v_i$ gets colored with color $c$.\n",
    "\n",
    "Since propositional variables are indicated by a single positive integer in pysat, we define a function that assigns to each such variable $p_{i,c}$ a unique index."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "num_colors = 3;\n",
    "def var_number(i, c):\n",
    "    return ((i-1)*num_colors)+c;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Then, to ensure that the truth value given to these propositional variables corresponds to a 3-coloring of the graph, we will need to add some clauses to the CNF formula.\n",
    "\n",
    "We begin by adding, for each vertex $v_i$, a clause that states that there must be at least one $c$ for which $p_{i,c}$ is true.\n",
    "For each $v_i$, we add the clause: $(p_{i,1} \\vee p_{i,2} \\vee p_{i,3})$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [],
   "source": [
    "for i in range(1,num_vertices+1):\n",
    "    clause = [];\n",
    "    for c in range(1,num_colors+1):\n",
    "        clause.append(var_number(i,c));\n",
    "    formula.append(clause);"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Then, we add, for each vertex $v_i$ several clauses, that (together) state that there must be at most one $c$ for which $p_{i,c}$ is true. For each $v_i$, we add the clauses: $(\\neg p_{i,1} \\vee \\neg p_{i,2})$, $(\\neg p_{i,1} \\vee \\neg p_{i,3})$, $(\\neg p_{i,2} \\vee \\neg p_{i,3})$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [],
   "source": [
    "for i in range(1,num_vertices+1):\n",
    "    for c1 in range(1,num_colors+1):\n",
    "        for c2 in range(c1+1,num_colors+1):\n",
    "            clause = [-1*var_number(i,c1), -1*var_number(i,c2)];\n",
    "            formula.append(clause);"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Together, the above two sets of clauses ensure that for each vertex $v_i$, there is exactly one color $c$ such that $p_{i,c}$ is true. In other words, the truth assignments satisfying these clauses correspond exactly to all possible 3-colorings of the vertices $v_1,\\dotsc,v_4$.\n",
    "\n",
    "## Ensuring that colorings are proper\n",
    "\n",
    "To make sure that only truth assignments are allowed that correspond to *proper* 3-colorings, we need to add some further clauses.\n",
    "\n",
    "For each edge $\\{ v_{i_1},v_{i_2} \\} \\in E$, and each color $c$, we add a clause that states that the vertices $v_{i_1}$ and $v_{i_2}$ do not both get colored with color $c$.\n",
    "For each edge $\\{ v_{i_1},v_{i_2} \\} \\in E$, we add the clauses: $(\\neg p_{i_1,1} \\vee \\neg p_{i_2,1})$, $(\\neg p_{i_1,2} \\vee \\neg p_{i_2,2})$, $(\\neg p_{i_1,3} \\vee \\neg p_{i_2,3})$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [],
   "source": [
    "for (i1,i2) in edges:\n",
    "    for c in range(1,num_colors+1):\n",
    "        clause = [-1*var_number(i1,c), -1*var_number(i2,c)];\n",
    "        formula.append(clause);"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Calling the SAT solver and constructing a coloring\n",
    "\n",
    "All together, the clauses that we added ensure the following. Every truth assignment that satisfies these clauses (if such a truth assignment exists) corresponds to a proper 3-coloring of the graph $G$. Therefore, we can now call the SAT solver to find a satisfying truth assignment, if it exists. And if it exists, we can use it to construct a proper 3-coloring of the graph.\n",
    "\n",
    "For our simple example, a satisfying truth assignment exists, and we get a proper 3-coloring of the graph."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "The graph is 3-colorable:\n",
      "- Vertex 1 gets color 1\n",
      "- Vertex 2 gets color 3\n",
      "- Vertex 3 gets color 2\n",
      "- Vertex 4 gets color 1\n"
     ]
    }
   ],
   "source": [
    "solver = MinisatGH();\n",
    "solver.append_formula(formula);\n",
    "\n",
    "answer = solver.solve();\n",
    "\n",
    "if answer == True:\n",
    "    print(\"The graph is 3-colorable:\");\n",
    "    model = solver.get_model();\n",
    "    for i in range(1,num_vertices+1):\n",
    "        for c in range(1,num_colors+1):\n",
    "            if var_number(i,c) in model:\n",
    "                print(\"- Vertex {} gets color {}\".format(i,c));\n",
    "else:\n",
    "    print(\"The graph is not 3-colorable.\");\n"
   ]
  }
 ],
 "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.7.7"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}