{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "from collections import defaultdict, deque"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## algorithm"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "def knowledge_base(formulas):\n",
    "    rules, variable, dependency = [], defaultdict(bool), defaultdict(list)\n",
    "\n",
    "    def _clause(formula):\n",
    "        # A, B, C => P\n",
    "        neg, pos = formula.replace(' ', '').split('=>')\n",
    "        neg, pos = set(neg.split('&')) - {''}, pos or None\n",
    "\n",
    "        # add rule\n",
    "        rules.append((neg, pos))\n",
    "        \n",
    "        # set variable and track dependencies\n",
    "        for i in neg:\n",
    "            dependency[i].append((neg, pos))\n",
    "\n",
    "    # parse formulas and build knowledge base\n",
    "    deque((_clause(i) for i in formulas.split('\\n') if i), 0)\n",
    "    \n",
    "    return rules, variable, dependency"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "def resolution(rules, variable, dependency):\n",
    "    # initial variables that have to be satisfied\n",
    "    to_satisfy = [(neg, pos) for neg, pos in rules if not neg]\n",
    "\n",
    "    while to_satisfy:\n",
    "        neg, pos = to_satisfy.pop()\n",
    "\n",
    "        # contradiction: true => false\n",
    "        if not pos:\n",
    "            return False\n",
    "\n",
    "        # satisfy variable\n",
    "        variable[pos] = True\n",
    "\n",
    "        # update dependent rules\n",
    "        for d_neg, d_pos in dependency[pos]:\n",
    "            d_neg.remove(pos)\n",
    "            \n",
    "            # next variable to be satisfied\n",
    "            if not d_neg and d_pos not in variable:\n",
    "                to_satisfy.append((d_neg, d_pos))\n",
    "\n",
    "    return True"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "def hornsat(formulas):\n",
    "    rules, variable, dependency = knowledge_base(formulas)\n",
    "    satisfiable = resolution(rules, variable, dependency)\n",
    "\n",
    "    print(['CONTRADICTION', 'SATISFIABLE'][satisfiable])\n",
    "    print(', '.join('%s=%s' % i for i in variable.items()))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## run"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "SATISFIABLE\n",
      "X=True, Y=True, Z=True\n"
     ]
    }
   ],
   "source": [
    "hornsat(\"\"\"\n",
    "X => Y\n",
    "Y => Z\n",
    "=> X\n",
    "\"\"\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "CONTRADICTION\n",
      "X=True, Y=True\n"
     ]
    }
   ],
   "source": [
    "hornsat(\"\"\"\n",
    "X => Y\n",
    "Y => X\n",
    "=> X\n",
    "Y =>\n",
    "\"\"\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "SATISFIABLE\n",
      "R=True, S=True, P=True\n"
     ]
    }
   ],
   "source": [
    "hornsat(\"\"\"\n",
    "P & Q & R & S => X\n",
    "P & Q => R\n",
    "R => S\n",
    "X =>\n",
    "=> P\n",
    "=> R\n",
    "\"\"\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "CONTRADICTION\n",
      "Q=True, P=True, R=True, S=True, X=True\n"
     ]
    }
   ],
   "source": [
    "hornsat(\"\"\"\n",
    "P & Q & R & S => X\n",
    "P & Q => R\n",
    "R => S\n",
    "X =>\n",
    "=> P\n",
    "=> Q\n",
    "\"\"\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "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.0"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}