CMPUT 325 - Assignment #1

Due Date: 11:59pm, Tuesday 28/Sept/04, using 

try c325 a1 your_file
You should submit one file containing all your programs along with documentation. Your programs will be run against our solutions and results generated. This may provide feedback to your work. You can keep submitting, and the last one before the deadline will be retained as your submission. Questions on the try command can be directed to tommy@cs.ualberta.ca

Assignment Marks: There are a total of 65 marks possible on this assignment.  It is worth 8% of the total course grade. Your programs must be readable and understandable as well as correct. You should read the guidelines as given in programming style and marking guideline. You could lose up to 1/2 of the marks for bad style even if your programs are correct.
(25/Sept: Changed "penalty for bad style", from 1/3 to 1/2, to be consistent with other documentation, and TA's earlier comments.)

Restrictions:

You may only use the built-in Lisp functions and special forms shown here

You may write one or more functions to solve any given problem below. In some cases it is desirable to decompose a problem into smaller ones. However, if a problem has a straightforward single-function solution, it's a bad idea to solve it in a complex way by decomposition.

#1 (5 marks)  Write the Lisp function 
    (my-min L)
that returns  the minimum value of the argument list-of-numbers L.
You may assume L is a list with at least 1 element, which includes only numeric values.
 
>(my-min '(3 1 -5 2)
-5

>(my-min '(1))
1

#2 (10 mark)  Write the Lisp function 
   (deep-member x y)
that returns T if the first argument x appears anywhere at any level in the argument recursive-list y and NIL otherwise. This should test for lists being members of lists. Both the argument x and the list y may be NIL or lists containing NIL. See the examples. You cannot just call the built-in function member (see restrictions above).
(22/Sept: Corrected version appears above -- the first argument need not be an atom.)
Examples: 
>(deep-member '1 '(1) )
T
>(deep-member '1 '( (1) 2 3) )
T
>(deep-member '1 '( ((4 1)) 2 3) )
T
>(deep-member '(1) '((1) 2 3) )
T
>(deep-member nil nil)
NIL
>(deep-member nil '(nil) )
T
>(deep-member nil '((nil) ) )
T
>(deep-member '(nil) '(1 2 3 (nil)) )
T
>(deep-member '(3) '(3) )
NIL

#3 (10 mark)  Write the Lisp function: 
    (deep-subst x y L)
that returns returns a list L1 formed by replacing, within the recursive-list L, each occurance of the atom x (at any level) with the atom y.
(You may assume that L is a recursive list, and that x and y are each atoms.)

>(deep-subst 4 t '(truth is 4))
(TRUTH IS T)

>(deep-subst
4 nil '(4 is not (4)))
(NIL IS not (NIL))

>(deep-subst 4 nil '(5 is not (22)))
(5 is not (22))

#4 (5 marks)   Write the Lisp function 
      (lookup atom pair-list)
that finds the "atom-entry" within the list of pairs pair-list, or NIL if atom does not match any of the entries in pair-list .
You may assume that atom is an atom and pair-list is a list whose entries are each 2-element lists, whose FIRST element is always an atom.
>(lookup '5 '((t frog) (5 what) (nil 1)))
(5 what)

>(lookup 5 '((1 this) (2 is) (3 a) (4 test)) )
nil

#5 (15 marks)   In general, a "conjunctive normal form" (CNF)  formula is a conjunction of clauses, where each clause is  a disjunction of literals, and each literal is either a variable or its negation -- eg,
   cnf1 =   (-x1 v -x2 v +x3)  &  (+x2 v +x4 v -x5)
(We will later see that any boolean formula can be expressed as a CNF formula.)
Given a set of variables, an assignment maps each variable to either true (T) or false (NIL) --
e.g., the assignment 
   assgn1  =  ( (x1 t) (x2 nil) (x3 t) (x4 nil) (x5 t ) )

maps x1 to T, x2 to NIL, x3 to T, x4 to NIL and x5 to T.

Given a specific assign assgn, the CNF formula cnf evaluates to T if each of its clauses evaluates to T (otherwise it evaluates NIL); and a clause evaluates to T if at least one of its literals evaluates to T (otherwise it evaluates to NIL), and a positive literal  +X1 is T if it is assigned to T in assgn; and a negative literal  -X3 is T if it is assigned to NIL in assgn.
Eg, using assgn1 , the first clause of cnf1,
   (-x1 v -x2 v +x3)
 evaluates to T as its 2nd literal, -x2, evaluates to T as assgn1 includes (x2 nil).
However, cnf1's second clause
  (+x2 v +x4 v -x5)
evaluates to NIL as each of its 3 literals evaluates to NIL.
Hence, the conjunction of these clauses, cnf1, evaluates to NIL.

Write the Lisp function 
     (eval-cnf cnf assgn)
that evaluates the boolean CNF formula cnf formula, with respect to the assignment assgn, returning T if assgn satisfies cnf, and NIL otherwise.
We encode a CNF as a list of clauses, where each clause is represented as a list of literals, and each literal is a two element list of + or -, followed by variable-name.  ("+" means the variable is true, "-" for false).
Hence   we would write
     (+x1 v -x2 v +x3)  &  (+x2 v +x4 v -x5)
as
     ( ((+ x1) (- x2) (+ x3))  ((+ x2) (+ x4) (- x5)) )
As shown above, we represent an assignment as a list of   (variable value)   pairs; see assgn1 above.

Note the empty CNF list is true, and the empty clause (within the list) is false.
(23/Sept: Corrected version appears above -- the "true" and "false" were backwards! Also corrected the first example below, and added another example.) 
> (eval-cnf  '()  '((a t)))
T

> (eval-cnf  '(() ((+ a)) )  '((a t)))
NIL

> (eval-cnf  '( ((+ a)) ) '((a t)))
T 

> (eval-cnf  '( ((+ a)) ) '((a nil)))
NIL 

> (eval-cnf  '( ((+ a) (- a)) ) '((a nil)))
T 

> (eval-cnf  '( ((+ a) (- b)) ) '((a nil)(b nil)))
T 

> (eval-cnf  '( ((+ a) (- b)) ((- a)) ) '((a nil)(b nil)))
T 

> (eval-cnf  '( ((+ a) (- b)) ((+ a)) ) '((a nil)(b nil)))
NIL

#6 (20 mark) Satisfiability -- finding a satisfying assignment for a boolean formula -- is one of the core ideas in computing science. It is used for verifying hardware, verifying software, reasoning, planning, as well as other areas of artificial intelligence.  And of course, all NP-hard problems reduce to satisfiability.  We will later see it is the core procedure for proving arbitrary conclusions from known information.

Write a LISP function

      (sat cnf) 

that returns a satisfying assignment if the CNF formula cnf  is satisfiable, and otherwise return NIL.

This function should use the simple "generate and test" approach:  successively generate each possible assignments to the variables, then test if that assignment satisfies the CNF formula -- ie, if it makes the CNF true (hint: think eval-cnf).
Given a list of the variables in the formula, there is a simple recursive way to walk through the set of all assignments.  You need only generate one assignment -- ie, your function should terminate on finding a satisfying assignment.

> (sat '( ((+ a)) ) ) 
((a t)) 

> (sat '( ((+ a)) ((- a)) ) ) 
NIL 

> (sat '( ((+ a)) ((- b)) ) ) 
((a t) (b nil)) 

> (sat '( ((+ a) (+ b)) ((- b)) ) ) 
((a t) (b nil)) 


   ;; ORIG: (a->b) &  (b->c) &  (c->-a)
   ;;       (~a v b) & (~b v c) & (~c v ~ a)
   ;; CNF + ( (~a b) (~b c) (~c ~a) )

> (sat '( ((- a) (+ b)) ((- b) (+  c)) ((- c) (- a)) ) )
((A NIL) (B T) (C T)) 

   ;; a->b, b->c, c-> d
> (sat '( ((- a ) (+ b)) ((- b) (+  c)) ((- c) (+ d)) ) )
( (a t) (b t) (c t) (d t)) 


   ;; a <=> b, -a , b
   ;; a-> b, b->a, -a, b
> (sat '( ((- a) (+ b)) ((- b) (+ a)) ((- a)) ((+ b)) ) ) 
nil
End of Assignment 1.