examples/ds-asp.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Solving Dominating Set using ASP\n",
    "\n",
    "This is a small example to show how you can encode the problem of [Dominating Set](https://en.wikipedia.org/wiki/Dominating_set) into ASP and using an ASP solver to solve the problem.\n",
    "\n",
    "We will use [clingo](https://potassco.org/clingo/) in Python for this. Have a look at [these instructions](asp.ipynb) to see how you can use clingo from Python.\n",
    "\n",
    "Let's start off with an empty string, that we will fill with an answer set program."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "import clingo\n",
    "\n",
    "asp_code = \"\";"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Dominating set\n",
    "\n",
    "In the problem of *Dominating Set (DS)*, 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$. In addition, you are given as input a positive integer $k \\in \\mathbb{N}$.\n",
    "\n",
    "A *dominating set* of a graph $G = (V,E)$ is a subset $D \\subseteq V$ of vertices such that for every vertex $v \\in V$ holds that either (1) $v$ is in the set $D$ (i.e., $v \\in D$), or (2) there exists some vertex $u \\in D$ that is connected with an edge to $v$ (i.e., $u \\in D$ and $\\{ u,v \\} \\in E$).\n",
    "\n",
    "In the problem of dominating set, the question is to decide if there exists dominating set $D \\subseteq V$ of the graph $G$ that is of size $k$.\n",
    "\n",
    "## Encoding graphs in ASP\n",
    "\n",
    "To encode this problem in ASP, we first show how to encode a given graph in ASP.\n",
    "\n",
    "Take the following example graph $G = (V,E)$, where $V = \\{v_1,v_2,v_3,v_4,v_5,v_6,v_7\\}$ and $E = \\{ \\{v_1,v_2\\}, \\{v_1,v_3\\}, \\{v_2,v_3\\}, \\{v_3,v_4\\}, \\{v_4,v_5\\}, \\{v_5,v_6\\}, \\{v_5,v_7\\}, \\{v_6,v_7\\} \\}$. We can encode this in ASP using predicates `vertex/1` and `edge/2` as follows."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "asp_code += \"\"\"\n",
    "    vertex(v1).\n",
    "    vertex(v2).\n",
    "    vertex(v3).\n",
    "    vertex(v4).\n",
    "    vertex(v5).\n",
    "    vertex(v6).\n",
    "    vertex(v7).\n",
    "    edge(v1,v2).\n",
    "    edge(v1,v3).\n",
    "    edge(v2,v3).\n",
    "    edge(v3,v4).\n",
    "    edge(v4,v5).\n",
    "    edge(v5,v6).\n",
    "    edge(v5,v7).\n",
    "    edge(v6,v7).\n",
    "\"\"\";"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To make things easier, let's also add a rule that states that whenever `edge(U,V)` is true, also `edge(V,U)` is true. This way, we don't have to worry about the order of the vertices in the edges that we declare."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "asp_code += \"\"\"\n",
    "    edge(U,V) :- edge(V,U).\n",
    "\"\"\";"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Guessing a subset of $k$ vertices\n",
    "\n",
    "We will use a guess-and-check approach to model the problem of dominating set. In particular, we will add some rules to the answer set program that will guess a set of $k$ vertices, and then after that we will add some constraints that ensure that the set of vertices that we guessed is a dominating set.\n",
    "\n",
    "We guess the set of $k$ vertices as follows. We declare a constant `k` (with `k=3` for our example), and then we state that among the values for `V` for which `vertex(V)` is true, there are exactly `k` for which also `chosen(V)` is true."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [],
   "source": [
    "k = 3;\n",
    "asp_code += \"#const k={}.\".format(k)\n",
    "asp_code += \"\"\"\n",
    "    k { chosen(V) : vertex(V) } k.\n",
    "\"\"\""
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Verifying that the set dominates all vertices\n",
    "\n",
    "We now add rules and constraints expressing that the guessed set dominates all vertices in the graph.\n",
    "\n",
    "Firstly, we define a predicate `dominated/1` that is true for all vertices `V` that are dominated. We have two rules: the first one expresses that every chosen vertex is dominated, and the second one expresses that every vertex connected with an edge to a chosen vertex is dominated.\n",
    "\n",
    "Finally, we add a constraint that says that every vertex must be dominated."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [],
   "source": [
    "asp_code += \"\"\"\n",
    "    dominated(V) :- vertex(V), chosen(V).\n",
    "    dominated(V) :- vertex(V), chosen(U), edge(U,V).\n",
    "    :- vertex(V), not dominated(V).\n",
    "\"\"\""
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Showing the coloring\n",
    "\n",
    "Finally, we add a `#show` statement that indicates that we are only interested in the predicate `chosen/1`, and we ask clingo to print out some (say, 10) of the dominating sets of the graph of size $k$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {
    "scrolled": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[chosen(v1), chosen(v2), chosen(v5)]\n",
      "[chosen(v1), chosen(v3), chosen(v5)]\n",
      "[chosen(v2), chosen(v3), chosen(v5)]\n",
      "[chosen(v1), chosen(v4), chosen(v5)]\n",
      "[chosen(v2), chosen(v4), chosen(v5)]\n",
      "[chosen(v3), chosen(v4), chosen(v5)]\n",
      "[chosen(v1), chosen(v3), chosen(v7)]\n",
      "[chosen(v2), chosen(v3), chosen(v7)]\n",
      "[chosen(v1), chosen(v4), chosen(v7)]\n",
      "[chosen(v2), chosen(v4), chosen(v7)]\n",
      "The graph has a dominating set of size k=3\n"
     ]
    }
   ],
   "source": [
    "asp_code += \"\"\"\n",
    "    #show chosen/1.\n",
    "\"\"\"\n",
    "\n",
    "control = clingo.Control();\n",
    "control.add(\"base\", [], asp_code);\n",
    "control.ground([(\"base\", [])])\n",
    "\n",
    "def on_model(model):\n",
    "    print(model.symbols(shown=True));\n",
    "\n",
    "control.configuration.solve.models = 10;\n",
    "answer = control.solve(on_model=on_model)\n",
    "\n",
    "if answer.satisfiable == True:\n",
    "    print(\"The graph has a dominating set of size k={}\".format(k));\n",
    "else:\n",
    "    print(\"The graph does not have a dominating set of size k={}\".format(k));"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Finding a smallest dominating set\n",
    "\n",
    "In the ASP encoding above, we gave a specific size $k$ of the dominating set that we were after. What we can also do, instead, is ask for the smallest dominating set for a given graph.\n",
    "\n",
    "To illustrate this, we start by encoding the example graph again."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [],
   "source": [
    "asp_code = \"\"\"\n",
    "    vertex(v1).\n",
    "    vertex(v2).\n",
    "    vertex(v3).\n",
    "    vertex(v4).\n",
    "    vertex(v5).\n",
    "    vertex(v6).\n",
    "    vertex(v7).\n",
    "    edge(v1,v2).\n",
    "    edge(v1,v3).\n",
    "    edge(v2,v3).\n",
    "    edge(v3,v4).\n",
    "    edge(v4,v5).\n",
    "    edge(v5,v6).\n",
    "    edge(v5,v7).\n",
    "    edge(v6,v7).\n",
    "    edge(U,V) :- edge(V,U).\n",
    "\"\"\";"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "For our definition of the predicate `dominated/1` and the constraint that all vertices should be dominated, we can do exactly as before.\n",
    "\n",
    "However, we allow any set of vertices to be selected using `chosen/1`, rather than specifying a specific number of vertices to be selected."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [],
   "source": [
    "asp_code += \"\"\"\n",
    "    { chosen(V) : vertex(V) }.\n",
    "    \n",
    "    dominated(V) :- vertex(V), chosen(V).\n",
    "    dominated(V) :- vertex(V), chosen(U), edge(U,V).\n",
    "    :- vertex(V), not dominated(V).\n",
    "\"\"\";"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Then, in addition, we add a `#minimize` statement, that minimizes the amount of vertices that are chosen.\n",
    "\n",
    "We also add a rule that counts the number of vertices that are chosen (and captures this using the predicate `size/1`)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [],
   "source": [
    "asp_code += \"\"\"\n",
    "    #minimize { 1,chosen(V) : chosen(V) }.\n",
    "    size(K) :- K = #count { chosen(V) : chosen(V) }.\n",
    "    \n",
    "    #show chosen/1.\n",
    "    #show size/1.\n",
    "\"\"\";"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Finally, we call the ASP solver, and extract the smallest dominating sets that are found (together with their size)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Smallest dominating set (of size 2): {v3, v7}\n",
      "Smallest dominating set (of size 2): {v3, v6}\n",
      "Smallest dominating set (of size 2): {v3, v5}\n",
      "Smallest dominating set (of size 2): {v1, v5}\n",
      "Smallest dominating set (of size 2): {v2, v5}\n"
     ]
    }
   ],
   "source": [
    "control = clingo.Control();\n",
    "control.add(\"base\", [], asp_code);\n",
    "control.ground([(\"base\", [])])\n",
    "\n",
    "def on_model(model):\n",
    "    if model.optimality_proven == True:\n",
    "        dominating_set = [];\n",
    "        size = 0;\n",
    "        for atom in model.symbols(shown=True):\n",
    "            if atom.name == \"chosen\":\n",
    "                dominating_set.append(str(atom.arguments[0]))\n",
    "            if atom.name == \"size\":\n",
    "                size = int(str(atom.arguments[0]));\n",
    "        print(\"Smallest dominating set (of size {}): {{{}}}\".format(size,\", \".join(dominating_set)));\n",
    "\n",
    "control.configuration.solve.opt_mode = \"optN\";\n",
    "control.configuration.solve.models = 0;\n",
    "\n",
    "answer = control.solve(on_model=on_model)"
   ]
  }
 ],
 "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
}