k_cap_demo.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Package Import"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "import itertools\n",
    "import random\n",
    "import subprocess\n",
    "import os"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Function"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "def asign_k(k,generate):## inseart K to the generate part and return updated generate\n",
    "    gen_ls=generate.splitlines()\n",
    "    k_str='box(1..'+str(k)+').'\n",
    "    gen_ls.insert(1, k_str)\n",
    "    gen_update='\\n'.join(gen_ls)\n",
    "    return(gen_update)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "def str_to_lp(string,filename,problem):\n",
    "    if not os.path.exists(\"clingo_files\"):\n",
    "        os.makedirs(\"clingo_files\")\n",
    "    with open(\"clingo_files\"+\"/\"+problem+\"_\"+filename+\".lp\", \"w\") as text_file:\n",
    "        text_file.write(string)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [],
   "source": [
    "def run_clingo(instance, gen, check):\n",
    "    str_to_lp(instance,\"instance\",\"k_cap\")\n",
    "    str_to_lp(gen,\"generate\",\"k_cap\")\n",
    "    str_to_lp(check,\"check\",\"k_cap\")\n",
    "    command='bash -c \"clingo clingo_files/k_cap_instance.lp clingo_files/k_cap_generate.lp  clingo_files/k_cap_check.lp\"'\n",
    "    result=run_bash(command)\n",
    "    return(result)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [],
   "source": [
    "def run_bash(command):\n",
    "    stdout = subprocess.getoutput(command)\n",
    "    result=stdout.split(\"\\n\")[-6]\n",
    "    return(result)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# CAP Relationship"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<img src=\"img/cap_relationship.png\"> "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**conflict(R1,R2)**: requirement R1 and R2 are conflict\n",
    "\n",
    "Axiom: \n",
    "* has_conflict(R1,R2) ⇒ has_conflict(R2,R1) i.e., has_conflict/2 is symmetric\n",
    "* has_conflict is not (in general) transitive! \n",
    "* A requirement can have multiple conflicts (“M-N relationship”)\n",
    "\n",
    "**uses(M,R)**: Module M “needs” requirement R to run\n",
    "\n",
    "Axiom:\n",
    "* many-to-many relationship\n",
    "\n",
    "**on(M,B)**: module M will be run on box (i.e., container) B\n",
    "\n",
    "⇒ is it enough to install M only on one box? Or are there reasonable use cases to allow M to be installed on multiple boxes?\n",
    "\n",
    "If we allow more complex applications (such as workflows that are built using multiple modules), then it might be desirable to install a module M on multiple boxes (as required / useful for the workflow)\n",
    "But since we here consider M as the top-level application, we only need a single box to run M.\n",
    "So we can assume here that the functional dependency M → B holds!"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# M-R Instance"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<img src=\"img/cap_instance.png\"  width=\"600\"> "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Take the above instance as an example, we can translate it into clingo script"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [],
   "source": [
    "instance=\"\"\"\n",
    "uses(m1,r1).\n",
    "uses(m1,r4).\n",
    "uses(m2,r1).\n",
    "uses(m3,r2).\n",
    "uses(m3,r4).\n",
    "uses(m4,r2).\n",
    "uses(m4,r3).\n",
    "uses(m5,r2).\n",
    "\n",
    "has_conflict(r1,r2).\n",
    "has_conflict(r3,r4).\n",
    "\"\"\""
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# CAP Generate"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "For each module, there could be multiple boxes to choose from while every module M should be associated with exactly one box B (see the figure below)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<img src=\"img/cap_generate.png\" width=\"600\"/> "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [],
   "source": [
    "generate=\"\"\"\n",
    "mod(M) :- uses(M,_).\n",
    "%% This works: for each M, choose exactly one B:\n",
    "1 { on(M,B) : box(B) } 1  :- mod(M).\n",
    "\"\"\""
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# ASP Check"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [],
   "source": [
    "check=\"\"\"\n",
    "\n",
    "inst(B,R) :- on(M,B), uses(M,R).\n",
    " :- has_conflict(R1,R2), inst(B,R1), inst(B,R2).\n",
    "\n",
    "#show inst/2.\n",
    "\"\"\""
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Problem1: K_CAP"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    " Given a constant K, find all possible solutions to CAP with k containers"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [],
   "source": [
    "k=3"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [],
   "source": [
    "generate_update=asign_k(k,generate) # update generate with k boxes"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'SATISFIABLE'"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "run_clingo(instance, generate_update, check)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Problem2: min_K_CAP"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "container number: 1\n",
      "UNSATISFIABLE\n",
      "container number: 2\n",
      "UNSATISFIABLE\n",
      "container number: 3\n",
      "SATISFIABLE\n",
      "\n",
      "\n",
      "Minimum K for this instance is: 3\n"
     ]
    }
   ],
   "source": [
    "k=0\n",
    "clingo_output=\"\"\n",
    "#find the minimum number of containers to satisfy all\n",
    "while clingo_output!=\"SATISFIABLE\":\n",
    "    k=k+1  ## for other problems, the variables should be revised\n",
    "    print(\"container number: \"+str(k)) \n",
    "    generate_update=asign_k(k,generate) # update generate with k boxes\n",
    "    clingo_output=run_clingo(instance, generate_update, check)\n",
    "    print(clingo_output)\n",
    "print(\"\\n\\nMinimum K for this instance is: {}\".format(k))"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "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.8.12"
  },
  "toc": {
   "base_numbering": 1,
   "nav_menu": {},
   "number_sections": true,
   "sideBar": true,
   "skip_h1_title": false,
   "title_cell": "Table of Contents",
   "title_sidebar": "Contents",
   "toc_cell": false,
   "toc_position": {},
   "toc_section_display": true,
   "toc_window_display": false
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}