## coding in Scheme Language.

## coding in Scheme Language.

(OP)

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.

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

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.