algorithms2/week6/Week6.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "{-# LANGUAGE LambdaCase #-}\n",
    "\n",
    "import qualified Data.Graph          as G\n",
    "import qualified Data.HashMap.Strict as H\n",
    "import qualified Data.HashSet        as S\n",
    "import qualified Data.Array          as A\n",
    "\n",
    "import Prelude hiding (lookup)\n",
    "\n",
    "import Control.Monad.ST\n",
    "import Data.STRef\n",
    "import Control.Monad (forM_, when)\n",
    "import Data.Maybe (isNothing, fromJust)\n",
    "\n",
    "import Debug.Trace\n",
    "\n",
    "denormalise = subtract\n",
    "normalise   = (+)\n",
    "other n v = 2*n - v\n",
    "clauses n [u,v] = [(other n u, v), (other n v, u)]\n",
    "\n",
    "tarjan :: Int -> G.Graph -> [S.HashSet Int]\n",
    "tarjan n graph = runST $ do\n",
    "    index    <- newSTRef (0 :: Int)\n",
    "    stack    <- newSTRef []\n",
    "    stackSet <- newSTRef S.empty\n",
    "    indices  <- newSTRef H.empty\n",
    "    lowlinks <- newSTRef H.empty\n",
    "    output   <- newSTRef []\n",
    "\n",
    "    forM_ (G.vertices graph) $ \\v -> do\n",
    "        vIndex <- H.lookup v <$> readSTRef indices\n",
    "        when (isNothing vIndex) $\n",
    "            strongConnect n v graph index stack stackSet indices lowlinks output\n",
    "\n",
    "    readSTRef output\n",
    "\n",
    "\n",
    "strongConnect\n",
    "    :: (Num a, Ord a, Show a)\n",
    "    => Int\n",
    "    -> Int\n",
    "    -> G.Graph\n",
    "    -> STRef s a\n",
    "    -> STRef s [Int]\n",
    "    -> STRef s (S.HashSet Int)\n",
    "    -> STRef s (H.HashMap Int a)\n",
    "    -> STRef s (H.HashMap Int a)\n",
    "    -> STRef s [S.HashSet Int]\n",
    "    -> ST    s ()\n",
    "strongConnect n v graph index stack stackSet indices lowlinks output = do\n",
    "    i <- readSTRef index\n",
    "    insert v i indices\n",
    "    insert v i lowlinks\n",
    "    increment index\n",
    "    push stack stackSet v\n",
    "\n",
    "    forM_ (graph A.! v) $ \\w -> lookup w indices >>= \\case\n",
    "        Nothing     -> do\n",
    "            strongConnect n w graph index stack stackSet indices lowlinks output\n",
    "            vLowLink <- fromJust <$> lookup v lowlinks\n",
    "            wLowLink <- fromJust <$> lookup w lowlinks\n",
    "            insert v (min vLowLink wLowLink) lowlinks\n",
    "        Just wIndex -> do\n",
    "            wOnStack <- S.member w <$> readSTRef stackSet\n",
    "            when wOnStack $ do\n",
    "                vLowLink <- fromJust <$> lookup v lowlinks\n",
    "                insert v (min vLowLink wIndex) lowlinks\n",
    "\n",
    "    vLowLink <- fromJust <$> lookup v lowlinks\n",
    "    vIndex   <- fromJust <$> lookup v indices\n",
    "    when (vLowLink == vIndex) $ do\n",
    "        scc <- addSCC n v S.empty stack stackSet\n",
    "        modifySTRef' output (scc:)\n",
    "    where\n",
    "        lookup value hashMap     = H.lookup value <$> readSTRef hashMap\n",
    "        insert key value hashMap = modifySTRef' hashMap (H.insert key value)\n",
    "        increment counter        = modifySTRef' counter (+1)\n",
    "\n",
    "addSCC :: Int -> Int -> S.HashSet Int -> STRef s [Int] -> STRef s (S.HashSet Int) -> ST s (S.HashSet Int)\n",
    "addSCC n v scc stack stackSet = pop stack stackSet >>= \\w -> if ((other n w) `S.member` scc) then error \"not satisfiable\" else\n",
    "    let scc' = S.insert w scc\n",
    "    in if w == v then return scc' else addSCC n v scc' stack stackSet\n",
    "\n",
    "push :: STRef s [Int] -> STRef s (S.HashSet Int) -> Int -> ST s ()\n",
    "push stack stackSet e = do\n",
    "    modifySTRef' stack    (e:)\n",
    "    modifySTRef' stackSet (S.insert e)\n",
    "\n",
    "pop :: STRef s [Int] -> STRef s (S.HashSet Int) -> ST s Int\n",
    "pop stack stackSet = do\n",
    "    e <- head <$> readSTRef stack\n",
    "    modifySTRef' stack tail\n",
    "    modifySTRef' stackSet (S.delete e)\n",
    "    return e"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "import qualified Data.ByteString as B\n",
    "import qualified Data.ByteString.Char8 as BC\n",
    "import Data.Maybe"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "checkSat name = do\n",
    "    p <- map (map (fst . fromJust . BC.readInt) . BC.words) . BC.lines <$> B.readFile name\n",
    "    let pNo    = head $ head p\n",
    "        pn     = map (map (normalise pNo)) $ tail p\n",
    "        pGraph = G.buildG (0,2*pNo) $ concatMap (clauses pNo) pn\n",
    "    return $ length $ tarjan pNo pGraph"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "199991"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "checkSat \"2sat1.txt\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style><span class='err-msg'>not satisfiable<br/>CallStack (from HasCallStack):<br/>  error, called at &lt;interactive&gt;:61:99 in interactive:IHaskell2</span>"
      ],
      "text/plain": [
       "not satisfiable\n",
       "CallStack (from HasCallStack):\n",
       "  error, called at <interactive>:61:99 in interactive:Ghci2"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "checkSat \"2sat2.txt\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "799667"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "checkSat \"2sat3.txt\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "1199985"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "checkSat \"2sat4.txt\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style><span class='err-msg'>not satisfiable<br/>CallStack (from HasCallStack):<br/>  error, called at &lt;interactive&gt;:61:99 in interactive:IHaskell2</span>"
      ],
      "text/plain": [
       "not satisfiable\n",
       "CallStack (from HasCallStack):\n",
       "  error, called at <interactive>:61:99 in interactive:Ghci2"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "checkSat \"2sat5.txt\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style><span class='err-msg'>not satisfiable<br/>CallStack (from HasCallStack):<br/>  error, called at &lt;interactive&gt;:61:99 in interactive:IHaskell2</span>"
      ],
      "text/plain": [
       "not satisfiable\n",
       "CallStack (from HasCallStack):\n",
       "  error, called at <interactive>:61:99 in interactive:Ghci2"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "checkSat \"2sat6.txt\""
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Haskell",
   "language": "haskell",
   "name": "haskell"
  },
  "language_info": {
   "codemirror_mode": "ihaskell",
   "file_extension": ".hs",
   "name": "haskell",
   "version": "8.0.2"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}