CSCE 420 Lecture 14

« previous | Thursday, February 28, 2013 | next »

End Exam 1 content

Back-Chaining

def backchain kb, query
  stack = [query]
  bc kb, stack
end

def bc kb, stack
  return true if stack.empty?
  goal = stack.pop
  return bc(kb, stack) if kb.include? goal
  # rules of form conclusion => [[a1,...,an], [b1,...,bm], ...]
  kb.rules[goal].each do |antecedents|
    stack.push *antecedents
    return true if bc kb,stack
  end
  return false
end

Example

Knowledge Base

{
  1.  can_ride_bike_to_work -> can_get_to_work
  2.  can_drive_to_work -> can_get_to_work
  3.  can_walk_to_work -> can_get_to_work
  4.  have_bike && sunny -> can_ride_bike_to_work
  5.  own_car -> can_drive_to_work
  6.  rent_car -> can_drive_to_work
  7.  have_money && taxi_available -> can_drive_to_work
  8.  rainy
  9.  have_bike
  10. have_money
  11. rent_car
  12. taxi_available
}
query = can_get_to_work

Algorithm Trace

{can_get_to_work}  init
  {can_ride_bike_to_work}  pop top; match with consequence of rule 1; push antecedents
    {have_bike, sunny}  rule 4
      {sunny}  have_bike is a fact
        backtrack: sunny is not a fact and cannot be proved
  {can_drive_to_work}  make new choice; rule 2
    {own_car}  rule 5
      backtrack: don't own a car
    {rent_car}  rule 6
      {} rent_car is a fact
        return true

DFS of search-tree

• sector between branches = AND
• lack of sector (regular-looking tree) = OR

Resolution

Essentially proof by contradiction

1. negate query, add to KB
2. do resolution, try to derive "empty clause" (with 0 literals), which is False
3. if KB entails q then KB && !q is unsatisfiable

Resolution rule:

${\frac {(\alpha \vee \beta )\wedge (\neg \alpha \vee \gamma )}{\beta \vee \gamma }}$

Convert to conjunctive normal form (CNF): $(A\vee B\vee \neg C)\wedge (A\vee \neg D)$

(c.f. disjunctive normal form (DNF): $(X\wedge Y)\vee (x\wedge Z)$)

1. eliminate ↔ and →
2. push negations inward
3. rearrange to CNF using distributivity

Example Conversion

${\begin{aligned}A\iff (B\vee C)&\equiv (A\implies (B\vee C))\wedge ((B\vee C)\implies A\\&\equiv (\neg A\vee B\vee C)\wedge \neg (B\vee C)\vee A\\&\equiv (\neg A\vee B\vee C)\wedge (\neg B\wedge \neg C)\vee A\\&\equiv (\neg A\vee B\vee C)\wedge (\neg B\vee A)\wedge (\neg C\vee A)\end{aligned}}$

Algorithm

function PL-Resolution(KB, α) returns true or false
  clauses := set of clauses in CNF representation of KB && ¬α
  new := {}
  loop do
    for each c[i], c[j] in clauses do
      resolvents := PL-Resolve(c[i], c[j])
      if resolvents contains the empty clause then return true
      new := new union resolvents
    end for
    if new subset of clauses then return false
    clauses := clauses union new
  end loop
end function

KB = { A <-> (B || C), !A }
q = !B
KB.entails?(q = !B)

Convert to CNF:
KB = {
  1. !A || B || C
  2. !B || A
  3. !C || A
  4. !A
}

Add negation of query
5.  B
6.  B || !B || C == T (1,2)
7.  A || !A || C == T (1,2)
8.  A || !A || B      (1,3)
9.  A                 (2,5)
10. !B                (4,2)
11. empty clause      (4,9)

This works because KB ∧ ¬q is unsatisfiable.

• $\mathrm {KB} \models q$ is defined as:
  • all models (truth assignments) that satisfy KB also satisfy $q$.
  • In space of all possible models, $M(\mathrm {KB} )\subset M(q)$
• Our construction $\mathrm {KB} \wedge \neg q$ is represented as $M(\mathrm {KB} \cap M(\neg q)$
• Since $M(q)\supseteq M(\mathrm {KB}$, the intersection is empty and therefore not satisfiable

DPLL

• returns satisfying model (truth assignment) or false
• requires conversion to CNF
• start with empty truth assignment
• choose variable and bind to truth value
• if any sentences are violated (i.e. sentence is false), backtrack
• else recurse and choose another variable

function DPLL-Satisfiable?(sentence) returns true or false
  clauses := set of clauses in CNF representation of sentence
  symbols := list of propositional symbols (variables) in sentence
  return DPLL(clauses, symbols, [])
end function

function DPLL(clauses, symbols, model) returns true or false
  if every clause in clauses is true in model then return true
  if some clause in clauses is false in model then return false
  P.value := Find-Pure-Symbol(symbols, clauses, model)
  if P is non-null then return DPLL(clauses, symbols - P, [P = value|model])
  P.value := Find-Unit-Clause(clauses, model)
  if P is non-null then return DPLL(clauses, symbols - P, [P = value|model])
  P := First(symbols); rest := Rest(symbols)
  return DPLL(clauses, rest, [P = true|model]) or DPLL(clauses, rest, [P = false|model])
end function

function Find-Pure-Symbol(symbols, clauses, model) returns symbol assignment
  for each symbol in symbols
    if all are non-negated then return true assignment for symbol
    if all are negated then return false assignment for symbol
  end for
end function

Complexity

determining entailment is equivalent to satisfiability

The easy answer is model enumeration: calculate truth of all possible truth assignments $O(2^{n})$.

Cook's Theorem: Every NPC problem can be reduced to 3-SAT

Exam

• No Mult. Choice
• Definitions
• Tracing Algorithms, conversion, etc.
• Advantage of one algorithm over another