Symmetry-Degree-of-a-Query.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Imports"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "from PW_explorer.load_worlds import load_worlds\n",
    "from PW_explorer.run_clingo import run_clingo"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "from DLV_Input_Parser.dlv_rules_parser import parse_dlv_rules"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "application/javascript": [
       "IPython.CodeCell.options_default.highlight_modes['prolog'] = {'reg':[/^%%(clingo|dlv)/]};"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "%load_ext PWE_NB_Extension"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Implementation"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We know that the symmetry degree is defined as the number of automorphism groups of the incidence graph of a query. Below we define an encoding that finds all the automorphisms of a given graph."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "##### Automorphism Encoding"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [],
   "source": [
    "%%clingo --donot-display_input -lci automorphisms --donot-run\n",
    "\n",
    "% e(X,Y) :- e(Y,X). --> only if undirected\n",
    "gnode(X) :- e(X,_).\n",
    "gnode(X) :- e(_,X).\n",
    "\n",
    "vmap(X,Y) ; vout(X,Y) :- gnode(X), gnode(Y).\n",
    ":- vmap(X1,Y1), vmap(X2,Y2), e(X1,X2), not e(Y1,Y2).\n",
    ":- vmap(X1,Y1), vmap(X2,Y2), not e(X1,X2), e(Y1,Y2).\n",
    "\n",
    "% used1(X) :- vmap(X,_).\n",
    "% :- gnode(X), not used1(X).\n",
    "% :- vmap(X,Y),vmap(X,Z),Y!=Z.\n",
    "% :- vmap(Y,X),vmap(Z,X),Y!=Z.\n",
    "\n",
    ":- gnode(X), #count {Y: vmap(X,Y)} != 1.\n",
    ":- gnode(X), #count {Y: vmap(Y,X)} != 1.\n",
    "\n",
    "% #show vmap/2.\n",
    "#show."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [],
   "source": [
    "symm_degree_rules = str(automorphisms).split('\\n')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We can construct a incidence graph of query Q using the function below."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [],
   "source": [
    "def get_incidence_graph_edge_facts(rule):\n",
    "    listener = parse_dlv_rules(rule, print_parse_tree=False)\n",
    "    edges = []\n",
    "    for rule in listener.rules:\n",
    "        head_atoms, tail_atoms = rule[0], rule[1]\n",
    "        atom_count = 0\n",
    "        for head in head_atoms+tail_atoms:\n",
    "            atom_node = '\"{}_{}_{}\"'.format(head.rel_name, head.rel_arity, atom_count)\n",
    "            edges.extend([('\"{}\"'.format(v), atom_node) for v in head.vars])\n",
    "            atom_count += 1\n",
    "    edge_facts = []\n",
    "    for e in edges:\n",
    "        edge_facts.append(\"e({},{}).\".format(*e))\n",
    "    return edge_facts"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We now combine these two to find the symmetry degree."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [],
   "source": [
    "def get_symm_degree(rule):\n",
    "    edge_facts = get_incidence_graph_edge_facts(rule)\n",
    "#     print(edge_facts)\n",
    "    asp_out, _ = run_clingo(symm_degree_rules+edge_facts)\n",
    "    _, _, pw_objs = load_worlds(asp_out, silent=True)\n",
    "    return len(pw_objs)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Testing"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "6"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# tri/0\n",
    "get_symm_degree('tri :- e(X,Y), e(Y,Z), e(Z,X).')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "2"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# tri/1\n",
    "get_symm_degree('tri(X) :- e(X,Y), e(Y,Z), e(Z,X).')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "4"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# tri/2\n",
    "get_symm_degree('tri(X,Y) :- e(X,Y), e(Y,Z), e(Z,X).')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "6"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# tri/3\n",
    "get_symm_degree('tri(X,Y,Z) :- e(X,Y), e(Y,Z), e(Z,X).')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "2"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# thop/0\n",
    "get_symm_degree('thop :- hop(X,Z1), hop(Z1,Z2), hop(Z2,Y).')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "1"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# thop/1\n",
    "get_symm_degree('thop(X) :- hop(X,Z1), hop(Z1,Z2), hop(Z2,Y).')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "8"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# thop/2\n",
    "get_symm_degree('thop(X,Y) :- hop(X,Z1), hop(Z1,Z2), hop(Z2,Y).')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "1"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# thop/3\n",
    "get_symm_degree('thop(X,Y,Z1) :- hop(X,Z1), hop(Z1,Z2), hop(Z2,Y).')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "2"
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# thop/4\n",
    "get_symm_degree('thop(X,Y,Z1,Z2) :- hop(X,Z1), hop(Z1,Z2), hop(Z2,Y).')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "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.8"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}