Notes on Chapter 7: Logical Agents and Propositional Satisfiability¶

Logical Agents¶

logical agents use logic to make decisions and act in the world

the two most common kinds of logics are:

propositional logic
first-order logic (e.g. logic with quantifiers like “for all” and “there exists”)

there are (many!) other sorts of logic, but those are beyond the scope of this course

when thinking about logical agents, we imagine that the agent has a knowledge base (KB for short) that contains logical sentences that describe the state of the world

you could think of a KB as a database designed for storing and retrieving logical sentences

there are two main KB operations: TELL and ASK

TELL puts a new fact into the KB
ASK queries the KB about what is known; this usually involves inference, where the KB can determine that facts are true (or likely to be true) even though they have not been explicitly told them
- e.g. if a KB knows that a car is traveling at 50kmph, then it ought to be able to infer from that fact that the car is not being washed

coming up with efficient ways to represent KBs and perform these two operations is one of the major problems in AI

Propositional Logic¶

to be concrete, we will focus on propositional logic

you should already know about this from programming, and discrete math

but lets quickly review it …

here is an example propositional logic sentence: P -> ~(Q & R)

-> is the logical connective implication
~ is the logical connective negation
& is the logical connective and
v is the logical connective or (not shown in this expression)
<-> is the logical connective equivalence (not shown in this expression)
P, Q, and R are variables
we also will sometimes have special symbols True and False, indicating the constant values of true and false

a grammar for the syntax of propositional logic is given in Figure 7.7 (p. 244) of the text

the semantics of propositional logic is usually defined in English, or with truth tables, e.g.

S ^ T is true when S is true and T is true, and false otherwise

S T  S ^ T
----------
0 0    0
0 1    0
1 0    0
1 1    0

the special symbol True is always true, and the special symbol False is always false

we define an atomic sentence to be either the special symbols True or False, or a variable (e.g. P, Q, R, …)

a literal is either an atomic sentence (a positive literal), or the negation of an atomic sentence (a negative literal)

e.g. True, False, ~True, P, ~P, A, B, ~M are all literals

e.g. True, False, P, A, and B are all positive literals

e.g. ~True, ~P, ~M are all negative literals

given a propositional logic sentence like P -> ~(Q & R), we are usually interested in whether it is true or false

if we are given the truth values of P, Q, and R, then we can use the definitions of the logical connectives to calculate the expression of the sentence

e.g. suppose P=true, Q=true, and R=false; then P -> ~(Q & R) is false

a related question we might ask is if there is any assignment of truth-values to P, Q, and R that make it true

The SAT Problem¶

this is known as the SAT, or satisfiability problem, and it turns out to have a lot of practical applications

many problems can be cast as SAT problems, including CSPs (!)
very efficient SAT solvers have been created and refined over the years

e.g. does P -> ~(Q & R) have a satisfying assignment? yes: if you know the definition of ->, then you know that “false -> anything” is true, and so setting P=false, and Q and R to any other values, is a satisfying assignment

when discussing the SAT problem, we will often talk about models

practically speaking, for propositional logic, a model of a sentence is a particular assignment of values to variables (of that sentence) that make it true

e.g. P=false, Q=true, and R=false is a model of P -> ~(Q & R), because the sentence evaluates to true with those assignments

e.g. P=true, Q=true, and R=false is also a model of P -> ~(Q & R)

e.g. P=true, Q=true, and R=true is not a model of P -> ~(Q & R)

sometimes we use the notation M(s) to denote all models of a sentence s

if M(s) contains all possible assignments of values to variables, then s is a tautology
if M(s) is empty, then s is a contradiction

e.g. here is the truth table for P -> ~(Q & R):

P Q R   P -> ~(Q & R)
---------------------
0 0     1
0 1     1
1 0     1
1 1     1
0 0     1
0 1     1
1 0     1
1 1     0

this shows that P=true, Q=true, and R=true is the only assignment of values to variables that does not model P -> ~(Q & R)

so M(P -> ~(Q & R)) = { (0,0,0), (0,0,1), (0,1,0), (0,1,1), (1,0,0), (1,0,1), (1,1,0) }

the SAT problem thus asks for a given sentence s if M(s) is non-empty, and what is one element in it

Modelling with Propositional Logic¶

to see how we can use propositional logic and SAT to solve problems, lets try modelling the n-queens problem in propositional logic

recall that the N-queens problem asks you to place N chess queens on an NxN so that no two queens are on the same row, column, or diagonal

The N=2 Queens Problem as a SAT Problem¶

we’ll start with n=2; this obviously has no solutions, but it’s a good warm-up

we’ll represent the n=2 problem with 4 logical variables, one for each square of the board:

A B
C D

now we add constraints on these variables

we will use x!=y to mean sentences x and y have different values, i.e.:

x y   x!=y
----------
0 0    0
0 1    1
1 0    1
1 1    0

!= is known as exclusive-or, but for this problem it’s convenient to think of it as the “not equal” operator

there are three groups of constraints: row constraints, column constraints, and diagonal constraints

row constraints: A!=B, C!=D

column constraints: A!=C, B!=D

diagonal constraints: A!=D, B!=C

we can join all these constraints together with & to make a single propositional logic expression:

A!=B & C!=D & A!=C & B!=D & A!=D & B!=C

if this expression is satisfiable, then that means there is a way to place 2 queens on the board that don’t attack each other

but we know this is impossible, so we know this expression is not satisfiable

we used != here for convenience, but in practice SAT solvers might not directly support the != (exclusive-or) connective

so we can re-write the constraints using just &, v (or), and ~ (not)

row constraints:

(
     ( A & ~B)
   v (~A &  B)
)

(
     ( C & ~D)
   v (~C &  D)
)

column constraints:

(
     ( A & ~C)
   v (~A &  C)
)

(
     ( B & ~D)
   v (~B &  D)
)

diagonal constraints:

(
     ( A & ~D)
   v (~A &  D)
)

(
     ( B & ~C)
   v (~B &  C)
)

and-ing all of these together gives one big sentence:

   (
        ( A & ~B)
      v (~A &  B)
   )
&
   (
        ( C & ~D)
      v (~C &  D)
   )
&
   (
        ( A & ~C)
      v (~A &  C)
   )
&
   (
        ( B & ~D)
      v (~B &  D)
   )
&
   (
        ( A & ~D)
      v (~A &  D)
   )
&
   (
        ( B & ~C)
      v (~B &  C)
   )

some SAT solvers require that the sentence being solved be in conjunction normal form (CNF)

a sentence is in CNF if its consists of a series of literals or-ed together all join by &, e.g. this sentence is in CNF:

  (P v ~Q v R)    // conjunctive normal form (CNF)
& (~P v ~Q v R)
& (P v Q v ~R)

all propositional logic sentences can be converted to CNF (see p.253-4 of the textbook)

the following constraint on B and C is not in CNF:

(
     ( B & ~C)
   v (~B &  C)
)

to convert it CNF, we can apply the distributivity rule (see p.249) twice to get this logically equivalent expression:

  ( B v  C)
& (~B v ~C)

you can use a truth-table to verify that these are, in fact, logically equivalent

so the entire expression in CNF would be this:

  ( A v  B)
& (~A v ~B)
& ( C v  D)
& (~C v ~D)
& ( A v  C)
& (~A v ~C)
& ( B v  D)
& (~B v ~D)
& ( A v  D)
& (~A v ~D)
& ( B v  C)
& (~B v ~C)

if we agree to put one disjunct per line, then we can get rid of the & operators and brackets:

 A v  B
~A v ~B
 C v  D
~C v ~D
 A v  C
~A v ~C
 B v  D
~B v ~D
 A v  D
~A v ~D
 B v  C
~B v ~C

there is also no need for the v either, so this could be further simplified to:

 A  B
~A ~B
 C  D
~C ~D
 A  C
~A ~C
 B  D
~B ~D
 A  D
~A ~D
 B  C
~B ~C

for SAT solvers, one more major simplification is made: for variables, numbers are used instead of letters, and negation is represented by a -

so if we let A=1, B=2, C=3, and D=4, our expression becomes:

we’re almost done! the standard SAT solver input requires a few more things:

the first line should indicate the number of variables and number of clauses (a clause is a disjunction of literals), in this format:
```
p cnf <num_vbles> <num_clauses>
```
every clause must end with a 0
a line that beings with a c is a comment that is ignored by the solver

so here is the final input:

 c N=2 queens problem
 p cnf 4 12
 1  2 0
-1 -2 0
 3  4 0
-3 -4 0
 1  3 0
-1 -3 0
 2  4 0
-2 -4 0
 1  4 0
-1 -4 0
 2  3 0
-2 -3 0

to solve this with minisat, we put the above input into a file named queens2.txt, and then run this command:

$ minisat queens2.txt out
... lots of info about the solution ...

UNSATISFIABLE

$ cat out
UNSAT

which variables are true/false are written to the output file (named out here); if, as in this example, there are no satisfying assignments, then UNSAT is written

The N=3 Queens Problem as a SAT Problem¶

now lets try the N=3 queens problem; we will use these 9 variables:

A B C
D E F
G H I

through a bit of trial and error, it’s not hard to see that this cannot be solved

lets list the constraints

consider the first row: A B C

exactly one of these must be true, and the others false; we can write that constraint like this:

   ( A & ~B & ~C)   // first row
v  (~A &  B & ~C)
v  (~A & ~B &  C)

but this is not in CNF; so lets think about how to make this constraint CNF

exactly one A, B, or C must be true, so this constraint holds:

A v B v C

suppose that A is true; that means B is false and C is false; symbolically, this means A->~B and A->~C, and those can be re-written as the logically equivalent sentences ~A v ~B and ~A v ~C

we can do the same thing for B and C, and so we get these constraints in CNF:

A v B v C
~A v ~B
~A v ~C
~B v ~A   // repeat!
~B v ~C
~C v ~A   // repeat!
~C v ~B   // repeat!

removing the repeated clauses gives:

A v B v C  // first row
~A v ~B
~A v ~C
~B v ~C

intuitively, this says that at least one of A, B, or C is true, and also if you pick any pair of variables, at least one of the variables in the pair will be false

this amounts to saying exactly one of A, B, or C is true

we do the same thing for the next two rows:

D v E v F  // second row
~D v ~E
~D v ~F
~E v ~F

G v H v I  // third row
~G v ~H
~G v ~I
~H v ~I

the column constraints have the same format:

A v D v G  // column 1
~A v ~D
~A v ~G
~D v ~G

B v E v H  // column 2
~B v ~E
~B v ~H
~E v ~H

C v F v I  // column 3
~C v ~F
~C v ~I
~F v ~I

for the diagonal constraints, there are two main diagonals (AEI and CEG), and 4 short diagonals (BF, FH, HD, DB)

the constraint on the diagonals is different that the constraint on the rows and columns: at most one queen can appear on any diagonal (i.e. it’s okay for a diagonal to have no queens, something that can’t happen with rows and columns)

so for the diagonal constraints, we will not have the “or” of all the variables involved, just the following 2-variable constraints:

~A v ~E  // AEI
~A v ~I
~E v ~I

~C v ~E  // CEG
~C v ~G
~E v ~G

~B v ~F  // BF

~F v ~H  // FH

~H v ~D  // HD

~D v ~B  // DB

now, as we did for the N=2 case, we join together all these constraints using & to get one (big!) CNF sentence that is true just when 3 non-attacking queens on a 3x3 board

since we know that puzzle is not solvable, we know that this sentence has no satisfying assignment

here is the input formatted for minisat:

c 3-queens problem
p cnf 9 34
1 2 3 0
-1 -2 0
-1 -3 0
-2 -3 0
4 5 6 0
-4 -5 0
-4 -6 0
-5 -6 0
7 8 9 0
-7 -8 0
-7 -9 0
-8 -9 0
1 4 7 0
-1 -4 0
-1 -7 0
-4 -7 0
2 5 8 0
-2 -5 0
-2 -8 0
-5 -8 0
3 6 9 0
-3 -6 0
-3 -9 0
-6 -9 0
-1 -5 0
-1 -9 0
-5 -9 0
-3 -5 0
-3 -7 0
-5 -7 0
-2 -6 0
-6 -8 0
-8 -4 0
-4 -2 0

The N=4 Queens Problem as a SAT Problem¶

for the N=4 queens problem, the constraints are similar to the ones for N=3, but there are more of them and they are a little bigger

there are 16 variables:

A B C D
E F G H
I J K L
M N O P

to help with this, we’ll use the notation exactly_one(W,X,Y,Z) to indicate a CNF expression that allows exactly one of W, X, Y, or Z to be true

and at_most_one(W,X,Y,Z) to indicate a CNF expression that allows at most one of W, X, Y, or Z to be true

row constraints:

exactly_one(A,B,C,D)

exactly_one(E,F,G,H)

exactly_one(I,J,K,L)

exactly_one(M,N,O,P)

column constraints:

exactly_one(A,E,I,M)

exactly_one(B,F,J,N)

exactly_one(C,G,K,O)

exactly_one(D,H,L,P)

for the diagonal constraints, notice that the diagonals go in two different directions, range in size from 2 to 4, and at most one queen can appear on any diagonal:

at_most_one(C,H)

at_most_one(B,G,L)

at_most_one(A,F,K,P)

at_most_one(E,J,O)

at_most_one(I,N)

here is a CNF version of the constraints that can be input into minisat:

c 4-queens problem (sat)
p cnf 16 84
-1 -2 0
-1 -3 0
-1 -4 0
-2 -3 0
-2 -4 0
-3 -4 0
1 2 3 4 0
-5 -6 0
-5 -7 0
-5 -8 0
-6 -7 0
-6 -8 0
-7 -8 0
5 6 7 8 0
-9 -10 0
-9 -11 0
-9 -12 0
-10 -11 0
-10 -12 0
-11 -12 0
9 10 11 12 0
-13 -14 0
-13 -15 0
-13 -16 0
-14 -15 0
-14 -16 0
-15 -16 0
13 14 15 16 0
-1 -5 0
-1 -9 0
-1 -13 0
-5 -9 0
-5 -13 0
-9 -13 0
1 5 9 13 0
-2 -6 0
-2 -10 0
-2 -14 0
-6 -10 0
-6 -14 0
-10 -14 0
2 6 10 14 0
-3 -7 0
-3 -11 0
-3 -15 0
-7 -11 0
-7 -15 0
-11 -15 0
3 7 11 15 0
-4 -8 0
-4 -12 0
-4 -16 0
-8 -12 0
-8 -16 0
-12 -16 0
4 8 12 16 0
-3 -8 0
-2 -7 0
-2 -12 0
-7 -12 0
-1 -6 0
-1 -11 0
-1 -16 0
-6 -11 0
-6 -16 0
-11 -16 0
-5 -10 0
-5 -15 0
-10 -15 0
-9 -14 0
-2 -5 0
-3 -6 0
-3 -9 0
-6 -9 0
-4 -7 0
-4 -10 0
-4 -13 0
-7 -10 0
-7 -13 0
-10 -13 0
-8 -11 0
-8 -14 0
-11 -14 0
-12 -15 0

the 4-queens problem has solutions, and so this sentence is satisfiable, e.g. minisat returned this model:

-1 -2 3 -4 5 -6 -7 -8 -9 -10 -11 12 -13 14 -15 -16

a negative number means the variable is assigned false, and a positive number mean its assigned true

this model corresponds to this placement of queens:

. . Q .
Q . . .
. . . Q
. Q . .

N-queens in General¶

the previous examples of the N queens problem shows the general pattern you can follow to create a CNF expression that, when satisfied, is a solution to the N-queens problem

SAT Solvers¶

SAT solvers are a kinds of CSP solver tuned specifically for solving SAT problems

they are efficient enough to actually be useful in some practical applications, and can sometimes efficiently solve problems with 1000s of variables and clauses

there are two main categories of SAT solvers:

backtracking solvers (like minisat)
- can be used to prove that a sentence is unsatisfiable
local search solvers (like Walksat)
- can’t be used to prove (with 100% certainty, at least) that a sentence is unsatisfiable

modern backtracking SAT solvers combine efficient data structures and SAT-specific heuristics to efficiently solve many large SAT problems

they are a practical choice for solve CSP-like problems, or problems that require backtracking
the tricky part is usually coming up with an efficient CNF-encoding of all the constraints, and as with the N-queen problem this may involve writing a program to do this

SAT: DPLL Algorithm¶

the DPLL algorithm (Davis, Putnam, Logemann, and Loveland); from early 1960s

the input to DPLL is a CNF (conjunctive normal form) sentence

recall that a CNF sentence is a series of clauses and-ed together
a clause is one, or more, literals or-ed together
a literal is a variable, or the negation of a variable
any propositional sentence can be converted to CNF

it is essentially a depth-first backtracking algorithm, with a few improvements:

early termination

sometimes you don’t need to assign all variables to determine if a sentence is satisfied, e.g. (A | B) & (A | C) is true if A is true, no matter the values of B and C
- so once A is assigned true in the backtracking search, we can see that the sentence is satisfied, and can stop immediately and return SAT
similarly, if any clause is false, then the entire CNF sentence must be false (because it is multiple clauses and-ed together), and backtracking can occur; this might happen after only a few variables have been assigned, e.g. (A | !B) & (C | !D) must be false if A=false and B=true — no need to check C and D
pure symbol heuristic

a “symbol” is pure if it occurs with the same “sign” in all clauses, i.e. it always occurs negated, or always occurs un-negated

e.g. (A | !B) & (!B | !C) & (C | A)
- A is pure because it appears with the same sign in all clauses
- B is pure because it appears with the same sign in all clauses
- C is not pure because it appears with different signs, C in clauses, !C in another
all pure symbols can be assigned a value that makes them true, since doing so can never make a clause false

e.g. (A | !B) & (!B | !C) & (C | A)
- A is pure, so setting A=True will never make the clauses it appears in false
- B is also pure, so setting B=False will never make the clauses it appears in false
- A=True, B=True, C=True (or C=False) is a satisfying assignment
note that a symbol could become pure based on partial assignments, i.e. assigning values to some variables may make some clauses true, and true clauses can be ignored when determining a variable purity
unit clause heuristic

a unit clause is a clause with one literal, i.e. a clause that is just a variable, or the negation of a variable

in the context of DPLL, a unit clause can also occur when all literals but one in a clause have a known value, e.g. if A=false and B=true in the current search, then (A | !B | !C) becomes a unit clause

since a unit clause has only one literal and that must evaluate to true, we can immediately assign it the value that makes it true

after assigning a unit clause the required value, other clauses may simplify to unit clauses, sometimes resulting in a cascade of assignments that is similar to forward checking

e.g. consider the sentence (A | !B) & (A | B | !C) & (B | C)
- for the sake of this example, suppose we set A=False
- the first clause is now a unit clause, and that means !B must be true, so B=False
- the third clause is now a unit clause, so !C=True, meaning C=False
- since B and C are both False, the clause (B | C) cannot be satisfied, so the entire expression is unsatisfiable
e.g. consider the sentence (A | !B) & (!A | B | C) & (B | !C)
- suppose we set A=False
- this forces !B=True, i.e. B=False
- since !A=True, (!A | B | C) is true
- since B=False, (B | !C) is a unit clause, so !C=True, i.e. C=False
- therefore A=False, B=False, C=False is a satisfying assignment

the above heuristics have been part of the DPLL algorithm since its invention

modern SAT solvers based on DPLL typically implement many other clever tricks and heuristics that have a significant impact on performance, such as:

component analysis: SAT solvers may be able to recognize disjoint subsets of clauses and solve them independently
Variable and value ordering: as with CSPs, heuristics can for choosing the next variable to assign and the value to assign it can be quite effective; e.g. the degree heuristic says you should choose the next variable to assign to be the one that appears in the most clauses
Intelligent backtracking: SAT solvers can use clause learning to keep track of conflict, i.e. they add new clauses to the sentence to avoid going down parts of the search tree that are known to be unfruitful
- experiments show that this is probably the single feature with the greatest performance impact in SAT solving
Random restarts: if it seems progress is not being made, a solver can re-start the search, making difference random choices and preserving any learned conflicts
Clever indexing: SAT solvers can use efficient customized data structures to quickly find things like all clauses in which a variable appears as a positive literal, or to determine in which clauses unit propagation will occur (2-watched literals)

overall, these sorts of additions to the basic DPLL have resulted in extremely efficient SAT solvers that are good enough to be able to solve some practical problems involving tens of thousands of variable and clauses

both the theory of SAT and the practice of implementing efficient SAT solvers is still well-studied area of computer science, with dozens of research papers being published per year

SAT: Walksat¶

just as some CSPs can be efficiently solved by local search (such as min-conflicts), the local search algorithm named Walksat can efficiently find satisfying assignments for some sentences even more quickly than DPLL solvers

keep in mind that, like min-conflicts for CSPs, Walksat is a randomized algorithm and so cannot prove that a sentence is unsatisfiable
- if Walksat can’t satisfy a sentence, then you might take that as good evidence that the sentence can’t be satisfied — but it’s not a proof that no satisfying assignment exists!

in Walksat, all variables in the sentence have a value (you could start with a random initial assignment)

then Walksat repeatedly does the following until the sentence is satisfied, or some max number of flips is reached:

it chooses an unsatisfied clause at random
it then “flips” the value of one of the variables in the clause by randomly choosing (with some probability \(p\)) one of the following:
- pick a variable to flip at random
- or, flip the variable that maximizes the number of satisfied clauses overall

this is a much simpler algorithm than DPLL!

it is perhaps surprising that it can work so well

it has undergone extensive testing, and it can efficiently satisfy many large sentences

but keep in mind it can never prove unsatisfiability!

Propositional Theorem Proving¶

a different approach to using logic to solve problems is to use logical rules of inference to generate logical implications

in some cases, this can be less work than model-checking (i.e. generating a truth table) or even SAT solving

plus, logical rules of inference are a the level of logical reasoning that humans consciously strive to do

theorem-proving is interested in entailment, e.g. given a logical sentence A and a logical sentence B, we can ask if A entails B

the idea is that the A sentence is what the agent knows, and the B sentence is something that the agent can infer from what it knows

sentence A might be very big, i.e. the entire “brain” of an agent encoded in logic

an important basic result in logic is the deduction theorem, which says:

A entails B if, and only if, A => B is a tautology (i.e. valid for all assignments of values to its variables)

so we can answer the question “Does A entail B?” by showing the A => B is a tautology

recall that a sentence is unsatisfiable if no assignment of values to its variables makes it true

so A => B is a tautology, then !(A=>B) is unsatisfiable, and !(A=>B) == !(!(A & !B)) == A & !B

so we can re-write the deduction theorem like this:

A entails B if, and only if, A & !B is unsatisfiable

so you could use a SAT solver to figure out entailment!

Rules of Inference¶

recall that there are various rules of inference that can be used to create proofs, i.e. chains of correct inferences

so if you start with a true fact and correctly applying only valid inferences, you will end up with a valid inference

modus ponens is this rule:

A, A => B
---------   modus ponens
    B

this rule says that if you are given some sentence A, and some sentence B, you may infer B

and-elimination is this pair of rules:

A & B
-----       and-elimination
  A

A & B
-----
  B

these rules encode the (obvious!) fact that if the sentence A&B is true, then A is true, and also B is true

logical equivalences can also be stated as inference rules, e.g.:

A <==> B
---------------
(A=>B) & (B=>A)

there are many inference rules, and choosing a reasonable set of rules for a theorem-prover turns out to be important

we can think of the application of one rule of inference as an action performed to the state of the world, i.e. the rule of inference adds more facts to the knowledge base
if there are multiple inference rules to choose from, then we need knowledge (i.e. heuristics) to help decide which rule to use
- or we could rely on backtracking, i.e. just pick a rule at random, apply it, and keep going until it “seems” like a proof is not being reached
plus, how do we know that the rules of inference we are using are complete, i.e. how do we know they will be able to find a proof of entailment (assuming such a proof exists)
- e.g. suppose the two and-elimination rules were our only rules of inference; is this enough to prove any entailment in propositional logic?
  - no!
  - for example, (P | P) -> P is clearly true, but and-elimination simply doesn’t match this match expression

Proof by Resolution¶

it turns that only inference rule is needed to be able to prove any logical entailment (that can be proved): the resolution rule

in a 2-variable form, the resolution inference rule is this:

A | B   !B
----------    resolution
    A

in English, this says that if A or B is true, and B is not true, then A must be true

we can generalize this as follows:

A_1 | A_2 | ... | A_i | ... | A_n    !A_i
-----------------------------------------     resolution generalized
A_1 | A_2 | ... | A_i-1 | A_i+1... | A_n

we’ve written A_i and !A_i, but those could be swapped: the key is that they are complementary literals

notice that there CNF-style clause about the inference line, and a CNF-style clause below it as well

recall that a CNF clause consists of literals (a variable, or the negation of a variable), or-ed together

so resolution can be stated conveniently in terms of clauses, e.g.:

Clause_1   L_i
--------------
Clause_2

here, L_i is a literal that has the opposite sign of a literal in Clause_1

Clause_2 is the same as Clause_1, but with the literal that is the opposite of L_i removed

e.g.:

(A | !B | !C)  !A
-----------------
    !B | !C

(A | !B | !C)  C
-----------------
    A | !B

full resolution generalizes this even further to two clauses:

Clause_1  Clause_2
------------------   full resolution
     Clause_3

here, we assume that some literal L appears in Clause_1, and the opposite of literal L appears in Clause_2

Clause_3 contains all the literals (or-ed together) from both Clause_1 and Clause_2, except for L and its opposite — those are not in Clause_3

e.g.:

(A | !B | !C)  (!A | !C | D)
----------------------------
        !B | !C | D

what is surprising is that full resolution is complete: it can be used to proved any entailment (assuming the entailment can be proven)

to do this, resolution requires that all sentences be converted to CNF

this can always be done … see the textbook for a sketch of the basic idea
the same requirement for most SAT solvers!

next, recall that if A entails B, then A & !B is unsatisfiable

resolutions theorem proving proves that A entails B by proving that A & !B is unsatisfiable

A & !B is converted to CNF
clauses with complementary literals are chosen and resolved (i.e. the resolution rule is applied to them to remove the literal and its complement) and added as a new clause in the knowledge base
this continues until one of two things happens:
1. no new clause can be added, which means that A does not entail B
2. two clauses resolve to yield the empty clause, which means that A entails B
  - the empty clause means there is a contradiction, i.e. if P and !P are clauses then we can apply resolution to them to get the “empty clause”
  - clearly, if both P and !P are in the same knowledge base, then it is inconsistent since P and !P is false for all value of P

example. KB = {P->Q, Q->R}

does KB entail P->R?
it’s not hard to see that it does, but lets use resolution to prove this
to prove KB entails P->R, we will prove that KB & !(P->R) is unsatisfiable
first we convert KB & !(P->R) to CNF:
```
!P | Q
!Q | R
P
!R
```

next we pick pairs of clauses and resolve them if we can; we added any clauses produce by this to the collection of clauses:

!P | Q
!Q | R
P
!R

!P | R     (from resolving !P | Q with !Q | R)
Q          (from resolving !P | Q with P)
!Q         (from resolving !Q | R with !R)

by resolving the newly added clauses, we get Q and !Q resolving to the empty clause, meaning we’ve reach a contradiction
this means KB & !(P->R) is unsatisfiable
which means KB entails (P->R)

this is a proof of entailment, and various resolutions are the steps of the proof

as with most proofs, different selection of what clauses to resolve could result in shorter or longer proofs, and in practice you usually want short proofs, and so heuristic would be needed to help make decisions

Horn Clauses and Definite Clauses¶

a definite clause is a clause in which exactly 1 literal is positive, e.g.:

A | !B | !C        definite clause

!A | !W | E | !S   definite clause

P                  definite clause

A | B | !C         not a definite clause

!T                 not a definite clause

a horn clause is a clause with 0 or 1 positive literals (i.e. at most one positive literal), e.g.:

A | !B | !C        horn clause

!A | !B | !C       horn clause

!A                 horn clause

A                  horn clause

note that every definite clause is a horn clause, but some horn clauses are not definite clauses

these restricted forms of clauses are interesting for a few reasons:

entailment of horn clauses an be decided in time linear with respect to the size of the knowledge base – much more efficient than full resolution
reasoning with horn clauses can be done in a straightforward way that humans find easier to follow than resolution
- i.e. forward chaining
definite clauses can be written in an appealing form using implication, i.e. the definite clause A | !B | !C can be written (B & C) -> A
- more generally, the definite clause A | !B1 | !B2 | … | !Bn can be written as (B1 & B2 & … & Bn) -> A
  - the implication is sometimes written in reverse:
    A <- B1 & B2 & ... & Bn
- for some real-world problems, this is can be a natural way to encode knowledge, i.e. A is true if B1, B2, …, and Bn are all true
- horn clauses are used extensively in the logic programming language Prolog

Table Of Contents

Previous topic

Next topic