diff --git a/README.md b/README.md index c97db60f1..a793deb30 100644 --- a/README.md +++ b/README.md @@ -98,9 +98,9 @@ Here is a table of algorithms, the figure, name of the algorithm in the book and | 7.10 | TT-Entails | `tt_entails` | [`logic.py`][logic] | Done | Included | | 7.12 | PL-Resolution | `pl_resolution` | [`logic.py`][logic] | Done | Included | | 7.14 | Convert to CNF | `to_cnf` | [`logic.py`][logic] | Done | Included | -| 7.15 | PL-FC-Entails? | `pl_fc_resolution` | [`logic.py`][logic] | Done | | -| 7.17 | DPLL-Satisfiable? | `dpll_satisfiable` | [`logic.py`][logic] | Done | | -| 7.18 | WalkSAT | `WalkSAT` | [`logic.py`][logic] | Done | | +| 7.15 | PL-FC-Entails? | `pl_fc_resolution` | [`logic.py`][logic] | Done | Included | +| 7.17 | DPLL-Satisfiable? | `dpll_satisfiable` | [`logic.py`][logic] | Done | Included | +| 7.18 | WalkSAT | `WalkSAT` | [`logic.py`][logic] | Done | Included | | 7.20 | Hybrid-Wumpus-Agent | `HybridWumpusAgent` | | | | | 7.22 | SATPlan | `SAT_plan` | [`logic.py`][logic] | Done | | | 9 | Subst | `subst` | [`logic.py`][logic] | Done | | diff --git a/logic.ipynb b/logic.ipynb index 726a8d69d..0cd6cbc1f 100644 --- a/logic.ipynb +++ b/logic.ipynb @@ -1489,6 +1489,853 @@ "pl_resolution(wumpus_kb, ~P22), pl_resolution(wumpus_kb, P22)" ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "### Effective Propositional Model Checking\n", + "\n", + "The previous segments elucidate the algorithmic procedure for model checking. \n", + "In this segment, we look at ways of making them computationally efficient.\n", + "
\n", + "The problem we are trying to solve is conventionally called the _propositional satisfiability problem_, abbreviated as the _SAT_ problem.\n", + "In layman terms, if there exists a model that satisfies a given Boolean formula, the formula is called satisfiable.\n", + "
\n", + "The SAT problem was the first problem to be proven _NP-complete_.\n", + "The main characteristics of an NP-complete problem are:\n", + "- Given a solution to such a problem, it is easy to verify if the solution solves the problem.\n", + "- The time required to actually solve the problem using any known algorithm increases exponentially with respect to the size of the problem.\n", + "
\n", + "
\n", + "Due to these properties, heuristic and approximational methods are often applied to find solutions to these problems.\n", + "
\n", + "It is extremely important to be able to solve large scale SAT problems efficiently because \n", + "many combinatorial problems in computer science can be conveniently reduced to checking the satisfiability of a propositional sentence under some constraints.\n", + "
\n", + "We will introduce two new algorithms that perform propositional model checking in a computationally effective way.\n", + "
\n" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "### 1. DPLL (Davis-Putnam-Logeman-Loveland) algorithm\n", + "This algorithm is very similar to Backtracking-Search.\n", + "It recursively enumerates possible models in a depth-first fashion with the following improvements over algorithms like `tt_entails`:\n", + "1. Early termination:\n", + "
\n", + "In certain cases, the algorithm can detect the truth value of a statement using just a partially completed model.\n", + "For example, $(P\\lor Q)\\land(P\\lor R)$ is true if P is true, regardless of other variables.\n", + "This reduces the search space significantly.\n", + "2. Pure symbol heuristic:\n", + "
\n", + "A symbol that has the same sign (positive or negative) in all clauses is called a _pure symbol_.\n", + "It isn't difficult to see that any satisfiable model will have the pure symbols assigned such that its parent clause becomes _true_.\n", + "For example, $(P\\lor\\neg Q)\\land(\\neg Q\\lor\\neg R)\\land(R\\lor P)$ has P and Q as pure symbols\n", + "and for the sentence to be true, P _has_ to be true and Q _has_ to be false.\n", + "The pure symbol heuristic thus simplifies the problem a bit.\n", + "3. Unit clause heuristic:\n", + "
\n", + "In the context of DPLL, clauses with just one literal and clauses with all but one _false_ literals are called unit clauses.\n", + "If a clause is a unit clause, it can only be satisfied by assigning the necessary value to make the last literal true.\n", + "We have no other choice.\n", + "
\n", + "Assigning one unit clause can create another unit clause.\n", + "For example, when P is false, $(P\\lor Q)$ becomes a unit clause, causing _true_ to be assigned to Q.\n", + "A series of forced assignments derived from previous unit clauses is called _unit propagation_.\n", + "In this way, this heuristic simplifies the problem further.\n", + "
\n", + "The algorithm often employs other tricks to scale up to large problems.\n", + "However, these tricks are currently out of the scope of this notebook. Refer to section 7.6 of the book for more details.\n", + "
\n", + "
\n", + "Let's have a look at the algorithm." + ] + }, + { + "cell_type": "code", + "execution_count": 48, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + "\n", + "\n", + "\n", + " \n", + " \n", + " \n", + "\n", + "\n", + "

\n", + "\n", + "

def dpll(clauses, symbols, model):\n",
+       "    """See if the clauses are true in a partial model."""\n",
+       "    unknown_clauses = []  # clauses with an unknown truth value\n",
+       "    for c in clauses:\n",
+       "        val = pl_true(c, model)\n",
+       "        if val is False:\n",
+       "            return False\n",
+       "        if val is not True:\n",
+       "            unknown_clauses.append(c)\n",
+       "    if not unknown_clauses:\n",
+       "        return model\n",
+       "    P, value = find_pure_symbol(symbols, unknown_clauses)\n",
+       "    if P:\n",
+       "        return dpll(clauses, removeall(P, symbols), extend(model, P, value))\n",
+       "    P, value = find_unit_clause(clauses, model)\n",
+       "    if P:\n",
+       "        return dpll(clauses, removeall(P, symbols), extend(model, P, value))\n",
+       "    if not symbols:\n",
+       "        raise TypeError("Argument should be of the type Expr.")\n",
+       "    P, symbols = symbols[0], symbols[1:]\n",
+       "    return (dpll(clauses, symbols, extend(model, P, True)) or\n",
+       "            dpll(clauses, symbols, extend(model, P, False)))\n",
+       "

\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "psource(dpll)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The algorithm uses the ideas described above to check satisfiability of a sentence in propositional logic.\n", + "It recursively calls itself, simplifying the problem at each step. It also uses helper functions `find_pure_symbol` and `find_unit_clause` to carry out steps 2 and 3 above.\n", + "
\n", + "The `dpll_satisfiable` helper function converts the input clauses to _conjunctive normal form_ and calls the `dpll` function with the correct parameters." + ] + }, + { + "cell_type": "code", + "execution_count": 49, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + "\n", + "\n", + "\n", + " \n", + " \n", + " \n", + "\n", + "\n", + "

\n", + "\n", + "

def dpll_satisfiable(s):\n",
+       "    """Check satisfiability of a propositional sentence.\n",
+       "    This differs from the book code in two ways: (1) it returns a model\n",
+       "    rather than True when it succeeds; this is more useful. (2) The\n",
+       "    function find_pure_symbol is passed a list of unknown clauses, rather\n",
+       "    than a list of all clauses and the model; this is more efficient."""\n",
+       "    clauses = conjuncts(to_cnf(s))\n",
+       "    symbols = list(prop_symbols(s))\n",
+       "    return dpll(clauses, symbols, {})\n",
+       "

\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "psource(dpll_satisfiable)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Let's see a few examples of usage." + ] + }, + { + "cell_type": "code", + "execution_count": 50, + "metadata": {}, + "outputs": [], + "source": [ + "A, B, C, D = expr('A, B, C, D')" + ] + }, + { + "cell_type": "code", + "execution_count": 51, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "{C: False, A: True, D: True, B: True}" + ] + }, + "execution_count": 51, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "dpll_satisfiable(A & B & ~C & D)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "This is a simple case to highlight that the algorithm actually works." + ] + }, + { + "cell_type": "code", + "execution_count": 52, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "{C: True, D: False, B: True}" + ] + }, + "execution_count": 52, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "dpll_satisfiable((A & B) | (C & ~A) | (B & ~D))" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "If a particular symbol isn't present in the solution, \n", + "it means that the solution is independent of the value of that symbol.\n", + "In this case, the solution is independent of A." + ] + }, + { + "cell_type": "code", + "execution_count": 53, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "{A: True, B: True}" + ] + }, + "execution_count": 53, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "dpll_satisfiable(A |'<=>'| B)" + ] + }, + { + "cell_type": "code", + "execution_count": 54, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "{C: True, A: True, B: False}" + ] + }, + "execution_count": 54, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "dpll_satisfiable((A |'<=>'| B) |'==>'| (C & ~A))" + ] + }, + { + "cell_type": "code", + "execution_count": 55, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "{C: True, A: True}" + ] + }, + "execution_count": 55, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "dpll_satisfiable((A | (B & C)) |'<=>'| ((A | B) & (A | C)))" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "### 2. WalkSAT algorithm\n", + "This algorithm is very similar to Hill climbing.\n", + "On every iteration, the algorithm picks an unsatisfied clause and flips a symbol in the clause.\n", + "This is similar to finding a neighboring state in the `hill_climbing` algorithm.\n", + "
\n", + "The symbol to be flipped is decided by an evaluation function that counts the number of unsatisfied clauses.\n", + "Sometimes, symbols are also flipped randomly, to avoid local optima. A subtle balance between greediness and randomness is required. Alternatively, some versions of the algorithm restart with a completely new random assignment if no solution has been found for too long, as a way of getting out of local minima of numbers of unsatisfied clauses.\n", + "
\n", + "
\n", + "Let's have a look at the algorithm." + ] + }, + { + "cell_type": "code", + "execution_count": 56, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + "\n", + "\n", + "\n", + " \n", + " \n", + " \n", + "\n", + "\n", + "

\n", + "\n", + "

def WalkSAT(clauses, p=0.5, max_flips=10000):\n",
+       "    """Checks for satisfiability of all clauses by randomly flipping values of variables\n",
+       "    """\n",
+       "    # Set of all symbols in all clauses\n",
+       "    symbols = {sym for clause in clauses for sym in prop_symbols(clause)}\n",
+       "    # model is a random assignment of true/false to the symbols in clauses\n",
+       "    model = {s: random.choice([True, False]) for s in symbols}\n",
+       "    for i in range(max_flips):\n",
+       "        satisfied, unsatisfied = [], []\n",
+       "        for clause in clauses:\n",
+       "            (satisfied if pl_true(clause, model) else unsatisfied).append(clause)\n",
+       "        if not unsatisfied:  # if model satisfies all the clauses\n",
+       "            return model\n",
+       "        clause = random.choice(unsatisfied)\n",
+       "        if probability(p):\n",
+       "            sym = random.choice(list(prop_symbols(clause)))\n",
+       "        else:\n",
+       "            # Flip the symbol in clause that maximizes number of sat. clauses\n",
+       "            def sat_count(sym):\n",
+       "                # Return the the number of clauses satisfied after flipping the symbol.\n",
+       "                model[sym] = not model[sym]\n",
+       "                count = len([clause for clause in clauses if pl_true(clause, model)])\n",
+       "                model[sym] = not model[sym]\n",
+       "                return count\n",
+       "            sym = argmax(prop_symbols(clause), key=sat_count)\n",
+       "        model[sym] = not model[sym]\n",
+       "    # If no solution is found within the flip limit, we return failure\n",
+       "    return None\n",
+       "

\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "psource(WalkSAT)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The function takes three arguments:\n", + "
\n", + "1. The `clauses` we want to satisfy.\n", + "
\n", + "2. The probability `p` of randomly changing a symbol.\n", + "
\n", + "3. The maximum number of flips (`max_flips`) the algorithm will run for. If the clauses are still unsatisfied, the algorithm returns `None` to denote failure.\n", + "
\n", + "The algorithm is identical in concept to Hill climbing and the code isn't difficult to understand.\n", + "
\n", + "
\n", + "Let's see a few examples of usage." + ] + }, + { + "cell_type": "code", + "execution_count": 57, + "metadata": { + "collapsed": true + }, + "outputs": [], + "source": [ + "A, B, C, D = expr('A, B, C, D')" + ] + }, + { + "cell_type": "code", + "execution_count": 58, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "{C: False, A: True, D: True, B: True}" + ] + }, + "execution_count": 58, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "WalkSAT([A, B, ~C, D], 0.5, 100)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "This is a simple case to show that the algorithm converges." + ] + }, + { + "cell_type": "code", + "execution_count": 59, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "{C: True, A: True, B: True}" + ] + }, + "execution_count": 59, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "WalkSAT([A & B, A & C], 0.5, 100)" + ] + }, + { + "cell_type": "code", + "execution_count": 60, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "{C: True, A: True, D: True, B: True}" + ] + }, + "execution_count": 60, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "WalkSAT([A & B, C & D, C & B], 0.5, 100)" + ] + }, + { + "cell_type": "code", + "execution_count": 61, + "metadata": {}, + "outputs": [], + "source": [ + "WalkSAT([A & B, C | D, ~(D | B)], 0.5, 1000)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "This one doesn't give any output because WalkSAT did not find any model where these clauses hold. We can solve these clauses to see that they together form a contradiction and hence, it isn't supposed to have a solution." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "One point of difference between this algorithm and the `dpll_satisfiable` algorithms is that both these algorithms take inputs differently. \n", + "For WalkSAT to take complete sentences as input, \n", + "we can write a helper function that converts the input sentence into conjunctive normal form and then calls WalkSAT with the list of conjuncts of the CNF form of the sentence." + ] + }, + { + "cell_type": "code", + "execution_count": 62, + "metadata": { + "collapsed": true + }, + "outputs": [], + "source": [ + "def WalkSAT_CNF(sentence, p=0.5, max_flips=10000):\n", + " return WalkSAT(conjuncts(to_cnf(sentence)), 0, max_flips)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Now we can call `WalkSAT_CNF` and `DPLL_Satisfiable` with the same arguments." + ] + }, + { + "cell_type": "code", + "execution_count": 63, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "{A: False, D: False, C: True, B: False}" + ] + }, + "execution_count": 63, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "WalkSAT_CNF((A & B) | (C & ~A) | (B & ~D), 0.5, 1000)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "It works!\n", + "
\n", + "Notice that the solution generated by WalkSAT doesn't omit variables that the sentence doesn't depend upon. \n", + "If the sentence is independent of a particular variable, the solution contains a random value for that variable because of the stochastic nature of the algorithm.\n", + "
\n", + "
\n", + "Let's compare the runtime of WalkSAT and DPLL for a few cases. We will use the `%%timeit` magic to do this." + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": true + }, + "outputs": [], + "source": [ + "sentence_1 = A |'<=>'| B\n", + "sentence_2 = (A & B) | (C & ~A) | (B & ~D)\n", + "sentence_3 = (A | (B & C)) |'<=>'| ((A | B) & (A | C))" + ] + }, + { + "cell_type": "code", + "execution_count": 65, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "100 loops, best of 3: 2.46 ms per loop\n" + ] + } + ], + "source": [ + "%%timeit\n", + "dpll_satisfiable(sentence_1)\n", + "dpll_satisfiable(sentence_2)\n", + "dpll_satisfiable(sentence_3)" + ] + }, + { + "cell_type": "code", + "execution_count": 66, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "100 loops, best of 3: 1.91 ms per loop\n" + ] + } + ], + "source": [ + "%%timeit\n", + "WalkSAT_CNF(sentence_1)\n", + "WalkSAT_CNF(sentence_2)\n", + "WalkSAT_CNF(sentence_3)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "On an average, for solvable cases, `WalkSAT` is quite faster than `dpll` because, for a small number of variables, \n", + "`WalkSAT` can reduce the search space significantly. \n", + "Results can be different for sentences with more symbols though.\n", + "Feel free to play around with this to understand the trade-offs of these algorithms better." + ] + }, { "cell_type": "markdown", "metadata": {},