Transcript Week 7

10/1
Project 2 will be given out by 10/3
Will likely be on Sudoku solving using
CSP techniques
Mid-term will likely be around 10/17
Facts
Objects
relations
FOPC
Prob
FOPC
Ontological
commitment
facts
Prob
prop
logic
Prop
logic
t/f/u
Epistemological
commitment
Deg
belief
Assertions;
t/f
Prop logic
Objects,
relations
First order predicate logic
(FOPC)
Time
Degree of
belief
Degree of
belief
Prob. Prop. logic
Objects,
relations
First order Temporal logic
(FOPC)
First order Prob. logic
Degree of
truth
Fuzzy Logic
What is “monotonic” vs. “nonmonotonic” logic?
• Prop calculus (as well as the first order logic we shall discuss later) are
monotonic, in that once you prove a fact F to be true, no amount of
additional knowledge can allow us to disprove F.
• But, in the real world, we jump to conclusions by default, and revise them
on additional evidence
– Consider the way the truth of the statement “F: Tweety Flies” is revised by us
when we are given facts in sequence: 1. Tweety is a bird (F)2. Tweety is an
Ostritch (~F) 3. Tweety is a magical Ostritch (F) 4. Tweety was cursed recently
(~F) 5. Tweety was able to get rid of the curse (F)
• How can we make logic show this sort of “defeasible” (aka defeatable)
conclusions?
– Many ideas, with one being negation as failure
– Let the rule about birds be Bird & ~abnormal => Fly
• The “abnormal” predicate is treated specially—if we can’t prove abnormal, we can
assume ~abnormal is true
• (Note that in normal logic, failure to prove a fact F doesn’t allow us to assume that
~F is true since F may be holding in some models and not in other models).
– Non-monotonic logic enterprise involves (1) providing clean semantics for this
type of reasoning and (2) making defeasible inference efficient
There was a big discussion on this
Fuzzy Logic vs. Prob. Prop. Logic
• Fuzzy Logic assumes that
the word is made of
statements that have
different grades of truth
– Recall the puppy example
• Fuzzy Logic is “Truth
Functional”—i.e., it
assumes that the truth
value of a sentence can be
established in terms of the
truth values only of the
constituent elements of
that sentence.
• PPL assumes that the
world is made up of
statements that are either
true or false
• PPL is truth functional for
“truth value in a given
world” but not truth
functional for entailment
status.
is true in all worlds (rows)
Where KB is true…so it is entailed
Proof by model checking
KB&~
False
False
False
False
False
False
False
False
So, to check if KB entails ,
negate , add it to the KB,
try to show that the resultant (propositional) theory
has no solutions (must have to use systematic methods)
Model-checking by Stochastic
Hill-climbing
• Start with a model (a random t/f
assignment to propositions)
• For I = 1 to max_flips do
– If model satisfies clauses then
return model
– Else clause := a randomly selected
clause from clauses that is false in
model
• With probability p whichever
symbol in clause maximizes the
number of satisfied clauses
/*greedy step*/
• With probability (1-p) flip the
value in model of a randomly
selected symbol from clause
/*random step*/
• Return Failure
Remarkably good in practice!!
Clauses
1. (p,s,u)
2. (~p, q)
3. (~q, r)
4. (q,~s,t)
5. (r,s)
6. (~s,t)
7. (~s,u)
Consider the assignment “all false”
-- clauses 1 (p,s,u) & 5 (r,s) are violated
--Pick one—say 5 (r,s)
[if we flip r, 1 (remains) violated
if we flip s, 4,6,7 are violated]
So, greedy thing is to flip r
we get all false, except r
otherwise, pick either randomly
Inference rules
• Sound (but incomplete)
• Complete (but unsound)
– “Python” logic
– Modus Ponens
• A=>B, A |= B
– Modus tollens
• A=>B,~B |= ~A
– Abduction (??)
• A => B,~A |= ~B
– Chaining
• A=>B,B=>C |= A=>C
How about SOUND & COMPLETE?
--Resolution (needs normal forms)
Need something that does case analysis
If WMDs are found, the war is justified
W=>J
If WMDs are not found, the war is still justified
~W=>J
Is the war justified anyway?
|= J?
Can Modus Ponens derive it?
Forward
apply resolution steps
until the fact f you want to
prove appears as a resolvent
Backward (Resolution Refutation)
Add negation of the fact f you
want to derive to KB
apply resolution steps
until you derive an empty clause
If WMDs are found, the war is justified
J V J =J
~W V J
If WMDs are not found, the war is still justified
WVJ
Is the war justified anyway?
Don’t need to use other
|= J?
equivalences if we use
resolution in refutation style
~J
~W
~WVJ
J
WVJ
Aka the product of sums form
From CSE/EEE 120
Aka the sum of products form
For any KB in horn form,
modus ponens is a sound
and complete inference
Prolog without variables
and without the cut operator
Is doing horn-clause theorem
proving
Conversion to CNF form
•
CNF clause= Disjunction of
literals
– Literal = a proposition or a
negated proposition
– Conversion:
• Remove implication
• Pull negation in
• Use demorgans laws to
distribute disjunction
over conjunction
• Separate conjunctions
into clauses
ANY propositional logic sentence
can be converted into CNF form
Try: ~(P&Q)=>~(R V W)
A  B  A  B
A
A B 
B
A
( A  B )  (A  B )  A  B 
B
AVC
( A  B)  C 
BVC
Steps in Resolution Refutation
•
Is there search in inference?
Yes!!
If the grass is wet, then it is either raining or the sprinkler Many
is on possible inferences can be done
Only few are actually relevant
• GW => R V SP
~GW V R V SP
--Idea: Set of Support
If it is raining, then Timmy is happy
At least one of the resolved
• R => TH
~R V TH
clauses is a goal clause, or
a descendant of a clause
If the sprinklers are on, Timmy is happy
derived from a goal clause
• SP => TH
~SP V TH
-- Used in the example here!!
Consider the following problem
–
–
–
– If timmy is happy, then he sings
• TH => SG
~TH V SG
SG V SP
– Timmy is not singing
• ~SG
TH V SP
~SG
– Prove that the grass is not wet
• |= ~GW?
SG
R V SP
GW
TH
SP
What if the new fact is inconsistent
with KB?
• Suppose we have a KB {P, P => ~F, Q=>J, R}; and our friend
comes running to tell you that M and F are true in the world.
• We notice that we can’t quite add F to KB since ~F is entailed.
• So what are our options?
– Ask our friend to take a hike
– Revise our theory so that F can be accommodated.
• To do this, we need to ensure that ~F is not entailed
• ..which means we have to stop the proof of ~F from going through.
– Since the proof for ~F is {P, P=>~F |= ~F}, we have to either change the
sentence P or the sentence P=>~F so that the proposition won’t go through
– Often there are many ways of doing this revision with little guidance as to
which revision is the best
» For example, we could change the second sentence to P&~M => ~F
» (But we could equally well have changed the sentence to P& L => ~F)
10/3
2.
Agenda: (as actually happened in the class)
1.
Project 2 code description (sudoku puzzle)
Long discussion on k-consistency and enforcement of kconsistency
3.
Discussion of DPLL algorithm
4.
Discussion of state of the art in SAT solvers
Discussion of Project 2 code
• Notice that constraints can be represented
either as pieces of code or declaratively as
legal/illegal partial assignments
– Sometimes the “pieces of code” may be more
space efficient
– (SAT solvers, unlike CSP solvers, expect
explicit constraints—represented as clauses)
Why are CSP problems hard?
• Because what seems like a locally good
decision (value assignment to a variable),
may wind up leading to global
inconsistency
• But what if we pre-process the CSP
problem such that the local choices are
more likely to be globally consistent?
– Two CSP problems CSP1 and CSP2 are
considered equivalent if both of them have the
same solutions. Related to the way artificial potential fields can
be set up for improving hill-climbing..
Pre-processing to enforce
Special terminology
consistency for binary CSPs
• An n-variable CSP problem is said to be kconsistent iff every consistent assignment for (k-1)
of the n variables can be extended to include any kth variable
• Strongly k-consistent if it is j-consistent for
all j from 1 to k
• Higher the level of (strong) consistency of problem,
the lesser the amount of backtracking required to
solve the problem
– A CSP with strong n-consistency can be solved
without any backtracking
• We can improve the level of consistency of a
problem by explicating implicit constraints
– Enforcing k-consistency is of O(nk) complexity
• Break-even seems to be around k=2 (“arc
consistency”) or 3 (“path consistency”)
2-consistency is
called “Arc”
consistency
(since you need only
considers pairs of
variables connected
by an edge in the
constraint graph)
3-consistency is
called “path”
consistency
How much consistency
should we enforce?
Total cost
incurred in search
Cost of enforcing the
consistency
Cost of searching
with the heuristic
h0
1
2
3
n
Degree of consistency
(measured in k-strong-consistency)
Overloading new semantics
on an old graphic 
Consistency and Hardness
• In the worst case, a CSP can be solved efficiently (i.e.,
without backtracking) only if it is strongly n-consistent
• However, in many problems, enforcing k-consistency
automatically renders the problem n-consistent as a sideeffect
– In such a case, we can clearly see that the problem is solvable in
O(nk) time (basically the time taken for pre-processing)
• The hardness of a CSP problem can be thought of in terms
of the “degree of consistency” that needs to be enforced on
that CSP before it can be solved efficiently (backtrackfree)
Enforcing Arc Consistency: An example
X:{1,2,3}
X<Y
Y:{1,2,3}
Y<Z
Z:{1,2,3}
X:{1}
X<Y
Y:{2}
Y<Z
Z:{3}
When we enforce arc-consistency on the top left CSP (shown as a
constraint graph), we get the CSP shown in the bottom left.
Notice how the domains have reduced. Here is an
explanation of what happens.
Suppose we start from Z. If Z=1, then Y can’t have any valid
values. So, we remove 1 from Z’s domain. If Z=2, or 3 then
Y can have a valid value (since Y can be 1 or 2).
Now we go to Y. If Y=1, then X can’t have any value. So, we
remove 1 from X’s domain. If Y=3, then Z can’t have any
value. So, we remove 3 from Y’s domain. So Y has just 2 in
its domain!
Now notice that Y’s domain has changed. So, we re-consider Z
(since anytime Y’s domain changes, it is possible that Z’s
domain gets affected). Sure enough, Z=2 no longer works
since Y can only be 2 and so it can’t take any value if Z=2.
So, we remove 2 also from Z’s domain. So, Z’s domain is
now just 3!
Now, we go to X. X can’t be 2 or 3 (since for either of those
values, Y will not have a value. So, X has domain 1!
Notice that in this case, arc-consistency SOLVES the problem,
since X,Y and Z have exactly 1 value each and that is the
only possible solution. This is not always the case (see next
example).
Consistency enforcement as inferring
implicit constraints
•
•
•
In general, enforcing consistency involves explicitly adding constraints that are implicit given the existing constraints
– E.g. In enforcing 3-consistency if we find that for a particular 2-label {xi=v1 & xj=v2} there is no possible
consistent value of xk, then we write this as an additional constraint
• {xi=v1}=> {xj != v2}
– [Domain reduction is just a special case] When enforcing 2-consistency (or arc-consistency), the new
constraints will be of the form xi!=v1 , and so these can be represented by just contracting the domain of xi by
pruning v1 from it
Unearthing implicit constraints can also be interpreted as “inferring” new constraints that hold (are “entailed”) given
the existing constraints
– In the context of boolean CSPs (I.e., propositional satisfiability problems), the analogy is even more striking
since unearthing new constraints means writing down new clauses (or “facts”) that are entailed given the
existing clauses
– This interpretation shows that consistency enforcement is just a form of “inference”/ “entailment computation”
process.
[Conditioning & Inference—The Yin and Yang] There is a general idea that in solving a search
problem, you can interleave two different processes
–
• “inference” trying to either infer the solution itself or saying no solution exists
• “conditioning or enumeration”which attempts to systematically go through potential solutions looking for
a real solution.
Good search algorithms interleave both inference and conditioning
• E.g. the CSP algorithm we discussed in the class uses backtracking search (enumeration), and forward
checking (inference).
More on arc-consistency
Arc-consistency doesn’t always imply that the CSP has a solution or that
there is no search required. In the previous example, if each variable had
domains 1,2,3,4, then at the end of enforcing arc-consistency, each variable
will still have 2 values in its domain—thus necessitating search.
Here is another example which shows that the search may find that there is
no solution for the CSP, even though it is arc-consistent.
Here is a binary CSP that
Is arc-consistent but has no
Solution.
Approximating K-Consistency
• K-consistency enforcement takes O(nk) effort. Since we are doing this
only to reduce the overall search effort (rather than to get a separate
badge for consistency), we can cut corners
• [Directional K-consistency] Given a fixed permutation (order) over the
n variables, assignment to first k-1 variables can be extended to the kth variable
– Clearly cheaper than K-consistency
– If we know that the search will consider variables in a fixed order, then
enforcing directional consistency w.r.t. that order is better.
• [Partial K-consistency enforcement] Run the K-consistency
enforcement algorithm partially (i.e., stop before reaching fixed-point)
– Put a time-limit on the consistency computation
• Recall how we could cut corners in computing Pattern Database heuristics by
spending only a limited time on the PDB and substituting other cheaper
heuristics in their place
– Only do one pass of the consistency enforcement
• This is what “forward checking” does..
> : “stronger than”
Arc-Consistency > directed arc-consistency > Forward Checking
After directional arc-consistency
Assuming the variable order
X<Y<Z
X:{1,2,3}
DAC:For each variable u, we only consider
The effects on the variables that
Come after u in the ordering
X:{1,2}
X<Y
X<Y
Y:{2}
Y:{1,2,3}
Y<Z
Y<Z
AC is the strongest
It propagates Changes in
all directions Until we
reach a fixed point
(no further changes)
Z:{1,2,3}
Z:{1,2,3}
After forward checking assuming
X<Y<Z, and X has been set to value 1
After arc-consistency
X:{1}
X<Y
X:{1}
Y:{2}
Y<Z
Z:{3}
ADDED AFTER CLASS
IMPORTANT
FC: We start with the current
Assignment for some of the
Variables, and only consider their
Effects on the future variables.
(only a single level
Propagation is done. After we find
that a value of Y is pruned, we don’t try
To see if that changes domain of Z)
X<Y
Y:{2,3}
Y<Z
Z:{1,2,3}
Davis-Putnam-Logeman-Loveland
Procedure
detect failure
DPLL Example
Pick p;
set p=true
unit propagation
(p,s,u) satisfied (remove)
p;(~p,q)  q derived; set q=T
(~p,q) satisfied (remove)
(q,~s,t) satisfied (remove)
q;(~q,r)r derived; set r=T
(~q,r) satisfied (remove)
s was not Pure
in all clauses (only
(r,s) satisfied (remove)
The remaining ones)
pure literal elimination
in all the remaining clauses, s occurs negative
set ~s=True (i.e. s=False)
At this point all clauses satisfied. Return
p=T,q=T;r=T;s=False
Clauses
(p,s,u)
(~p, q)
(~q, r)
(q,~s,t)
(r,s)
(~s,t)
(~s,u)
Model-checking by Stochastic
Hill-climbing
• Start with a model (a random t/f
assignment to propositions)
• For I = 1 to max_flips do
– If model satisfies clauses then
return model
– Else clause := a randomly selected
clause from clauses that is false in
model
• With probability p whichever
symbol in clause maximizes the
number of satisfied clauses
/*greedy step*/
• With probability (1-p) flip the
value in model of a randomly
selected symbol from clause
/*random step*/
• Return Failure
Clauses
1. (p,s,u)
2. (~p, q)
3. (~q, r)
4. (q,~s,t)
5. (r,s)
6. (~s,t)
7. (~s,u)
Consider the assignment “all false”
-- clauses 1 (p,s,u) & 5 (r,s) are violated
--Pick one—say 5 (r,s)
[if we flip r, 1 (remains) violated
if we flip s, 4,6,7 are violated]
So, greedy thing is to flip r
we get all false, except r
otherwise, pick either randomly
Remarkably good in practice!!
but not complete and so can’t be used to do entailment
Lots of work in SAT solvers
• DPLL was the first (late 60’s)
• Circa 1994 came GSAT (hill climbing search for SAT)
• Circa 1997 came SATZ
– Branches on the variable that causes the most amount of unit
propagation..
• Circa 1998-99 came RelSAT
– Does dependency directed backtracking..
• ~2000 came CHAFF
• Current champion: Siege
• Current best can be found at
– http://www.satlive.org/
– A primer on solvers circa 2005 is at
http://www.cs.sfu.ca/~mitchell/papers/colLogCS85.pdf