I need help. I am not quite familiar with scheme lang and this HW just came.

=============================================================


Consider the following example:

( and (or a (not b) (not (or (not c) d))) (or b d) )

This is not CNF, but an equivalent CNF formula is

( and (or a (not b) c) (or a (not b) (not d)) (or b d) )

There are 3 clauses, two with 3 literals and one with 2 literals. The
truth-table would have 16 rows since there are 4 propositional
variables: a, b, c, and d.  Rather than use strict boolean logic
syntax, it is convenient to represent a CNF formula as simply a list
of lists of literals. In other words, a CNF formula is a list of
clauses, and a clause is a list of literals.  With this convention,
the above CNF formula would be represented as

((a (not b) c)  (a (not b) (not d))  (b d))

The literals (not d) in the second clause and d in the third clause
are said to be complements of each other. In other words, negating
one makes it equal to the other [e.g., (not (not d)) = d].

The satisfiability of a CNF (or of any) formula can of course be
determined using truth tables. But there is another way to consider
this: A CNF formula is satisfiable if and only if at least one literal
from every clause can be made true. Since a clause is a disjunction,
the one true literal makes the clause true, and since every clause
is thus true, the conjunction of the clauses is true.

Thus one way to determine if a CNF formula is satisfiable is to try to
find a list of literals, one from each clause, that can all be made
true. Why could this be difficult -- why can't we just pick a
literal from each clause and set them all true? Well, suppose our
collection (sometimes called a "path" through the clauses) contained
both a literal and its complement. For example, if we choose "a" from
the first clause, "(not b)" from the 2nd clause, and "b" from the 3rd
clause, then our path is (a (not b) b). Well, we cannot assign these 3
literals true, because we cannot make both "b" and "(not b)"
simultaneously true.

So we may have to search through many or all of the paths through
the clauses in our CNF formula to find one, all of whose literals
can simultaneously be made true. In fact, if the formula is
unsatisfiable, then ALL of the paths will contain complementary
literals.

Is there a simple way to find and search through all the paths? Well,
if we think of each clause as a set, then any path through the
clauses is simply a member of the cross-product of those sets.
In our example above, the cross-product of the 3 clauses would have
eighteen 3-tuples:

((a a b)                  (a a d)                 (a (not b) b)
 (a (not b) d)            (a (not d) b)           (a (not d) d)
 ((not b) a b)            ((not b) a d)           ((not b) (not b) b)
 ((not b) (not b) d)      ((not b) (not d) b)     ((not b) (not d) d)
 (c a b)                  (c a d)                 (c (not b) b)
 (c (not b) d)            (c (not d) b)           (c (not d) d))

We have now reduced the problem of satisfiability testing to the
problem of searching through a list of n-tuples to see if any one
n-tuple is consistent -- i.e., if it does not contain both a
literal and its complement.

First, how do we get the list of n-tuples? Easy, our mcross function
from the class slides:

(define (mcross setlist)
  (cond ((< (length setlist) 2)  ())
        ((= (length setlist) 2)  (cross (car setlist) (cadr setlist)))
        ((null? (car setlist)) ())
        (#t  (append (tackon (caar setlist)
                             (mcross (cdr setlist)) )
                     (mcross (cons (cdar setlist) (cdr setlist))) )) ) )

(define (cross set1 set2)
  (cond ((or (null? set1) (null? set2))  ())
        (#t  (cons (list (car set1) (car set2))
                   (append (cross (list (car set1))  (cdr set2))
                           (cross (cdr set1) set2) ) )) ) )

(define (tackon e l)
  (cond ((null? l)  ())
        (#t  (cons (cons e (car l))
                   (tackon e (cdr l)) )) ) )


This assignment comes in two parts, worth a total of 13 (out of 10)
points. In other words, there is extra credit built-in. But no
single question or part is designated as extra credit. It's just
that the total is 13.

Part 1) (8 points)

You are to design a function satx that takes a CNF formula as its only
argument. As above, the formula is represented as a list of lists of
literals. The function satx returns the first satisfiable path it
finds, or else returns () in case there are none. These formulas are
already proper input to mcross, so it's easy to produce a list of
their paths. If we define cnf1 and cnf4 as follows:

(define cnf1 '((a b c) (c d) (e)) )
(define cnf4 '( (a b) (a (not b)) ((not a) b) ((not a) (not b)) ) )

then (satx cnf1) = (a c e)
and  (satx cnf4) = ()


Hint: There are of course many ways to break down this computation.
Here is one that works nicely:

Get these functions to work:

(define comp (lambda (lit)
  ;  

This function takes a literal as argument and returns the complement
literal as the returning value. Examples: (comp 'a) = (not a), and
(comp '(not b)) = b.

(define noclash (lambda (lit path)
  ; returns #t if the complement of lit is not a member of path


(define consistent (lambda (path)

This function returns #t whenever path does not contain a
complementary pair of literals; () otherwise.  The empty path is
consistent, and in general, a path is consistent if the first literal
does not clash with the rest of the path AND if the rest of the path
is consistent.

If you have the 3 functions above working, it's easy to write
a function goodpath that takes a list of paths and returns the
first path that is consistent (if there is one), and returns ()
if none are consistent.

(define goodpath (lambda (pathlist)


Finally, if we have goodpath, then satx is easy because given
a CNF formula, all we have to do is feed the cross-product of
its clauses to goodpath.