How to determine if CNF formula is satisfiable in Scheme?
- by JJBIRAN
Program a SCHEME function sat that takes one argument, a CNF formula represented as above. If we had evaluated (define cnf '((a (not b) c) (a (not b) (not d)) (b d))) then evaluating (sat cnf) would return #t, whereas (sat '((a) (not a))) would return ().
You should have following two 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 consistent (lambda (lit path)
This function takes a literal and a list of literals as arguments, and returns #t whenever the complement of the first argument is not a member of the list represented by the 2nd argument; () otherwise. .
Now for the sat function. The real searching involves the list of clauses (the CNF formula) and the path that has currently been developed. The sat function should merely invoke the real "workhorse" function, which will have 2 arguments, the current path and the clause list. In the initial call, the current path is of course empty.
Hints on sat. (Ignore these at your own risk!)
(define sat (lambda (clauselist)
; invoke satpath
(define satpath (lambda (path clauselist) ; just returns #t or ()
; base cases:
; if we're out of clauses, what then?
; if there are no literals to choose in the 1st clause, what then?
;
; then in general:
; if the 1st literal in the 1st clause is consistent with the
; current path, and if << returns #t,
; then return #t.
;
; if the 1st literal didn't work, then search <<
; the CNF formula in which the 1st clause doesn't have that literal
Don't make this too hard. My program is a few functions averaging about 2-8 lines each. SCHEME is consise and elegant!
The following expressions may help you to test your programs. All but cnf4 are satisfiable. By including them along with your function definitions, the functions themselves are automatically tested and results displayed when the file is loaded.
(define cnf1 '((a b c) (c d) (e)) )
(define cnf2 '((a c) (c)))
(define cnf3 '((d e) (a)))
(define cnf4 '( (a b) (a (not b)) ((not a) b) ((not a) (not b)) ) )
(define cnf5 '((d a) (d b c) ((not a) (not d))
(e (not d)) ((not b)) ((not d) (not e))))
(define cnf6 '((d a) (d b c) ((not a) (not d) (not c))
(e (not c)) ((not b)) ((not d) (not e))))
(write-string "(sat cnf1) ") (write (sat cnf1)) (newline)
(write-string "(sat cnf2) ") (write (sat cnf2)) (newline)
(write-string "(sat cnf3) ") (write (sat cnf3)) (newline)
(write-string "(sat cnf4) ") (write (sat cnf4)) (newline)
(write-string "(sat cnf5) ") (write (sat cnf5)) (newline)
