Xref: utzoo comp.theory:1139 comp.lang.scheme:1757
Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!sdd.hp.com!zaphod.mps.ohio-state.edu!ncar!boulder!ccncsu!longs.LANCE.ColoState.Edu!ld231782
From: ld231782@longs.LANCE.ColoState.Edu (Lawrence Detweiler)
Newsgroups: comp.theory,comp.lang.scheme
Subject: satisfiability satisfied
Summary: code to solve the NP complete satisfiability problem in Scheme (LISP dialect from MIT)
Keywords: P NP Scheme SAT satisfiability problem TMP
Message-ID: <10236@ccncsu.ColoState.EDU>
Date: 14 Oct 90 03:49:48 GMT
Sender: news@ccncsu.ColoState.EDU
Lines: 326


To whom it may interest:

I have invented algorithms to solve the satisfiability problem and implemented
them in Scheme.  I am posting one for public scrutiny.  I would be grateful to
converse with anyone knowledgable on the subject.  (Are the algorithms truly
original?  What are their orders of efficiency?)

The program uses Scheme's prefixed notation, recognizing the operators
AND, OR, and NOT.

| 1 ]==> (load "retro.scm")
|
| RETROSPECT
|
| 1 ]==> (retrospect)
|
| (and (or a c) (or b c) (or a c))
|
| ((B . #!TRUE) (A . #!TRUE))
|
| #!TRUE
|

This version (see below) is optimized to find one satisfying assignment.
It writes the solution in a pair-list notation with the variable name and
value for each assignment as the CAR and CDR, respectively, of each pair.
On early Scheme interpreters (like mine) the equivalence of the empty list
#!NULL and the the boolean #!FALSE objects affects the output:

| 1 ]==> (retrospect)
|
| (and a (not b))
|
| ((B) (A . #!TRUE))
|
| #!TRUE

Here `(B)' is actually `(B #!FALSE)' and the list is terminated prematurely.

In the examples above a solution was possible and the program returns #!TRUE.
The program returns #!FALSE if it can't get no satisfaction:

|
| (and a (not a))
|
| ()
|

I also have a minor variation on this version that lists all unique
satisfying assignments:

|
| (and (or a b) (or b c) (or a c))
|
| ((C . #!TRUE) (B . #!TRUE) (A . #!TRUE))
| ((C) (B . #!TRUE) (A . #!TRUE))
| ((C . #!TRUE) (B) (A . #!TRUE))
| ((C . #!TRUE) (B . #!TRUE) (A))
|
| #!TRUE
|

I have many ideas for more elegant (efficient) versions.

I think sophisticated variations on these algorithms may ultimately have the
potential to revolutionize logic programming.

RETRO.SCM

(define (retrospect)

  (define (inspect back with this table)

    (define stack #!null)

    (define bounds #!null)

    (define (try with this here)

      (define to stack)

      (define at bounds)

      (if
        (not
          (null? here)
        )
        (set! stack
          (cons here stack)
        )
      )

      (define (next)

        (let
          (
            (with
              (assq with table)
            )
          )
          (if (null? with)
            (let
              (
                (next
                  (car stack)
                )
              )
              (set! stack
                (cdr stack)
              )
              (next)
            )
            (try
              (cdr with)
              this
              #!null
            )
          )
        )
      )

      (define ok?
        (if (pair? with)
          (
            (cdr
              (assq
                (car with)
                back
              )
            )
            try
            (cdr with)
            this
          )
          (let
            (
              (bound
                (assq with bounds)
              )
            )
            (if (null? bound)
              (begin
                (set! bounds
                  (cons
                    (cons with this)
                    bounds
                  )
                )
                (next)
              )
              (if
                (eq?
                  this
                  (cdr bound)
                )
                (next)
                #!false
              )
            )
          )
        )
      )

      (set! stack to)

      (set! bounds at)

      ok?
    )

    (define (report)

      (write bounds)

      (newline)

      #!true
    )

    (try with this report)
  )

  (define (gate plan)

    (define (from text)

      (define (to code a b c)

        (define depends?
          (eq? a c)
        )

        (define (one of)

          (named-lambda (ok? with in)
            (if (null? with)
              #!false
              (if
                (in
                  (car with)
                  of
                  #!null
                )
                #!true
                (ok?
                  (cdr with)
                  in
                )
              )
            )
          )
        )

        (define (all of)

          (named-lambda (ok? with in)
            (in
              (car with)
              of
              (if
                (null?
                  (cdr with)
                )
                #!null
                (lambda ()
                  (ok?
                    (cdr with)
                    in
                  )
                )
              )
            )
          )
        )

        (define (mix this)

          (lambda (with in)

            (define (head way)

              (in
                (car with)
                way
                (lambda ()
                  (
                    (if this
                      (one
                        (not way)
                      )
                      (all way)
                    )
                    (cdr with)
                    in
                  )
                )
              )
            )

            (if (head this)
              #!true
              (head
                (not this)
              )
            )
          )
        )

        (define (when this that)

          (if depends?
            (mix this)
            (
              (if this
                one
                all
              )
              that
            )
          )
        )

        (cons code
          (lambda (try with this)
            (
              (if this
                (when b c)
                (when
                  (not b)
                  (not c)
                )
              )
              with
              try
            )
          )
        )
      )

      (apply to text)
    )

    (map from plan)
  )

  (define through
    (gate
      (list
        (list 'or #!false #!true #!true)
        (list 'and #!false #!false #!true)
        (list 'not #!true #!false #!false)
      )
    )
  )

  (define roots
    (read)
  )

  (define branches #!null)

  (inspect through roots #!true branches)
)

ld231782@longs.LANCE.ColoState.EDU