\documentstyle[11pt]{article}
% frob with the margins
\addtolength{\topmargin}{-1in}
\addtolength{\footskip}{-1in}
\addtolength{\textheight}{2in}
\addtolength{\oddsidemargin}{-.5in}
\addtolength{\evensidemargin}{-.5in}
\addtolength{\textwidth}{1in}
% no indent
\setlength{\parindent}{0pt}
% no page numbers
\pagestyle{empty}
% counter for page numbers
\newcounter{pg}
\setcounter{pg}{2}

% DEFINE THE PROBLEM SET NUMBER
\def\psnum{5}

% title command
\newcommand{\mytitle}[1]{\begin{center} {\Large Artificial Intelligence -- 
6.034 Problem Set \psnum \\ Juliet Bourne -- Section R1 -- #1} \\ 
\vspace{-.1in}
\rule{6in}{.5mm} \end{center}}
% problem command
\newcommand{\prob}[1]{\vspace{.15in}\noindent{\fbox{\large\bf Problem #1}}}
% subproblem command
\newcommand{\subprob}[1]{\vspace{.15in} \noindent{\large\bf #1.}}
% equations commands
\newcommand{\beq}{\(\begin{array}{l}}
\newcommand{\eeq}{\end{array}\)\vspace*{.2in}}
% newpage setup command 
\newcommand{\mynewpage}{\newpage\noindent
\begin{center}
{\Large 6.034 Problem Set \psnum -- Juliet Bourne -- {\bf Page \thepg}}
\rule{6in}{.5mm}
\end{center}
\addtocounter{pg}{1}}
% see-page command
\newcommand{\seepage}{\noindent See page \rule{.2in}{.1mm} for the
computer output.}

\begin{document}

\mytitle{11/2/90}

\prob{A}

Putting clause 1 into standard logical notation:
\begin{verbatim}
(not clear x s) (not clear y s) (equal x y) (on x y (puton x y s)) 
\end{verbatim}

\beq
\neg Clear(x,s) \vee \neg Clear(y,s) \vee Equal(x,y) \vee
On(x,y,Puton(x,y,s)) \\
\neg ( Clear(x,s) \wedge Clear(y,s) \wedge \neg Equal(x,y) ) \vee
On(x,y,Puton(x,y,s)) \\
\forall x \forall y \forall s [Clear(x,s) \wedge Clear(y,s) \wedge
\neg Equal(x,y) \Rightarrow On(x,y,Puton(x,y,s))]
\eeq

Clause 2:
\begin{verbatim}
(not on x y s) (not clear x s) (not clear z s) (equal y z) (equal x z)
(clear y (puton x z s))
\end{verbatim}

\beq
\neg On(x,y,s) \vee \neg Clear(x,s) \vee Clear(z,s) \vee Equal(y,z)
\vee \neg Clear(y,Puton(x,z,s)) \\
\neg ( On(x,y,s) \wedge Clear(x,s) \wedge Clear(z,s) \wedge \neg
Equal(y,z) \wedge \neg Equal(x,z) ) \vee Clear(y,Puton(x,z,s)) \\
\forall x \forall y \forall z \forall s [On(x,y,s) \wedge Clear(x,s) 
\wedge Clear(z,s) \wedge \neg Equal(y,z) \wedge \neg Equal(x,z) \\
\hspace*{.75in} \Rightarrow Clear(y,Puton(x,z,s))]
\eeq

Clause 3:
\begin{verbatim}
(not clear u s) (equal u y) (clear u (puton x y s))
\end{verbatim}

\beq
\neg Clear(u,s) \vee Equal(u,y) \vee Clear(u,Puton(x,y,s)) \\
\neg ( Clear(u,s) \wedge \neg Equal(u,y) ) \vee Clear(u,Puton(x,y,s)) \\
\forall x \forall y \forall z \forall s [Clear(u,s) \wedge \neg Equal(x,y)
\Rightarrow Clear(u,Puton(x,y,s))]
\eeq

Clause 4: $ \forall s [ Clear(table,s) ] $

Clause 5: $ On(b,a,S_0) $

Clause 6: $ On(a,table,S_0) $

Clause 7: $ Clear(b,S_0) $

Clause 8: $ Clear(c,S_0) $

Clause 9: $ On(c,table,S_0) $

Clause 11: $ \neg Equal(a,table) $

Clause 12: $ \neg Equal(b,table) $

Clause 13: $ \neg Equal(c,table) $

Clause 14: $ \neg Equal(a,b) $

Clause 15: $ \neg Equal(a,c) $

Clause 16: $ \neg Equal(b,a) $

Clause 17: $ \neg Equal(b,c) $

Clause 18: $ \neg Equal(c,a) $

Clause 19: $ \neg Equal(c,b) $

\vspace*{.1in}
Clause 10 (the negated goal):
\begin{verbatim}
(not clear a s) (not clear c s)
\end{verbatim}

\beq
\neg Clear(c,s) \vee \neg Clear(a,s) \\
\neg ( Clear(c,s) \wedge Clear(a,s) ) \\
\forall s [ \neg ( Clear(c,s) \wedge Clear(a,s) ) ] \\
\neg \exists s [ Clear(c,s) \wedge Clear(a,s) ]
\eeq

\mynewpage

\prob{B} Since the goal is to have both block A and block C clear,
intuitively the plan to reach this will be to put block B on the table.
Using this knowledge, resolving the clauses to reach a contradiction and
thus ``prove'' the goal is fairly easy.

\vspace*{.1in}
Resolve (2) and (10): $ y\rightarrow a \; \; s_{10} \rightarrow
Puton(x,z,s_{20}) $

Clause 20: 

\beq
\neg Clear(c,Puton(x,z,s_{20})) \vee \neg On(x,a,s_{20}) \vee 
\neg Clear(x,s_{20}) \vee \neg Clear(z,s_{20}) \\
\vee Equal(a,z) \vee Equal(x,z)
\eeq

Resolve (5) and (20): $ x \rightarrow b \; \; s_{20} \rightarrow S_0 $

Clause 21:

\beq
\neg Clear(c,Puton(b,z,S_0)) \vee \neg Clear(b,S_0) \vee 
\neg Clear(z,S_0) \vee Equal(a,z) \vee Equal(b,z)
\eeq

Resolve (4) and (21): $ z \rightarrow table \; \; s_4 \rightarrow S_0 $

Clause 22:

\beq
\neg Clear(c,Puton(b,table,S_0)) \vee \neg Clear(b,S_0) \vee 
Equal(a,table) \vee Equal(b,table)
\eeq

Resolve (11) and (22): 

Clause 23:

\beq
\neg Clear(c,Puton(b,table,S_0)) \vee \neg Clear(b,S_0) \vee 
Equal(b,table)
\eeq

Resolve (12) and (23):

Clause 24: $ \neg Clear(c,Puton(b,table,S_0)) \vee \neg Clear(b,S_0) $

\vspace*{.1in}
Resolve (3) and (24): $ u \rightarrow c \; \; x \rightarrow b \; \; s_3
\rightarrow S_0 $

Clause 25: $\neg Clear(b,S_0) \vee \neg Clear(c,S_0) \vee Equal(c,table) $

\vspace*{.1in}
Resolve (13) and (25):

Clause 26: $\neg Clear(b,S_0) \vee \neg Clear(c,S_0) $

\vspace*{.1in}
Resolve (7) and (26):

Clause 27: $\neg Clear(c,S_0) $

\vspace*{.1in}
Resolve (8) and (27): {\bf Contradiction}

\vspace*{.1in}
Tracing the resolution backwards, a plan to achieve the goal can be
derived. 

\beq
s_{10} \rightarrow Puton(x,z,s_{20}) \\
x \rightarrow b \; \; \; s_{20} \rightarrow S_0 \\
z \rightarrow table 
\eeq

Thus the plan is: $ Puton(b,table,S_0) $

\mynewpage

\prob{C}

\begin{verbatim}
 CYCLE=0, 1 clauses waiting to resolve ...
 RESOLVE called with:
   (10 (S) ((NOT CLEAR A S) (NOT CLEAR C S))) 
   (2 (X Y Z S)
    ((NOT ON X Y S) (NOT CLEAR X S) (NOT CLEAR Z S) (EQUAL Y Z)
     (EQUAL X Z) (CLEAR Y (PUTON X Z S)))) 
 Resolvents are:
(20 (Y4 Y3 Y1)
 ((NOT CLEAR C (PUTON Y1 Y3 Y4)) (NOT ON Y1 A Y4) (NOT CLEAR Y1 Y4)
  (NOT CLEAR Y3 Y4) (EQUAL A Y3) (EQUAL Y1 Y3)))

 CYCLE=2, 6 clauses waiting to resolve ...
 RESOLVE called with:
   (20 (Y4 Y3 Y1)
    ((NOT CLEAR C (PUTON Y1 Y3 Y4)) (NOT ON Y1 A Y4) (NOT CLEAR Y1 Y4)
     (NOT CLEAR Y3 Y4) (EQUAL A Y3) (EQUAL Y1 Y3))) 
   (5 NIL ((ON B A S0))) 
 Resolvents are:
(34 (X2)
 ((NOT CLEAR C (PUTON B X2 S0)) (NOT CLEAR B S0) (NOT CLEAR X2 S0)
  (EQUAL A X2) (EQUAL B X2)))

 CYCLE=3, 30 clauses waiting to resolve ...
 RESOLVE called with:
   (34 (X2)
    ((NOT CLEAR C (PUTON B X2 S0)) (NOT CLEAR B S0) (NOT CLEAR X2 S0)
     (EQUAL A X2) (EQUAL B X2))) 
   (4 (S) ((CLEAR TABLE S))) 
 Resolvents are:
(53 NIL
 ((NOT CLEAR C (PUTON B TABLE S0)) (NOT CLEAR B S0) (EQUAL A TABLE)
  (EQUAL B TABLE)))

 CYCLE=4, 42 clauses waiting to resolve ...
 RESOLVE called with:
   (53 NIL
    ((NOT CLEAR C (PUTON B TABLE S0)) (NOT CLEAR B S0) (EQUAL A TABLE)
     (EQUAL B TABLE))) 
   (3 (X Y S U) ((NOT CLEAR U S) (EQUAL U Y) (CLEAR U (PUTON X Y S)))) 
 Resolvents are:
(64 NIL
 ((NOT CLEAR B S0) (EQUAL A TABLE) (EQUAL B TABLE) (NOT CLEAR C S0)
  (EQUAL C TABLE)))
\end{verbatim}

\mynewpage

\begin{verbatim}
 CYCLE=133, 54 clauses waiting to resolve ...
 RESOLVE called with:
   (64 NIL
    ((NOT CLEAR B S0) (EQUAL A TABLE) (EQUAL B TABLE) (NOT CLEAR C S0)
     (EQUAL C TABLE))) 
   (7 NIL ((CLEAR B S0))) 
 Resolvents are:
(516 NIL
 ((EQUAL A TABLE) (EQUAL B TABLE) (NOT CLEAR C S0) (EQUAL C TABLE)))

 CYCLE=134, 51 clauses waiting to resolve ...
 RESOLVE called with:
   (516 NIL
    ((EQUAL A TABLE) (EQUAL B TABLE) (NOT CLEAR C S0) (EQUAL C TABLE))) 
   (8 NIL ((CLEAR C S0))) 
 Resolvents are:
(521 NIL ((EQUAL A TABLE) (EQUAL B TABLE) (EQUAL C TABLE)))

 CYCLE=135, 55 clauses waiting to resolve ...
 RESOLVE called with:
   (521 NIL ((EQUAL A TABLE) (EQUAL B TABLE) (EQUAL C TABLE))) 
   (11 NIL ((NOT EQUAL A TABLE))) 
 Resolvents are:
(525 NIL ((EQUAL B TABLE) (EQUAL C TABLE)))

 CYCLE=136, 58 clauses waiting to resolve ...
 RESOLVE called with:
   (525 NIL ((EQUAL B TABLE) (EQUAL C TABLE))) 
   (12 NIL ((NOT EQUAL B TABLE))) 
 Resolvents are:
(528 NIL ((EQUAL C TABLE)))

 CYCLE=137, 60 clauses waiting to resolve ...
 RESOLVE called with:
   (528 NIL ((EQUAL C TABLE))) 
   (13 NIL ((NOT EQUAL C TABLE))) 
 Resolvents are:
(CONTRADICTION 528 13)
\end{verbatim}

It takes 137 cycles to arrive at this contradiction, and the queue of
clauses waiting to be resolved grows to 75 clauses. The only real
difference between my hand resolution and this resolution was the
ordering of some of the resolutions.

\mynewpage

\prob{D} It seems like a good idea to try to resolve the shorter and
less complex clauses before trying the more hairier clauses, since
simpler resolvents would probably result. However, despite the fact that
I wrote a procedure which figures out the nesting of a list, which
include the length of the list, using this as the comparison function
for clauses made matters worse, not better. Here's my code anyway:

\begin{verbatim}
(defun nested (x &optional (cnt 0))
  (if (atom x)
      cnt
      (if (listp (car x))
          (+ cnt (nested (car x) 1) (nested (cdr x)))
          (nested (cdr x) cnt))))

(defun clause-is-better (clause-1 clause-2)
  (< (nested (clause-literals clause-1))
     (nested (clause-literals clause-2))))
\end{verbatim}

\prob{E} Like I said in D, my {\bf clause-is-better} function caused the
queue of clauses waiting to resolve to grow more than the original.
Therefore, I have nothing useful to show.

\prob{F} It's a bad idea because the later clauses will be preferref
over the older clauses. The later clauses will always be put ahead of
the previous clauses, no matter if they are worse (more off-the-mark)
than the previous clauses. This has a vicious circle effect, since the
later and possbily worse clauses will get resolved against the input
clauses, creating new clauses, which are probably even worse, which
(since they have higher clause numbers) will be put at the head of the
queue of clauses waiting to resolve. It seems that only sheer luck would
let this sorting of clauses actually produce a contradiction.

\end{document}
