Transcript Game Playing - BTechSpot.com

S P Vimal, Department of CSIS, BITS, Pilani
Agenda
2



A quick review of syntax & semantics
Entailment in Propositional Logic
Discussion
EA C461 Artificial Intelligence
Review: Propositional logic: Syntax
3

Propositional logic is the simplest logic

Atomic sentence : A Propositional symbol (written
in upper case, just for notational convenience)


W1,3 – Wumpus is in room (1,3)
True / False
EA C461 Artificial Intelligence
Review: Propositional logic: Syntax
4






If S is a sentence, S is a sentence (negation)
If S1 and S2 are sentences, (S1  S2)is a sentence
(conjunction)
If S1 and S2 are sentences, ( S1  S2) is a sentence
(disjunction)
If S1 and S2 are sentences, (S1  S2) is a sentence
(implication)
If S1 and S2 are sentences, (S1  S2) is a sentence
(biconditional)
Precedence   ,  ,  ,  , 
EA C461 Artificial Intelligence
Semantics


Defines the rules for defining the truth of a sentence w.r.t a
particular model.
Let the sentence in the KB make use of the proposition
symbols P12,P22,P31.
 One possible model is m1 = {P12=true,P22=false,P31=true}
With these symbols, 8 possible models, can be enumerated automatically.
Rules for evaluating truth with respect to a model m:
S is true iff
S is false
S1  S2 is true iff
S1 is true and S2 is true
S1  S2 is true iff
S1is true or S2 is true
S1  S2 is true iff
S1 is false or S2 is true
i.e.,
is false iff S1 is true and S2 is false
S1  S2 is true iff
S1S2 is true and S2S1 is true
Review: Truth tables for connectives
6
EA C461 Artificial Intelligence
Wumpus world sentences
7
Assume a wumpus world without wumpus (??)
Let Pi,j be true if there is a pit in [i, j].
Let Bi,j be true if there is a breeze in [i, j].
R1:  P1,1

"Pits cause breezes in adjacent squares"
R2: B1,1  (P1,2  P2,1)
R3: B2,1  (P1,1  P2,2  P3,1)
R4: B1,1
R5: B2,1
EA C461 Artificial Intelligence
Truth tables for inference
8
EA C461 Artificial Intelligence
Inference by enumeration
9

Depth-first enumeration of all models is sound and complete

For n symbols, time complexity is O(2n), space complexity is O(n)
EA C461 Artificial Intelligence
Equivalence


Two sentences α and β are equivalent, if they are
true in the same set of models, which is written as
α <=> β
In other words, α ≡ β if and only if α ╞ β and β ╞ α
Validity


A sentence is valid, if it is true in all models

Example : P V ‫ ר‬P

Tautologies
Deduction theorem:
For any sentence α and β, α ╞ β if and only if (α ╞ β )
valid

Now, What is inference?



Rephrase in terms of Deduction Theorem?
All you do is to check the validity of KB╞ α
Conversely???
Conversely, every valid implication represents an inference.
Satisfiablity



A sentence is satisfiable if it is true in some model.
If a sentence α is true in model m, then m satisfies
α, or we say m is the model of α.
How do you verify if a sentence is satisfiable?


Enumerate the possible models, until one is found to
satisfy.
Many problems in Computer Science can be
reduced to a satisfiablity problems

Ex. CSP is all about verifying if the constraints are
satisfiable by some assignments
Connection between Validity and Satisfiablity



α is valid iff ‫ר‬α is not satisfiable
How do we use this observation for ‘entailment’?
Let us phrase it this way
α╞ β if and only if the sentence (α Λ ‫ר‬β ) is not
satisfiable.

Reduction to an absurd thing / Proof by refutation /
Proof by contradiction
Proof methods
14

Proof methods divide into (roughly) two kinds:
 Application of inference rules




Legitimate (sound) generation of new sentences from old
Proof = a sequence of inference rule applications
Can use inference rules as operators in a standard search
algorithm
Typically require transformation of sentences into a normal form
Model checking



truth table enumeration (always exponential in n)
improved backtracking, e.g., Davis--Putnam-Logemann-Loveland
(DPLL)
heuristic search in model space (sound but incomplete)
e.g., min-conflicts-like hill-climbing algorithms
EA C461 Artificial Intelligence
A property
15

Monotonicity
Set of entailed sentences can only increase as information is
added to the knowledge base.
 If KB╞ β then KB Λ α╞ β


Inference rules can be applied whenever suitable
premises are found in the Knowledge base.
EA C461 Artificial Intelligence
Resolution
16
Conjunctive Normal Form (CNF)
conjunction of disjunctions of literals
clauses
E.g., (A  B)  (B  C  D)

Resolution inference rule (for CNF):
li …  lk,
m1  …  mn
li  …  li-1  li+1  …  lk  m1  …  mj-1  mj+1 ...  mn
where li and mj are complementary literals.
E.g.,

P1,3  P2,2, P2,2
P1,3
Resolution is sound and complete
for propositional logic
EA C461 Artificial Intelligence
Resolution algorithm
17

Proof by contradiction, i.e., show KBα unsatisfiable
EA C461 Artificial Intelligence
Resolution example
18

KB = (B1,1  (P1,2 P2,1))  B1,1

α = P1,2
EA C461 Artificial Intelligence
Completeness of Resolution
19

Resolution Closure (RC)
RC(S) – set of clauses derivable by repeated application of
resolution rule to clauses in S or their derivatives
RC(S) must be finite
Completeness is entailed by “Ground Resolution Theorem”
 “If a set of clauses is unsatisfiable, then the resolution closure
of those clauses contains the empty clause ”



EA C461 Artificial Intelligence
Contd…
20
Any complete search algorithm, applying only resolution can
derive any conclusion entailed by any knowledge base in
propositional logic

This is true only in restricted sense
Resolution can always be used to either confirm or refute a
sentence
 Resolution cannot be used to enumerate entailed sentences


Refutation completeness
EA C461 Artificial Intelligence
Forward and backward chaining
21

Horn Form (restricted)
KB = conjunction of Horn clauses
 Horn clause =


proposition symbol; or
(conjunction of symbols)  symbol
E.g., C  (B  A)  (C  D  B)
Modus Ponens (for Horn Form): complete for Horn KBs




α1, … ,αn,
α1  …  αn  β
β
Can be used with forward chaining or backward chaining.
These algorithms are very natural and run in linear time
EA C461 Artificial Intelligence
Forward chaining
22

Idea: fire any rule whose premises are satisfied in the KB,

add its conclusion to the KB, until query is found
EA C461 Artificial Intelligence
Forward chaining algorithm
23

Forward chaining is sound and complete for Horn KB
EA C461 Artificial Intelligence
Forward chaining example
24
EA C461 Artificial Intelligence
Forward chaining example
25
EA C461 Artificial Intelligence
Forward chaining example
26
EA C461 Artificial Intelligence
Forward chaining example
27
EA C461 Artificial Intelligence
Forward chaining example
28
EA C461 Artificial Intelligence
Forward chaining example
29
EA C461 Artificial Intelligence
Forward chaining example
30
EA C461 Artificial Intelligence
Forward chaining example
31
EA C461 Artificial Intelligence
Proof of completeness
32

FC derives every atomic sentence that is entailed by KB
1.
FC reaches a fixed point where no new atomic sentences
are derived
2.
Consider the final state as a model m, assigning true/false
to symbols
3.
Every clause in the original KB is true in m
a1  …  ak  b
4.
5.
Hence m is a model of KB
If KB╞ q, q is true in every model of KB, including m
EA C461 Artificial Intelligence
Backward chaining
33
Idea: work backwards from the query q:
to prove q by BC,
check if q is known already, or
prove by BC all premises of some rule concluding q
Avoid loops: check if new subgoal is already on the goal stack
Avoid repeated work: check if new subgoal
1.
has already been proved true, or
2.
has already failed
EA C461 Artificial Intelligence
Backward chaining example
34
EA C461 Artificial Intelligence
Backward chaining example
35
EA C461 Artificial Intelligence
Backward chaining example
36
EA C461 Artificial Intelligence
Backward chaining example
37
EA C461 Artificial Intelligence
Backward chaining example
38
EA C461 Artificial Intelligence
Backward chaining example
39
EA C461 Artificial Intelligence
Backward chaining example
40
EA C461 Artificial Intelligence
Backward chaining example
41
EA C461 Artificial Intelligence
Backward chaining example
42
EA C461 Artificial Intelligence
Backward chaining example
43
EA C461 Artificial Intelligence
Forward vs. backward chaining
44




FC is data-driven, automatic, unconscious processing,
 e.g., object recognition, routine decisions
May do lots of work that is irrelevant to the goal
BC is goal-driven, appropriate for problem-solving,
 e.g., Where are my keys? How do I get into a PhD program?
Complexity of BC can be much less than linear in size of KB
EA C461 Artificial Intelligence
Refining model checking



Algorithms checks satisfiability
The connection between finding a solution to a CSP and
finding satisfying model for a logical sentence implies the
existence of backtracking algorithm
DPLL (Davis, Putnam, Logemann & Loveland)
The DPLL algorithm
46
Determine if an input propositional logic sentence (in CNF) is satisfiable.
Improvements over truth table enumeration:
1.
Early termination
A clause is true if any literal is true.
A sentence is false if any clause is false.
2.
Pure symbol heuristic
Pure symbol: always appears with the same "sign" in all clauses.
e.g., In the three clauses (A  B), (B  C), (C  A), A and B are pure, C
is impure.
Make a pure symbol literal true.
3.
Unit clause heuristic
Unit clause: only one literal in the clause
The only literal in a unit clause must be true.
EA C461 Artificial Intelligence
The DPLL algorithm
47
EA C461 Artificial Intelligence
The WalkSAT algorithm
48



Incomplete, local search algorithm
Evaluation function: The min-conflict heuristic of minimizing the
number of unsatisfied clauses
Balance between greediness and randomness
EA C461 Artificial Intelligence
The WalkSAT algorithm
49
EA C461 Artificial Intelligence
Hard satisfiability problems
50

Consider randomly generated 3-CNF sentences. e.g.,
(D  B  C)  (B  A  C)  (C  B  E)  (E
 D  B)  (B  E  C)
m = number of clauses
n = number of symbols



This CNF has 16 models out of 32 possible assignments.
Quite easy to solve.
So where are hard problems?
 Fix n and keep increasing m,
EA C461 Artificial Intelligence
Hard satisfiability problems
51
EA C461 Artificial Intelligence
Hard satisfiability problems
52
0

Median runtime for 100 satisfiable random 3-CNF sentences
EA C461 Artificial Intelligence
Inference-based agents in the Wumpus world
53
A wumpus-world agent using propositional logic:
P1,1
W1,1
Bx,y  (Px,y+1  Px,y-1  Px+1,y  Px-1,y)
Sx,y  (Wx,y+1  Wx,y-1  Wx+1,y  Wx-1,y)
W1,1  W1,2  …  W4,4
W1,1  W1,2
W1,1  W1,3
…
 64 distinct proposition symbols, 155 sentences
EA C461 Artificial Intelligence
54
EA C461 Artificial Intelligence
Keeping Track of Location and Orientation
55
Should our KB include statements like
L11  Facing Right  Forward  L 21
What is the problem here?
L111 Facing Right1  Forward1  L 212
Facing Right  TurnLeft 1  FacingUp2
Result : tens of thousands of such sentences 
EA C461 Artificial Intelligence
Summary
56


Logical agents apply inference to a knowledge base to derive new
information and make decisions
Basic concepts of logic:









syntax: formal structure of sentences
semantics: truth of sentences wrt models
entailment: necessary truth of one sentence given another
inference: deriving sentences from other sentences
soundness: derivations produce only entailed sentences
completeness: derivations can produce all entailed sentences
Wumpus world requires the ability to represent partial and negated
information, reason by cases, etc.
Resolution is complete for propositional logic
Forward, backward chaining are linear-time, complete for Horn clauses
Propositional logic lacks expressive power
EA C461 Artificial Intelligence