{
"cells": [
{
"cell_type": "markdown",
"metadata": {
"collapsed": true
},
"source": [
"# Logic"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"This Jupyter notebook acts as supporting material for topics covered in __Chapter 6 Logical Agents__, __Chapter 7 First-Order Logic__ and __Chapter 8 Inference in First-Order Logic__ of the book *[Artificial Intelligence: A Modern Approach](http://aima.cs.berkeley.edu)*. We make use of the implementations in the [logic.py](https://github.com/aimacode/aima-python/blob/master/logic.py) module. See the [intro notebook](https://github.com/aimacode/aima-python/blob/master/intro.ipynb) for instructions.\n",
"\n",
"Let's first import everything from the `logic` module."
]
},
{
"cell_type": "code",
"execution_count": 1,
"metadata": {
"collapsed": true
},
"outputs": [],
"source": [
"from utils import *\n",
"from logic import *\n",
"from notebook import psource"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## CONTENTS\n",
"- Logical sentences\n",
" - Expr\n",
" - PropKB\n",
" - Knowledge-based agents\n",
" - Inference in propositional knowledge base\n",
" - Truth table enumeration\n",
" - Proof by resolution\n",
" - Forward and backward chaining\n",
" - DPLL\n",
" - WalkSAT\n",
" - SATPlan\n",
" - FolKB\n",
" - Inference in first order knowledge base\n",
" - Unification\n",
" - Forward chaining algorithm\n",
" - Backward chaining algorithm"
]
},
{
"cell_type": "markdown",
"metadata": {
"collapsed": true
},
"source": [
"## Logical Sentences"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The `Expr` class is designed to represent any kind of mathematical expression. The simplest type of `Expr` is a symbol, which can be defined with the function `Symbol`:"
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"x"
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"Symbol('x')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Or we can define multiple symbols at the same time with the function `symbols`:"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {
"collapsed": true
},
"outputs": [],
"source": [
"(x, y, P, Q, f) = symbols('x, y, P, Q, f')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We can combine `Expr`s with the regular Python infix and prefix operators. Here's how we would form the logical sentence \"P and not Q\":"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(P & ~Q)"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"P & ~Q"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"This works because the `Expr` class overloads the `&` operator with this definition:\n",
"\n",
"```python\n",
"def __and__(self, other): return Expr('&', self, other)```\n",
" \n",
"and does similar overloads for the other operators. An `Expr` has two fields: `op` for the operator, which is always a string, and `args` for the arguments, which is a tuple of 0 or more expressions. By \"expression,\" I mean either an instance of `Expr`, or a number. Let's take a look at the fields for some `Expr` examples:"
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"'&'"
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"sentence = P & ~Q\n",
"\n",
"sentence.op"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(P, ~Q)"
]
},
"execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"sentence.args"
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"'P'"
]
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"P.op"
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"()"
]
},
"execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"P.args"
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"'P'"
]
},
"execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"Pxy = P(x, y)\n",
"\n",
"Pxy.op"
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(x, y)"
]
},
"execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"Pxy.args"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"It is important to note that the `Expr` class does not define the *logic* of Propositional Logic sentences; it just gives you a way to *represent* expressions. Think of an `Expr` as an [abstract syntax tree](https://en.wikipedia.org/wiki/Abstract_syntax_tree). Each of the `args` in an `Expr` can be either a symbol, a number, or a nested `Expr`. We can nest these trees to any depth. Here is a deply nested `Expr`:"
]
},
{
"cell_type": "code",
"execution_count": 11,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(((3 * f(x, y)) + (P(y) / 2)) + 1)"
]
},
"execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"3 * f(x, y) + P(y) / 2 + 1"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Operators for Constructing Logical Sentences\n",
"\n",
"Here is a table of the operators that can be used to form sentences. Note that we have a problem: we want to use Python operators to make sentences, so that our programs (and our interactive sessions like the one here) will show simple code. But Python does not allow implication arrows as operators, so for now we have to use a more verbose notation that Python does allow: `|'==>'|` instead of just `==>`. Alternately, you can always use the more verbose `Expr` constructor forms:\n",
"\n",
"| Operation | Book | Python Infix Input | Python Output | Python `Expr` Input\n",
"|--------------------------|----------------------|-------------------------|---|---|\n",
"| Negation | ¬ P | `~P` | `~P` | `Expr('~', P)`\n",
"| And | P ∧ Q | `P & Q` | `P & Q` | `Expr('&', P, Q)`\n",
"| Or | P ∨ Q | `P` | `Q`| `P` | `Q` | `Expr('`|`', P, Q)`\n",
"| Inequality (Xor) | P ≠ Q | `P ^ Q` | `P ^ Q` | `Expr('^', P, Q)`\n",
"| Implication | P → Q | `P` |`'==>'`| `Q` | `P ==> Q` | `Expr('==>', P, Q)`\n",
"| Reverse Implication | Q ← P | `Q` |`'<=='`| `P` |`Q <== P` | `Expr('<==', Q, P)`\n",
"| Equivalence | P ↔ Q | `P` |`'<=>'`| `Q` |`P <=> Q` | `Expr('<=>', P, Q)`\n",
"\n",
"Here's an example of defining a sentence with an implication arrow:"
]
},
{
"cell_type": "code",
"execution_count": 12,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(~(P & Q) ==> (~P | ~Q))"
]
},
"execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"~(P & Q) |'==>'| (~P | ~Q)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## `expr`: a Shortcut for Constructing Sentences\n",
"\n",
"If the `|'==>'|` notation looks ugly to you, you can use the function `expr` instead:"
]
},
{
"cell_type": "code",
"execution_count": 13,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(~(P & Q) ==> (~P | ~Q))"
]
},
"execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"expr('~(P & Q) ==> (~P | ~Q)')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"`expr` takes a string as input, and parses it into an `Expr`. The string can contain arrow operators: `==>`, `<==`, or `<=>`, which are handled as if they were regular Python infix operators. And `expr` automatically defines any symbols, so you don't need to pre-define them:"
]
},
{
"cell_type": "code",
"execution_count": 14,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"sqrt(((b ** 2) - ((4 * a) * c)))"
]
},
"execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"expr('sqrt(b ** 2 - 4 * a * c)')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"For now that's all you need to know about `expr`. If you are interested, we explain the messy details of how `expr` is implemented and how `|'==>'|` is handled in the appendix."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Propositional Knowledge Bases: `PropKB`\n",
"\n",
"The class `PropKB` can be used to represent a knowledge base of propositional logic sentences.\n",
"\n",
"We see that the class `KB` has four methods, apart from `__init__`. A point to note here: the `ask` method simply calls the `ask_generator` method. Thus, this one has already been implemented, and what you'll have to actually implement when you create your own knowledge base class (though you'll probably never need to, considering the ones we've created for you) will be the `ask_generator` function and not the `ask` function itself.\n",
"\n",
"The class `PropKB` now.\n",
"* `__init__(self, sentence=None)` : The constructor `__init__` creates a single field `clauses` which will be a list of all the sentences of the knowledge base. Note that each one of these sentences will be a 'clause' i.e. a sentence which is made up of only literals and `or`s.\n",
"* `tell(self, sentence)` : When you want to add a sentence to the KB, you use the `tell` method. This method takes a sentence, converts it to its CNF, extracts all the clauses, and adds all these clauses to the `clauses` field. So, you need not worry about `tell`ing only clauses to the knowledge base. You can `tell` the knowledge base a sentence in any form that you wish; converting it to CNF and adding the resulting clauses will be handled by the `tell` method.\n",
"* `ask_generator(self, query)` : The `ask_generator` function is used by the `ask` function. It calls the `tt_entails` function, which in turn returns `True` if the knowledge base entails query and `False` otherwise. The `ask_generator` itself returns an empty dict `{}` if the knowledge base entails query and `None` otherwise. This might seem a little bit weird to you. After all, it makes more sense just to return a `True` or a `False` instead of the `{}` or `None` But this is done to maintain consistency with the way things are in First-Order Logic, where an `ask_generator` function is supposed to return all the substitutions that make the query true. Hence the dict, to return all these substitutions. I will be mostly be using the `ask` function which returns a `{}` or a `False`, but if you don't like this, you can always use the `ask_if_true` function which returns a `True` or a `False`.\n",
"* `retract(self, sentence)` : This function removes all the clauses of the sentence given, from the knowledge base. Like the `tell` function, you don't have to pass clauses to remove them from the knowledge base; any sentence will do fine. The function will take care of converting that sentence to clauses and then remove those."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Wumpus World KB\n",
"Let us create a `PropKB` for the wumpus world with the sentences mentioned in `section 7.4.3`."
]
},
{
"cell_type": "code",
"execution_count": 15,
"metadata": {
"collapsed": true
},
"outputs": [],
"source": [
"wumpus_kb = PropKB()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We define the symbols we use in our clauses.
\n",
"$P_{x, y}$ is true if there is a pit in `[x, y]`.
\n",
"$B_{x, y}$ is true if the agent senses breeze in `[x, y]`.
"
]
},
{
"cell_type": "code",
"execution_count": 16,
"metadata": {
"collapsed": true
},
"outputs": [],
"source": [
"P11, P12, P21, P22, P31, B11, B21 = expr('P11, P12, P21, P22, P31, B11, B21')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now we tell sentences based on `section 7.4.3`.
\n",
"There is no pit in `[1,1]`."
]
},
{
"cell_type": "code",
"execution_count": 17,
"metadata": {
"collapsed": true
},
"outputs": [],
"source": [
"wumpus_kb.tell(~P11)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"A square is breezy if and only if there is a pit in a neighboring square. This has to be stated for each square but for now, we include just the relevant squares."
]
},
{
"cell_type": "code",
"execution_count": 18,
"metadata": {
"collapsed": true
},
"outputs": [],
"source": [
"wumpus_kb.tell(B11 | '<=>' | ((P12 | P21)))\n",
"wumpus_kb.tell(B21 | '<=>' | ((P11 | P22 | P31)))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now we include the breeze percepts for the first two squares leading up to the situation in `Figure 7.3(b)`"
]
},
{
"cell_type": "code",
"execution_count": 19,
"metadata": {
"collapsed": true
},
"outputs": [],
"source": [
"wumpus_kb.tell(~B11)\n",
"wumpus_kb.tell(B21)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We can check the clauses stored in a `KB` by accessing its `clauses` variable"
]
},
{
"cell_type": "code",
"execution_count": 20,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"[~P11,\n",
" (~P12 | B11),\n",
" (~P21 | B11),\n",
" (P12 | P21 | ~B11),\n",
" (~P11 | B21),\n",
" (~P22 | B21),\n",
" (~P31 | B21),\n",
" (P11 | P22 | P31 | ~B21),\n",
" ~B11,\n",
" B21]"
]
},
"execution_count": 20,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"wumpus_kb.clauses"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We see that the equivalence $B_{1, 1} \\iff (P_{1, 2} \\lor P_{2, 1})$ was automatically converted to two implications which were inturn converted to CNF which is stored in the `KB`.
\n",
"$B_{1, 1} \\iff (P_{1, 2} \\lor P_{2, 1})$ was split into $B_{1, 1} \\implies (P_{1, 2} \\lor P_{2, 1})$ and $B_{1, 1} \\Longleftarrow (P_{1, 2} \\lor P_{2, 1})$.
\n",
"$B_{1, 1} \\implies (P_{1, 2} \\lor P_{2, 1})$ was converted to $P_{1, 2} \\lor P_{2, 1} \\lor \\neg B_{1, 1}$.
\n",
"$B_{1, 1} \\Longleftarrow (P_{1, 2} \\lor P_{2, 1})$ was converted to $\\neg (P_{1, 2} \\lor P_{2, 1}) \\lor B_{1, 1}$ which becomes $(\\neg P_{1, 2} \\lor B_{1, 1}) \\land (\\neg P_{2, 1} \\lor B_{1, 1})$ after applying De Morgan's laws and distributing the disjunction.
\n",
"$B_{2, 1} \\iff (P_{1, 1} \\lor P_{2, 2} \\lor P_{3, 2})$ is converted in similar manner."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Knowledge based agents"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"A knowledge-based agent is a simple generic agent that maintains and handles a knowledge base.\n",
"The knowledge base may initially contain some background knowledge.\n",
"
\n",
"The purpose of a KB agent is to provide a level of abstraction over knowledge-base manipulation and is to be used as a base class for agents that work on a knowledge base.\n",
"
\n",
"Given a percept, the KB agent adds the percept to its knowledge base, asks the knowledge base for the best action, and tells the knowledge base that it has in fact taken that action.\n",
"
\n",
"Our implementation of `KB-Agent` is encapsulated in a class `KB_AgentProgram` which inherits from the `KB` class.\n",
"
\n",
"Let's have a look."
]
},
{
"cell_type": "code",
"execution_count": 21,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"\n",
"\n",
"\n",
"
def KB_AgentProgram(KB):\n",
" """A generic logical knowledge-based agent program. [Figure 7.1]"""\n",
" steps = itertools.count()\n",
"\n",
" def program(percept):\n",
" t = next(steps)\n",
" KB.tell(make_percept_sentence(percept, t))\n",
" action = KB.ask(make_action_query(t))\n",
" KB.tell(make_action_sentence(action, t))\n",
" return action\n",
"\n",
" def make_percept_sentence(percept, t):\n",
" return Expr("Percept")(percept, t)\n",
"\n",
" def make_action_query(t):\n",
" return expr("ShouldDo(action, {})".format(t))\n",
"\n",
" def make_action_sentence(action, t):\n",
" return Expr("Did")(action[expr('action')], t)\n",
"\n",
" return program\n",
"
def tt_check_all(kb, alpha, symbols, model):\n",
" """Auxiliary routine to implement tt_entails."""\n",
" if not symbols:\n",
" if pl_true(kb, model):\n",
" result = pl_true(alpha, model)\n",
" assert result in (True, False)\n",
" return result\n",
" else:\n",
" return True\n",
" else:\n",
" P, rest = symbols[0], symbols[1:]\n",
" return (tt_check_all(kb, alpha, rest, extend(model, P, True)) and\n",
" tt_check_all(kb, alpha, rest, extend(model, P, False)))\n",
"
def tt_entails(kb, alpha):\n",
" """Does kb entail the sentence alpha? Use truth tables. For propositional\n",
" kb's and sentences. [Figure 7.10]. Note that the 'kb' should be an\n",
" Expr which is a conjunction of clauses.\n",
" >>> tt_entails(expr('P & Q'), expr('Q'))\n",
" True\n",
" """\n",
" assert not variables(alpha)\n",
" symbols = list(prop_symbols(kb & alpha))\n",
" return tt_check_all(kb, alpha, symbols, {})\n",
"
def to_cnf(s):\n",
" """Convert a propositional logical sentence to conjunctive normal form.\n",
" That is, to the form ((A | ~B | ...) & (B | C | ...) & ...) [p. 253]\n",
" >>> to_cnf('~(B | C)')\n",
" (~B & ~C)\n",
" """\n",
" s = expr(s)\n",
" if isinstance(s, str):\n",
" s = expr(s)\n",
" s = eliminate_implications(s) # Steps 1, 2 from p. 253\n",
" s = move_not_inwards(s) # Step 3\n",
" return distribute_and_over_or(s) # Step 4\n",
"
def eliminate_implications(s):\n",
" """Change implications into equivalent form with only &, |, and ~ as logical operators."""\n",
" s = expr(s)\n",
" if not s.args or is_symbol(s.op):\n",
" return s # Atoms are unchanged.\n",
" args = list(map(eliminate_implications, s.args))\n",
" a, b = args[0], args[-1]\n",
" if s.op == '==>':\n",
" return b | ~a\n",
" elif s.op == '<==':\n",
" return a | ~b\n",
" elif s.op == '<=>':\n",
" return (a | ~b) & (b | ~a)\n",
" elif s.op == '^':\n",
" assert len(args) == 2 # TODO: relax this restriction\n",
" return (a & ~b) | (~a & b)\n",
" else:\n",
" assert s.op in ('&', '|', '~')\n",
" return Expr(s.op, *args)\n",
"
def move_not_inwards(s):\n",
" """Rewrite sentence s by moving negation sign inward.\n",
" >>> move_not_inwards(~(A | B))\n",
" (~A & ~B)"""\n",
" s = expr(s)\n",
" if s.op == '~':\n",
" def NOT(b):\n",
" return move_not_inwards(~b)\n",
" a = s.args[0]\n",
" if a.op == '~':\n",
" return move_not_inwards(a.args[0]) # ~~A ==> A\n",
" if a.op == '&':\n",
" return associate('|', list(map(NOT, a.args)))\n",
" if a.op == '|':\n",
" return associate('&', list(map(NOT, a.args)))\n",
" return s\n",
" elif is_symbol(s.op) or not s.args:\n",
" return s\n",
" else:\n",
" return Expr(s.op, *list(map(move_not_inwards, s.args)))\n",
"
def distribute_and_over_or(s):\n",
" """Given a sentence s consisting of conjunctions and disjunctions\n",
" of literals, return an equivalent sentence in CNF.\n",
" >>> distribute_and_over_or((A & B) | C)\n",
" ((A | C) & (B | C))\n",
" """\n",
" s = expr(s)\n",
" if s.op == '|':\n",
" s = associate('|', s.args)\n",
" if s.op != '|':\n",
" return distribute_and_over_or(s)\n",
" if len(s.args) == 0:\n",
" return False\n",
" if len(s.args) == 1:\n",
" return distribute_and_over_or(s.args[0])\n",
" conj = first(arg for arg in s.args if arg.op == '&')\n",
" if not conj:\n",
" return s\n",
" others = [a for a in s.args if a is not conj]\n",
" rest = associate('|', others)\n",
" return associate('&', [distribute_and_over_or(c | rest)\n",
" for c in conj.args])\n",
" elif s.op == '&':\n",
" return associate('&', list(map(distribute_and_over_or, s.args)))\n",
" else:\n",
" return s\n",
"
def pl_resolution(KB, alpha):\n",
" """Propositional-logic resolution: say if alpha follows from KB. [Figure 7.12]"""\n",
" clauses = KB.clauses + conjuncts(to_cnf(~alpha))\n",
" new = set()\n",
" while True:\n",
" n = len(clauses)\n",
" pairs = [(clauses[i], clauses[j])\n",
" for i in range(n) for j in range(i+1, n)]\n",
" for (ci, cj) in pairs:\n",
" resolvents = pl_resolve(ci, cj)\n",
" if False in resolvents:\n",
" return True\n",
" new = new.union(set(resolvents))\n",
" if new.issubset(set(clauses)):\n",
" return False\n",
" for c in new:\n",
" if c not in clauses:\n",
" clauses.append(c)\n",
"
def clauses_with_premise(self, p):\n",
" """Return a list of the clauses in KB that have p in their premise.\n",
" This could be cached away for O(1) speed, but we'll recompute it."""\n",
" return [c for c in self.clauses\n",
" if c.op == '==>' and p in conjuncts(c.args[0])]\n",
"
def pl_fc_entails(KB, q):\n",
" """Use forward chaining to see if a PropDefiniteKB entails symbol q.\n",
" [Figure 7.15]\n",
" >>> pl_fc_entails(horn_clauses_KB, expr('Q'))\n",
" True\n",
" """\n",
" count = {c: len(conjuncts(c.args[0]))\n",
" for c in KB.clauses\n",
" if c.op == '==>'}\n",
" inferred = defaultdict(bool)\n",
" agenda = [s for s in KB.clauses if is_prop_symbol(s.op)]\n",
" while agenda:\n",
" p = agenda.pop()\n",
" if p == q:\n",
" return True\n",
" if not inferred[p]:\n",
" inferred[p] = True\n",
" for c in KB.clauses_with_premise(p):\n",
" count[c] -= 1\n",
" if count[c] == 0:\n",
" agenda.append(c.args[1])\n",
" return False\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",
"
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",
"
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",
"
def SAT_plan(init, transition, goal, t_max, SAT_solver=dpll_satisfiable):\n",
" """Converts a planning problem to Satisfaction problem by translating it to a cnf sentence.\n",
" [Figure 7.22]"""\n",
"\n",
" # Functions used by SAT_plan\n",
" def translate_to_SAT(init, transition, goal, time):\n",
" clauses = []\n",
" states = [state for state in transition]\n",
"\n",
" # Symbol claiming state s at time t\n",
" state_counter = itertools.count()\n",
" for s in states:\n",
" for t in range(time+1):\n",
" state_sym[s, t] = Expr("State_{}".format(next(state_counter)))\n",
"\n",
" # Add initial state axiom\n",
" clauses.append(state_sym[init, 0])\n",
"\n",
" # Add goal state axiom\n",
" clauses.append(state_sym[goal, time])\n",
"\n",
" # All possible transitions\n",
" transition_counter = itertools.count()\n",
" for s in states:\n",
" for action in transition[s]:\n",
" s_ = transition[s][action]\n",
" for t in range(time):\n",
" # Action 'action' taken from state 's' at time 't' to reach 's_'\n",
" action_sym[s, action, t] = Expr(\n",
" "Transition_{}".format(next(transition_counter)))\n",
"\n",
" # Change the state from s to s_\n",
" clauses.append(action_sym[s, action, t] |'==>'| state_sym[s, t])\n",
" clauses.append(action_sym[s, action, t] |'==>'| state_sym[s_, t + 1])\n",
"\n",
" # Allow only one state at any time\n",
" for t in range(time+1):\n",
" # must be a state at any time\n",
" clauses.append(associate('|', [state_sym[s, t] for s in states]))\n",
"\n",
" for s in states:\n",
" for s_ in states[states.index(s) + 1:]:\n",
" # for each pair of states s, s_ only one is possible at time t\n",
" clauses.append((~state_sym[s, t]) | (~state_sym[s_, t]))\n",
"\n",
" # Restrict to one transition per timestep\n",
" for t in range(time):\n",
" # list of possible transitions at time t\n",
" transitions_t = [tr for tr in action_sym if tr[2] == t]\n",
"\n",
" # make sure at least one of the transitions happens\n",
" clauses.append(associate('|', [action_sym[tr] for tr in transitions_t]))\n",
"\n",
" for tr in transitions_t:\n",
" for tr_ in transitions_t[transitions_t.index(tr) + 1:]:\n",
" # there cannot be two transitions tr and tr_ at time t\n",
" clauses.append(~action_sym[tr] | ~action_sym[tr_])\n",
"\n",
" # Combine the clauses to form the cnf\n",
" return associate('&', clauses)\n",
"\n",
" def extract_solution(model):\n",
" true_transitions = [t for t in action_sym if model[action_sym[t]]]\n",
" # Sort transitions based on time, which is the 3rd element of the tuple\n",
" true_transitions.sort(key=lambda x: x[2])\n",
" return [action for s, action, time in true_transitions]\n",
"\n",
" # Body of SAT_plan algorithm\n",
" for t in range(t_max):\n",
" # dictionaries to help extract the solution from model\n",
" state_sym = {}\n",
" action_sym = {}\n",
"\n",
" cnf = translate_to_SAT(init, transition, goal, t)\n",
" model = SAT_solver(cnf)\n",
" if model is not False:\n",
" return extract_solution(model)\n",
" return None\n",
"
def subst(s, x):\n",
" """Substitute the substitution s into the expression x.\n",
" >>> subst({x: 42, y:0}, F(x) + y)\n",
" (F(42) + 0)\n",
" """\n",
" if isinstance(x, list):\n",
" return [subst(s, xi) for xi in x]\n",
" elif isinstance(x, tuple):\n",
" return tuple([subst(s, xi) for xi in x])\n",
" elif not isinstance(x, Expr):\n",
" return x\n",
" elif is_var_symbol(x.op):\n",
" return s.get(x, x)\n",
" else:\n",
" return Expr(x.op, *[subst(s, arg) for arg in x.args])\n",
"
def fol_fc_ask(KB, alpha):\n",
" """A simple forward-chaining algorithm. [Figure 9.3]"""\n",
" # TODO: Improve efficiency\n",
" kb_consts = list({c for clause in KB.clauses for c in constant_symbols(clause)})\n",
" def enum_subst(p):\n",
" query_vars = list({v for clause in p for v in variables(clause)})\n",
" for assignment_list in itertools.product(kb_consts, repeat=len(query_vars)):\n",
" theta = {x: y for x, y in zip(query_vars, assignment_list)}\n",
" yield theta\n",
"\n",
" # check if we can answer without new inferences\n",
" for q in KB.clauses:\n",
" phi = unify(q, alpha, {})\n",
" if phi is not None:\n",
" yield phi\n",
"\n",
" while True:\n",
" new = []\n",
" for rule in KB.clauses:\n",
" p, q = parse_definite_clause(rule)\n",
" for theta in enum_subst(p):\n",
" if set(subst(theta, p)).issubset(set(KB.clauses)):\n",
" q_ = subst(theta, q)\n",
" if all([unify(x, q_, {}) is None for x in KB.clauses + new]):\n",
" new.append(q_)\n",
" phi = unify(q_, alpha, {})\n",
" if phi is not None:\n",
" yield phi\n",
" if not new:\n",
" break\n",
" for clause in new:\n",
" KB.tell(clause)\n",
" return None\n",
"
def fol_bc_or(KB, goal, theta):\n",
" for rule in KB.fetch_rules_for_goal(goal):\n",
" lhs, rhs = parse_definite_clause(standardize_variables(rule))\n",
" for theta1 in fol_bc_and(KB, lhs, unify(rhs, goal, theta)):\n",
" yield theta1\n",
"
def fol_bc_and(KB, goals, theta):\n",
" if theta is None:\n",
" pass\n",
" elif not goals:\n",
" yield theta\n",
" else:\n",
" first, rest = goals[0], goals[1:]\n",
" for theta1 in fol_bc_or(KB, subst(theta, first), theta):\n",
" for theta2 in fol_bc_and(KB, rest, theta1):\n",
" yield theta2\n",
"