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. We make use of the implementations in the logic.py module. See the intro notebook for instructions.
Let's first import everything from the logic
module.
from utils import *
from logic import *
from notebook import psource
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
:
Symbol('x')
x
Or we can define multiple symbols at the same time with the function symbols
:
(x, y, P, Q, f) = symbols('x, y, P, Q, f')
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":
P & ~Q
(P & ~Q)
This works because the Expr
class overloads the &
operator with this definition:
def __and__(self, other): return Expr('&', self, other)```
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:
sentence = P & ~Q
sentence.op
'&'
sentence.args
(P, ~Q)
P.op
'P'
P.args
()
Pxy = P(x, y)
Pxy.op
'P'
Pxy.args
(x, y)
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. 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
:
3 * f(x, y) + P(y) / 2 + 1
(((3 * f(x, y)) + (P(y) / 2)) + 1)
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:
Operation | Book | Python Infix Input | Python Output | Python Expr Input |
---|---|---|---|---|
Negation | ¬ P | ~P |
~P |
Expr('~', P) |
And | P ∧ Q | P & Q |
P & Q |
Expr('&', P, Q) |
Or | P ∨ Q | P | Q |
P | Q |
Expr(' |', P, Q) |
Inequality (Xor) | P ≠ Q | P ^ Q |
P ^ Q |
Expr('^', P, Q) |
Implication | P → Q | P |'==>' | Q |
P ==> Q |
Expr('==>', P, Q) |
Reverse Implication | Q ← P | Q |'<==' | P |
Q <== P |
Expr('<==', Q, P) |
Equivalence | P ↔ Q | P |'<=>' | Q |
P <=> Q |
Expr('<=>', P, Q) |
Here's an example of defining a sentence with an implication arrow:
~(P & Q) |'==>'| (~P | ~Q)
(~(P & Q) ==> (~P | ~Q))
expr
: a Shortcut for Constructing Sentences¶If the |'==>'|
notation looks ugly to you, you can use the function expr
instead:
expr('~(P & Q) ==> (~P | ~Q)')
(~(P & Q) ==> (~P | ~Q))
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:
expr('sqrt(b ** 2 - 4 * a * c)')
sqrt(((b ** 2) - ((4 * a) * c)))
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.
PropKB
¶The class PropKB
can be used to represent a knowledge base of propositional logic sentences.
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.
The class PropKB
now.
__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.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.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
.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.Let us create a PropKB
for the wumpus world with the sentences mentioned in section 7.4.3
.
wumpus_kb = PropKB()
We define the symbols we use in our clauses.
$P_{x, y}$ is true if there is a pit in [x, y]
.
$B_{x, y}$ is true if the agent senses breeze in [x, y]
.
P11, P12, P21, P22, P31, B11, B21 = expr('P11, P12, P21, P22, P31, B11, B21')
Now we tell sentences based on section 7.4.3
.
There is no pit in [1,1]
.
wumpus_kb.tell(~P11)
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.
wumpus_kb.tell(B11 | '<=>' | ((P12 | P21)))
wumpus_kb.tell(B21 | '<=>' | ((P11 | P22 | P31)))
Now we include the breeze percepts for the first two squares leading up to the situation in Figure 7.3(b)
wumpus_kb.tell(~B11)
wumpus_kb.tell(B21)
We can check the clauses stored in a KB
by accessing its clauses
variable
wumpus_kb.clauses
[~P11, (~P12 | B11), (~P21 | B11), (P12 | P21 | ~B11), (~P11 | B21), (~P22 | B21), (~P31 | B21), (P11 | P22 | P31 | ~B21), ~B11, B21]
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
.
$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})$.
$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}$.
$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.
$B_{2, 1} \iff (P_{1, 1} \lor P_{2, 2} \lor P_{3, 2})$ is converted in similar manner.
A knowledge-based agent is a simple generic agent that maintains and handles a knowledge base. The knowledge base may initially contain some background knowledge.
psource(KB_AgentProgram)
def KB_AgentProgram(KB):
"""A generic logical knowledge-based agent program. [Figure 7.1]"""
steps = itertools.count()
def program(percept):
t = next(steps)
KB.tell(make_percept_sentence(percept, t))
action = KB.ask(make_action_query(t))
KB.tell(make_action_sentence(action, t))
return action
def make_percept_sentence(percept, t):
return Expr("Percept")(percept, t)
def make_action_query(t):
return expr("ShouldDo(action, {})".format(t))
def make_action_sentence(action, t):
return Expr("Did")(action[expr('action')], t)
return program
The helper functions make_percept_sentence
, make_action_query
and make_action_sentence
are all aptly named and as expected,
make_percept_sentence
makes first-order logic sentences about percepts we want our agent to receive,
make_action_query
asks the underlying KB
about the action that should be taken and
make_action_sentence
tells the underlying KB
about the action it has just taken.
In this section we will look at two algorithms to check if a sentence is entailed by the KB
. Our goal is to decide whether $\text{KB} \vDash \alpha$ for some sentence $\alpha$.
It is a model-checking approach which, as the name suggests, enumerates all possible models in which the KB
is true and checks if $\alpha$ is also true in these models. We list the $n$ symbols in the KB
and enumerate the $2^{n}$ models in a depth-first manner and check the truth of KB
and $\alpha$.
psource(tt_check_all)
def tt_check_all(kb, alpha, symbols, model):
"""Auxiliary routine to implement tt_entails."""
if not symbols:
if pl_true(kb, model):
result = pl_true(alpha, model)
assert result in (True, False)
return result
else:
return True
else:
P, rest = symbols[0], symbols[1:]
return (tt_check_all(kb, alpha, rest, extend(model, P, True)) and
tt_check_all(kb, alpha, rest, extend(model, P, False)))
The algorithm basically computes every line of the truth table $KB\implies \alpha$ and checks if it is true everywhere.
psource(tt_entails)
def tt_entails(kb, alpha):
"""Does kb entail the sentence alpha? Use truth tables. For propositional
kb's and sentences. [Figure 7.10]. Note that the 'kb' should be an
Expr which is a conjunction of clauses.
>>> tt_entails(expr('P & Q'), expr('Q'))
True
"""
assert not variables(alpha)
symbols = list(prop_symbols(kb & alpha))
return tt_check_all(kb, alpha, symbols, {})
Keep in mind that for two symbols P and Q, P => Q is false only when P is True
and Q is False
.
Example usage of tt_entails()
:
tt_entails(P & Q, Q)
True
P & Q is True only when both P and Q are True. Hence, (P & Q) => Q is True
tt_entails(P | Q, Q)
False
tt_entails(P | Q, P)
False
If we know that P | Q is true, we cannot infer the truth values of P and Q. Hence (P | Q) => Q is False and so is (P | Q) => P.
(A, B, C, D, E, F, G) = symbols('A, B, C, D, E, F, G')
tt_entails(A & (B | C) & D & E & ~(F | G), A & D & E & ~F & ~G)
True
We can see that for the KB to be true, A, D, E have to be True and F and G have to be False. Nothing can be said about B or C.
Coming back to our problem, note that tt_entails()
takes an Expr
which is a conjunction of clauses as the input instead of the KB
itself.
You can use the ask_if_true()
method of PropKB
which does all the required conversions.
Let's check what wumpus_kb
tells us about $P_{1, 1}$.
wumpus_kb.ask_if_true(~P11), wumpus_kb.ask_if_true(P11)
(True, False)
Looking at Figure 7.9 we see that in all models in which the knowledge base is True
, $P_{1, 1}$ is False
. It makes sense that ask_if_true()
returns True
for $\alpha = \neg P_{1, 1}$ and False
for $\alpha = P_{1, 1}$. This begs the question, what if $\alpha$ is True
in only a portion of all models. Do we return True
or False
? This doesn't rule out the possibility of $\alpha$ being True
but it is not entailed by the KB
so we return False
in such cases. We can see this is the case for $P_{2, 2}$ and $P_{3, 1}$.
wumpus_kb.ask_if_true(~P22), wumpus_kb.ask_if_true(P22)
(False, False)
Recall that our goal is to check whether $\text{KB} \vDash \alpha$ i.e. is $\text{KB} \implies \alpha$ true in every model. Suppose we wanted to check if $P \implies Q$ is valid. We check the satisfiability of $\neg (P \implies Q)$, which can be rewritten as $P \land \neg Q$. If $P \land \neg Q$ is unsatisfiable, then $P \implies Q$ must be true in all models. This gives us the result "$\text{KB} \vDash \alpha$ if and only if $\text{KB} \land \neg \alpha$ is unsatisfiable".
This technique corresponds to proof by contradiction, a standard mathematical proof technique. We assume $\alpha$ to be false and show that this leads to a contradiction with known axioms in $\text{KB}$. We obtain a contradiction by making valid inferences using inference rules. In this proof we use a single inference rule, resolution which states $(l_1 \lor \dots \lor l_k) \land (m_1 \lor \dots \lor m_n) \land (l_i \iff \neg m_j) \implies l_1 \lor \dots \lor l_{i - 1} \lor l_{i + 1} \lor \dots \lor l_k \lor m_1 \lor \dots \lor m_{j - 1} \lor m_{j + 1} \lor \dots \lor m_n$. Applying the resolution yields us a clause which we add to the KB. We keep doing this until:
The empty clause is equivalent to False because it arises only from resolving two complementary unit clauses such as $P$ and $\neg P$ which is a contradiction as both $P$ and $\neg P$ can't be True at the same time.
There is one catch however, the algorithm that implements proof by resolution cannot handle complex sentences. Implications and bi-implications have to be simplified into simpler clauses. We already know that every sentence of a propositional logic is logically equivalent to a conjunction of clauses. We will use this fact to our advantage and simplify the input sentence into the conjunctive normal form (CNF) which is a conjunction of disjunctions of literals. For eg:
psource(to_cnf)
def to_cnf(s):
"""Convert a propositional logical sentence to conjunctive normal form.
That is, to the form ((A | ~B | ...) & (B | C | ...) & ...) [p. 253]
>>> to_cnf('~(B | C)')
(~B & ~C)
"""
s = expr(s)
if isinstance(s, str):
s = expr(s)
s = eliminate_implications(s) # Steps 1, 2 from p. 253
s = move_not_inwards(s) # Step 3
return distribute_and_over_or(s) # Step 4
to_cnf
calls three subroutines.
psource(eliminate_implications)
psource(move_not_inwards)
psource(distribute_and_over_or)
def eliminate_implications(s):
"""Change implications into equivalent form with only &, |, and ~ as logical operators."""
s = expr(s)
if not s.args or is_symbol(s.op):
return s # Atoms are unchanged.
args = list(map(eliminate_implications, s.args))
a, b = args[0], args[-1]
if s.op == '==>':
return b | ~a
elif s.op == '<==':
return a | ~b
elif s.op == '<=>':
return (a | ~b) & (b | ~a)
elif s.op == '^':
assert len(args) == 2 # TODO: relax this restriction
return (a & ~b) | (~a & b)
else:
assert s.op in ('&', '|', '~')
return Expr(s.op, *args)
def move_not_inwards(s):
"""Rewrite sentence s by moving negation sign inward.
>>> move_not_inwards(~(A | B))
(~A & ~B)"""
s = expr(s)
if s.op == '~':
def NOT(b):
return move_not_inwards(~b)
a = s.args[0]
if a.op == '~':
return move_not_inwards(a.args[0]) # ~~A ==> A
if a.op == '&':
return associate('|', list(map(NOT, a.args)))
if a.op == '|':
return associate('&', list(map(NOT, a.args)))
return s
elif is_symbol(s.op) or not s.args:
return s
else:
return Expr(s.op, *list(map(move_not_inwards, s.args)))
def distribute_and_over_or(s):
"""Given a sentence s consisting of conjunctions and disjunctions
of literals, return an equivalent sentence in CNF.
>>> distribute_and_over_or((A & B) | C)
((A | C) & (B | C))
"""
s = expr(s)
if s.op == '|':
s = associate('|', s.args)
if s.op != '|':
return distribute_and_over_or(s)
if len(s.args) == 0:
return False
if len(s.args) == 1:
return distribute_and_over_or(s.args[0])
conj = first(arg for arg in s.args if arg.op == '&')
if not conj:
return s
others = [a for a in s.args if a is not conj]
rest = associate('|', others)
return associate('&', [distribute_and_over_or(c | rest)
for c in conj.args])
elif s.op == '&':
return associate('&', list(map(distribute_and_over_or, s.args)))
else:
return s
Let's convert some sentences to see how it works
A, B, C, D = expr('A, B, C, D')
to_cnf(A |'<=>'| B)
((A | ~B) & (B | ~A))
to_cnf(A |'<=>'| (B & C))
((A | ~B | ~C) & (B | ~A) & (C | ~A))
to_cnf(A & (B | (C & D)))
(A & (C | B) & (D | B))
to_cnf((A |'<=>'| ~B) |'==>'| (C | ~D))
((B | ~A | C | ~D) & (A | ~A | C | ~D) & (B | ~B | C | ~D) & (A | ~B | C | ~D))
Coming back to our resolution problem, we can see how the to_cnf
function is utilized here
psource(pl_resolution)
def pl_resolution(KB, alpha):
"""Propositional-logic resolution: say if alpha follows from KB. [Figure 7.12]"""
clauses = KB.clauses + conjuncts(to_cnf(~alpha))
new = set()
while True:
n = len(clauses)
pairs = [(clauses[i], clauses[j])
for i in range(n) for j in range(i+1, n)]
for (ci, cj) in pairs:
resolvents = pl_resolve(ci, cj)
if False in resolvents:
return True
new = new.union(set(resolvents))
if new.issubset(set(clauses)):
return False
for c in new:
if c not in clauses:
clauses.append(c)
pl_resolution(wumpus_kb, ~P11), pl_resolution(wumpus_kb, P11)
(True, False)
pl_resolution(wumpus_kb, ~P22), pl_resolution(wumpus_kb, P22)
(False, False)
Previously, we said we will look at two algorithms to check if a sentence is entailed by the KB
. Here's a third one.
The difference here is that our goal now is to determine if a knowledge base of definite clauses entails a single proposition symbol q - the query.
There is a catch however - the knowledge base can only contain Horn clauses.
psource(PropDefiniteKB.clauses_with_premise)
def clauses_with_premise(self, p):
"""Return a list of the clauses in KB that have p in their premise.
This could be cached away for O(1) speed, but we'll recompute it."""
return [c for c in self.clauses
if c.op == '==>' and p in conjuncts(c.args[0])]
Let's now have a look at the pl_fc_entails
algorithm.
psource(pl_fc_entails)
def pl_fc_entails(KB, q):
"""Use forward chaining to see if a PropDefiniteKB entails symbol q.
[Figure 7.15]
>>> pl_fc_entails(horn_clauses_KB, expr('Q'))
True
"""
count = {c: len(conjuncts(c.args[0]))
for c in KB.clauses
if c.op == '==>'}
inferred = defaultdict(bool)
agenda = [s for s in KB.clauses if is_prop_symbol(s.op)]
while agenda:
p = agenda.pop()
if p == q:
return True
if not inferred[p]:
inferred[p] = True
for c in KB.clauses_with_premise(p):
count[c] -= 1
if count[c] == 0:
agenda.append(c.args[1])
return False
The function accepts a knowledge base KB
(an instance of PropDefiniteKB
) and a query q
as inputs.
clauses = ['(B & F)==>E',
'(A & E & F)==>G',
'(B & C)==>F',
'(A & B)==>D',
'(E & F)==>H',
'(H & I)==>J',
'A',
'B',
'C']
We will now tell
this information to our knowledge base.
definite_clauses_KB = PropDefiniteKB()
for clause in clauses:
definite_clauses_KB.tell(expr(clause))
We can now check if our knowledge base entails the following queries.
pl_fc_entails(definite_clauses_KB, expr('G'))
True
pl_fc_entails(definite_clauses_KB, expr('H'))
True
pl_fc_entails(definite_clauses_KB, expr('I'))
False
pl_fc_entails(definite_clauses_KB, expr('J'))
False
The previous segments elucidate the algorithmic procedure for model checking. In this segment, we look at ways of making them computationally efficient.
This algorithm is very similar to Backtracking-Search.
It recursively enumerates possible models in a depth-first fashion with the following improvements over algorithms like tt_entails
:
psource(dpll)
def dpll(clauses, symbols, model):
"""See if the clauses are true in a partial model."""
unknown_clauses = [] # clauses with an unknown truth value
for c in clauses:
val = pl_true(c, model)
if val is False:
return False
if val is not True:
unknown_clauses.append(c)
if not unknown_clauses:
return model
P, value = find_pure_symbol(symbols, unknown_clauses)
if P:
return dpll(clauses, removeall(P, symbols), extend(model, P, value))
P, value = find_unit_clause(clauses, model)
if P:
return dpll(clauses, removeall(P, symbols), extend(model, P, value))
if not symbols:
raise TypeError("Argument should be of the type Expr.")
P, symbols = symbols[0], symbols[1:]
return (dpll(clauses, symbols, extend(model, P, True)) or
dpll(clauses, symbols, extend(model, P, False)))
The algorithm uses the ideas described above to check satisfiability of a sentence in propositional logic.
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.
psource(dpll_satisfiable)
def dpll_satisfiable(s):
"""Check satisfiability of a propositional sentence.
This differs from the book code in two ways: (1) it returns a model
rather than True when it succeeds; this is more useful. (2) The
function find_pure_symbol is passed a list of unknown clauses, rather
than a list of all clauses and the model; this is more efficient."""
clauses = conjuncts(to_cnf(s))
symbols = list(prop_symbols(s))
return dpll(clauses, symbols, {})
Let's see a few examples of usage.
A, B, C, D = expr('A, B, C, D')
dpll_satisfiable(A & B & ~C & D)
{A: True, B: True, C: False, D: True}
This is a simple case to highlight that the algorithm actually works.
dpll_satisfiable((A & B) | (C & ~A) | (B & ~D))
{B: True, C: True, D: False}
If a particular symbol isn't present in the solution, it means that the solution is independent of the value of that symbol. In this case, the solution is independent of A.
dpll_satisfiable(A |'<=>'| B)
{A: True, B: True}
dpll_satisfiable((A |'<=>'| B) |'==>'| (C & ~A))
{A: False, B: True, C: True}
dpll_satisfiable((A | (B & C)) |'<=>'| ((A | B) & (A | C)))
{B: True, C: True}
This algorithm is very similar to Hill climbing.
On every iteration, the algorithm picks an unsatisfied clause and flips a symbol in the clause.
This is similar to finding a neighboring state in the hill_climbing
algorithm.
psource(WalkSAT)
def WalkSAT(clauses, p=0.5, max_flips=10000):
"""Checks for satisfiability of all clauses by randomly flipping values of variables
"""
# Set of all symbols in all clauses
symbols = {sym for clause in clauses for sym in prop_symbols(clause)}
# model is a random assignment of true/false to the symbols in clauses
model = {s: random.choice([True, False]) for s in symbols}
for i in range(max_flips):
satisfied, unsatisfied = [], []
for clause in clauses:
(satisfied if pl_true(clause, model) else unsatisfied).append(clause)
if not unsatisfied: # if model satisfies all the clauses
return model
clause = random.choice(unsatisfied)
if probability(p):
sym = random.choice(list(prop_symbols(clause)))
else:
# Flip the symbol in clause that maximizes number of sat. clauses
def sat_count(sym):
# Return the the number of clauses satisfied after flipping the symbol.
model[sym] = not model[sym]
count = len([clause for clause in clauses if pl_true(clause, model)])
model[sym] = not model[sym]
return count
sym = argmax(prop_symbols(clause), key=sat_count)
model[sym] = not model[sym]
# If no solution is found within the flip limit, we return failure
return None
The function takes three arguments:
A, B, C, D = expr('A, B, C, D')
WalkSAT([A, B, ~C, D], 0.5, 100)
{A: True, B: True, C: False, D: True}
This is a simple case to show that the algorithm converges.
WalkSAT([A & B, A & C], 0.5, 100)
{A: True, B: True, C: True}
WalkSAT([A & B, C & D, C & B], 0.5, 100)
{A: True, B: True, C: True, D: True}
WalkSAT([A & B, C | D, ~(D | B)], 0.5, 1000)
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.
One point of difference between this algorithm and the dpll_satisfiable
algorithms is that both these algorithms take inputs differently.
For WalkSAT to take complete sentences as input,
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.
def WalkSAT_CNF(sentence, p=0.5, max_flips=10000):
return WalkSAT(conjuncts(to_cnf(sentence)), 0, max_flips)
Now we can call WalkSAT_CNF
and DPLL_Satisfiable
with the same arguments.
WalkSAT_CNF((A & B) | (C & ~A) | (B & ~D), 0.5, 1000)
{A: True, B: True, C: False, D: True}
It works!
sentence_1 = A |'<=>'| B
sentence_2 = (A & B) | (C & ~A) | (B & ~D)
sentence_3 = (A | (B & C)) |'<=>'| ((A | B) & (A | C))
%%timeit
dpll_satisfiable(sentence_1)
dpll_satisfiable(sentence_2)
dpll_satisfiable(sentence_3)
1.55 ms ± 64.6 µs per loop (mean ± std. dev. of 7 runs, 1000 loops each)
%%timeit
WalkSAT_CNF(sentence_1)
WalkSAT_CNF(sentence_2)
WalkSAT_CNF(sentence_3)
1.02 ms ± 6.92 µs per loop (mean ± std. dev. of 7 runs, 1000 loops each)
On an average, for solvable cases, WalkSAT
is quite faster than dpll
because, for a small number of variables,
WalkSAT
can reduce the search space significantly.
Results can be different for sentences with more symbols though.
Feel free to play around with this to understand the trade-offs of these algorithms better.
In this section we show how to make plans by logical inference. The basic idea is very simple. It includes the following three steps:
Lets have a look at the algorithm
psource(SAT_plan)
def SAT_plan(init, transition, goal, t_max, SAT_solver=dpll_satisfiable):
"""Converts a planning problem to Satisfaction problem by translating it to a cnf sentence.
[Figure 7.22]"""
# Functions used by SAT_plan
def translate_to_SAT(init, transition, goal, time):
clauses = []
states = [state for state in transition]
# Symbol claiming state s at time t
state_counter = itertools.count()
for s in states:
for t in range(time+1):
state_sym[s, t] = Expr("State_{}".format(next(state_counter)))
# Add initial state axiom
clauses.append(state_sym[init, 0])
# Add goal state axiom
clauses.append(state_sym[goal, time])
# All possible transitions
transition_counter = itertools.count()
for s in states:
for action in transition[s]:
s_ = transition[s][action]
for t in range(time):
# Action 'action' taken from state 's' at time 't' to reach 's_'
action_sym[s, action, t] = Expr(
"Transition_{}".format(next(transition_counter)))
# Change the state from s to s_
clauses.append(action_sym[s, action, t] |'==>'| state_sym[s, t])
clauses.append(action_sym[s, action, t] |'==>'| state_sym[s_, t + 1])
# Allow only one state at any time
for t in range(time+1):
# must be a state at any time
clauses.append(associate('|', [state_sym[s, t] for s in states]))
for s in states:
for s_ in states[states.index(s) + 1:]:
# for each pair of states s, s_ only one is possible at time t
clauses.append((~state_sym[s, t]) | (~state_sym[s_, t]))
# Restrict to one transition per timestep
for t in range(time):
# list of possible transitions at time t
transitions_t = [tr for tr in action_sym if tr[2] == t]
# make sure at least one of the transitions happens
clauses.append(associate('|', [action_sym[tr] for tr in transitions_t]))
for tr in transitions_t:
for tr_ in transitions_t[transitions_t.index(tr) + 1:]:
# there cannot be two transitions tr and tr_ at time t
clauses.append(~action_sym[tr] | ~action_sym[tr_])
# Combine the clauses to form the cnf
return associate('&', clauses)
def extract_solution(model):
true_transitions = [t for t in action_sym if model[action_sym[t]]]
# Sort transitions based on time, which is the 3rd element of the tuple
true_transitions.sort(key=lambda x: x[2])
return [action for s, action, time in true_transitions]
# Body of SAT_plan algorithm
for t in range(t_max):
# dictionaries to help extract the solution from model
state_sym = {}
action_sym = {}
cnf = translate_to_SAT(init, transition, goal, t)
model = SAT_solver(cnf)
if model is not False:
return extract_solution(model)
return None
Let's see few examples of its usage. First we define a transition and then call SAT_plan
.
transition = {'A': {'Left': 'A', 'Right': 'B'},
'B': {'Left': 'A', 'Right': 'C'},
'C': {'Left': 'B', 'Right': 'C'}}
print(SAT_plan('A', transition, 'C', 2))
print(SAT_plan('A', transition, 'B', 3))
print(SAT_plan('C', transition, 'A', 3))
None ['Right'] ['Left', 'Left']
Let us do the same for another transition.
transition = {(0, 0): {'Right': (0, 1), 'Down': (1, 0)},
(0, 1): {'Left': (1, 0), 'Down': (1, 1)},
(1, 0): {'Right': (1, 0), 'Up': (1, 0), 'Left': (1, 0), 'Down': (1, 0)},
(1, 1): {'Left': (1, 0), 'Up': (0, 1)}}
print(SAT_plan((0, 0), transition, (1, 1), 4))
['Right', 'Down']
FolKB
¶The class FolKB
can be used to represent a knowledge base of First-order logic sentences. You would initialize and use it the same way as you would for PropKB
except that the clauses are first-order definite clauses. We will see how to write such clauses to create a database and query them in the following sections.
In this section we create a FolKB
based on the following paragraph.
The law says that it is a crime for an American to sell weapons to hostile nations. The country Nono, an enemy of America, has some missiles, and all of its missiles were sold to it by Colonel West, who is American.
The first step is to extract the facts and convert them into first-order definite clauses. Extracting the facts from data alone is a challenging task. Fortunately, we have a small paragraph and can do extraction and conversion manually. We'll store the clauses in list aptly named clauses
.
clauses = []
“... it is a crime for an American to sell weapons to hostile nations”
The keywords to look for here are 'crime', 'American', 'sell', 'weapon' and 'hostile'. We use predicate symbols to make meaning of them.
Criminal(x)
: x
is a criminalAmerican(x)
: x
is an AmericanSells(x ,y, z)
: x
sells y
to z
Weapon(x)
: x
is a weaponHostile(x)
: x
is a hostile nationLet us now combine them with appropriate variable naming to depict the meaning of the sentence. The criminal x
is also the American x
who sells weapon y
to z
, which is a hostile nation.
$\text{American}(x) \land \text{Weapon}(y) \land \text{Sells}(x, y, z) \land \text{Hostile}(z) \implies \text{Criminal} (x)$
clauses.append(expr("(American(x) & Weapon(y) & Sells(x, y, z) & Hostile(z)) ==> Criminal(x)"))
"The country Nono, an enemy of America"
We now know that Nono is an enemy of America. We represent these nations using the constant symbols Nono
and America
. the enemy relation is show using the predicate symbol Enemy
.
$\text{Enemy}(\text{Nono}, \text{America})$
clauses.append(expr("Enemy(Nono, America)"))
"Nono ... has some missiles"
This states the existence of some missile which is owned by Nono. $\exists x \text{Owns}(\text{Nono}, x) \land \text{Missile}(x)$. We invoke existential instantiation to introduce a new constant M1
which is the missile owned by Nono.
$\text{Owns}(\text{Nono}, \text{M1}), \text{Missile}(\text{M1})$
clauses.append(expr("Owns(Nono, M1)"))
clauses.append(expr("Missile(M1)"))
"All of its missiles were sold to it by Colonel West"
If Nono owns something and it classifies as a missile, then it was sold to Nono by West.
$\text{Missile}(x) \land \text{Owns}(\text{Nono}, x) \implies \text{Sells}(\text{West}, x, \text{Nono})$
clauses.append(expr("(Missile(x) & Owns(Nono, x)) ==> Sells(West, x, Nono)"))
"West, who is American"
West is an American.
$\text{American}(\text{West})$
clauses.append(expr("American(West)"))
We also know, from our understanding of language, that missiles are weapons and that an enemy of America counts as “hostile”.
$\text{Missile}(x) \implies \text{Weapon}(x), \text{Enemy}(x, \text{America}) \implies \text{Hostile}(x)$
clauses.append(expr("Missile(x) ==> Weapon(x)"))
clauses.append(expr("Enemy(x, America) ==> Hostile(x)"))
Now that we have converted the information into first-order definite clauses we can create our first-order logic knowledge base.
crime_kb = FolKB(clauses)
The subst
helper function substitutes variables with given values in first-order logic statements.
This will be useful in later algorithms.
It's implementation is quite simple and self-explanatory.
psource(subst)
def subst(s, x):
"""Substitute the substitution s into the expression x.
>>> subst({x: 42, y:0}, F(x) + y)
(F(42) + 0)
"""
if isinstance(x, list):
return [subst(s, xi) for xi in x]
elif isinstance(x, tuple):
return tuple([subst(s, xi) for xi in x])
elif not isinstance(x, Expr):
return x
elif is_var_symbol(x.op):
return s.get(x, x)
else:
return Expr(x.op, *[subst(s, arg) for arg in x.args])
Here's an example of how subst
can be used.
subst({x: expr('Nono'), y: expr('M1')}, expr('Owns(x, y)'))
Owns(Nono, M1)
In this section we look at a forward chaining and a backward chaining algorithm for FolKB
. Both aforementioned algorithms rely on a process called unification, a key component of all first-order inference algorithms.
We sometimes require finding substitutions that make different logical expressions look identical. This process, called unification, is done by the unify
algorithm. It takes as input two sentences and returns a unifier for them if one exists. A unifier is a dictionary which stores the substitutions required to make the two sentences identical. It does so by recursively unifying the components of a sentence, where the unification of a variable symbol var
with a constant symbol Const
is the mapping {var: Const}
. Let's look at a few examples.
unify(expr('x'), 3)
{x: 3}
unify(expr('A(x)'), expr('A(B)'))
{x: B}
unify(expr('Cat(x) & Dog(Dobby)'), expr('Cat(Bella) & Dog(y)'))
{x: Bella, y: Dobby}
In cases where there is no possible substitution that unifies the two sentences the function return None
.
print(unify(expr('Cat(x)'), expr('Dog(Dobby)')))
None
We also need to take care we do not unintentionally use the same variable name. Unify treats them as a single variable which prevents it from taking multiple value.
print(unify(expr('Cat(x) & Dog(Dobby)'), expr('Cat(Bella) & Dog(x)')))
None
We consider the simple forward-chaining algorithm presented in Figure 9.3. We look at each rule in the knowledge base and see if the premises can be satisfied. This is done by finding a substitution which unifies each of the premise with a clause in the KB
. If we are able to unify the premises, the conclusion (with the corresponding substitution) is added to the KB
. This inferencing process is repeated until either the query can be answered or till no new sentences can be added. We test if the newly added clause unifies with the query in which case the substitution yielded by unify
is an answer to the query. If we run out of sentences to infer, this means the query was a failure.
The function fol_fc_ask
is a generator which yields all substitutions which validate the query.
psource(fol_fc_ask)
def fol_fc_ask(KB, alpha):
"""A simple forward-chaining algorithm. [Figure 9.3]"""
# TODO: Improve efficiency
kb_consts = list({c for clause in KB.clauses for c in constant_symbols(clause)})
def enum_subst(p):
query_vars = list({v for clause in p for v in variables(clause)})
for assignment_list in itertools.product(kb_consts, repeat=len(query_vars)):
theta = {x: y for x, y in zip(query_vars, assignment_list)}
yield theta
# check if we can answer without new inferences
for q in KB.clauses:
phi = unify(q, alpha, {})
if phi is not None:
yield phi
while True:
new = []
for rule in KB.clauses:
p, q = parse_definite_clause(rule)
for theta in enum_subst(p):
if set(subst(theta, p)).issubset(set(KB.clauses)):
q_ = subst(theta, q)
if all([unify(x, q_, {}) is None for x in KB.clauses + new]):
new.append(q_)
phi = unify(q_, alpha, {})
if phi is not None:
yield phi
if not new:
break
for clause in new:
KB.tell(clause)
return None
Let's find out all the hostile nations. Note that we only told the KB
that Nono was an enemy of America, not that it was hostile.
answer = fol_fc_ask(crime_kb, expr('Hostile(x)'))
print(list(answer))
[{x: Nono}]
The generator returned a single substitution which says that Nono is a hostile nation. See how after adding another enemy nation the generator returns two substitutions.
crime_kb.tell(expr('Enemy(JaJa, America)'))
answer = fol_fc_ask(crime_kb, expr('Hostile(x)'))
print(list(answer))
[{x: Nono}, {x: JaJa}]
Note: fol_fc_ask
makes changes to the KB
by adding sentences to it.
This algorithm works backward from the goal, chaining through rules to find known facts that support the proof. Suppose goal
is the query we want to find the substitution for. We find rules of the form $\text{lhs} \implies \text{goal}$ in the KB
and try to prove lhs
. There may be multiple clauses in the KB
which give multiple lhs
. It is sufficient to prove only one of these. But to prove a lhs
all the conjuncts in the lhs
of the clause must be proved. This makes it similar to And/Or search.
The OR part of the algorithm comes from our choice to select any clause of the form $\text{lhs} \implies \text{goal}$. Looking at all rules's lhs
whose rhs
unify with the goal
, we yield a substitution which proves all the conjuncts in the lhs
. We use parse_definite_clause
to attain lhs
and rhs
from a clause of the form $\text{lhs} \implies \text{rhs}$. For atomic facts the lhs
is an empty list.
psource(fol_bc_or)
def fol_bc_or(KB, goal, theta):
for rule in KB.fetch_rules_for_goal(goal):
lhs, rhs = parse_definite_clause(standardize_variables(rule))
for theta1 in fol_bc_and(KB, lhs, unify(rhs, goal, theta)):
yield theta1
The AND corresponds to proving all the conjuncts in the lhs
. We need to find a substitution which proves each and every clause in the list of conjuncts.
psource(fol_bc_and)
def fol_bc_and(KB, goals, theta):
if theta is None:
pass
elif not goals:
yield theta
else:
first, rest = goals[0], goals[1:]
for theta1 in fol_bc_or(KB, subst(theta, first), theta):
for theta2 in fol_bc_and(KB, rest, theta1):
yield theta2
Now the main function fl_bc_ask
calls fol_bc_or
with substitution initialized as empty. The ask
method of FolKB
uses fol_bc_ask
and fetches the first substitution returned by the generator to answer query. Let's query the knowledge base we created from clauses
to find hostile nations.
# Rebuild KB because running fol_fc_ask would add new facts to the KB
crime_kb = FolKB(clauses)
crime_kb.ask(expr('Hostile(x)'))
{v_5: x, x: Nono}
You may notice some new variables in the substitution. They are introduced to standardize the variable names to prevent naming problems as discussed in the Unification section
|'==>'|
¶Consider the Expr
formed by this syntax:
P |'==>'| ~Q
(P ==> ~Q)
What is the funny |'==>'|
syntax? The trick is that "|
" is just the regular Python or-operator, and so is exactly equivalent to this:
(P | '==>') | ~Q
(P ==> ~Q)
In other words, there are two applications of or-operators. Here's the first one:
P | '==>'
PartialExpr('==>', P)
What is going on here is that the __or__
method of Expr
serves a dual purpose. If the right-hand-side is another Expr
(or a number), then the result is an Expr
, as in (P | Q)
. But if the right-hand-side is a string, then the string is taken to be an operator, and we create a node in the abstract syntax tree corresponding to a partially-filled Expr
, one where we know the left-hand-side is P
and the operator is ==>
, but we don't yet know the right-hand-side.
The PartialExpr
class has an __or__
method that says to create an Expr
node with the right-hand-side filled in. Here we can see the combination of the PartialExpr
with Q
to create a complete Expr
:
partial = PartialExpr('==>', P)
partial | ~Q
(P ==> ~Q)
This trick is due to Ferdinand Jamitzky, with a modification by C. G. Vedant, who suggested using a string inside the or-bars.
expr
¶How does expr
parse a string into an Expr
? It turns out there are two tricks (besides the Jamitzky/Vedant trick):
==>
" with "|'==>'|
" (and likewise for other operators).eval
the resulting string in an environment in which every identifieris bound to a symbol with that identifier as the op
.
In other words,
expr('~(P & Q) ==> (~P | ~Q)')
(~(P & Q) ==> (~P | ~Q))
is equivalent to doing:
P, Q = symbols('P, Q')
~(P & Q) |'==>'| (~P | ~Q)
(~(P & Q) ==> (~P | ~Q))
One thing to beware of: this puts ==>
at the same precedence level as "|"
, which is not quite right. For example, we get this:
P & Q |'==>'| P | Q
(((P & Q) ==> P) | Q)
which is probably not what we meant; when in doubt, put in extra parens:
(P & Q) |'==>'| (P | Q)
((P & Q) ==> (P | Q))
from notebook import Canvas_fol_bc_ask
canvas_bc_ask = Canvas_fol_bc_ask('canvas_bc_ask', crime_kb, expr('Criminal(x)'))
This notebook by Chirag Vartak and Peter Norvig.