Xref: utzoo comp.theory:1163 comp.lang.scheme:1766
Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!samsung!uakari.primate.wisc.edu!unmvax!ariel.unm.edu!nmsu!opus!ted
From: ted@nmsu.edu (Ted Dunning)
Newsgroups: comp.theory,comp.lang.scheme
Subject: Re: satisfiability satisfied
Message-ID: <TED.90Oct23150902@kythera.nmsu.edu>
Date: 23 Oct 90 21:09:02 GMT
References: <10236@ccncsu.ColoState.EDU>
Sender: news@NMSU.Edu
Followup-To: comp.theory
Organization: NMSU Computer Science
Lines: 223
In-reply-to: ld231782@longs.LANCE.ColoState.Edu's message of 14 Oct 90 03:49:48 GMT


In article <10236@ccncsu.ColoState.EDU> ld231782@longs.LANCE.ColoState.Edu (Lawrence Detweiler) writes:

   I have invented algorithms to solve the satisfiability problem and
   implemented them in Scheme.

this seems to indicate some confusion.  satisfiability is not a hard
problem to solve, nor is it particularly hard to solve common input
cases quickly.  it is very hard to solve all cases quickly.

   I am posting one for public scrutiny.

this is a brave act and itself should be commended.  

   (Are the algorithms truly original?

here is where is begin to sound less complimentary.  the code as
posted was not only written in such a poor style as to appear
intentionally obfuscatory, but no comments about what the algorithm
actually is appear anywhere.   give the reader a break.

   What are their orders of efficiency?)

who can say if you don't explain what you are doing?

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

i think you will need to buttress this assertion rather more firmly
than this.

   RETRO.SCM
	... 100 lines or so of strangely formatted code deleted.


in order to make this post be a little more constructive, here is _my_
version of a satisfiability program....  hope it helps.

;;; simple code to solve satisfiability.  uses a continuation passing
;;; style to implement a backtracking search.  no attempt is made to
;;; make the search go fast other than using shared variables.

;;; copyright 1990 ted dunning.  right to freely use and modify is
;;; granted if this copyright notice is retained and my contribution
;;; is acknowledged.

;; simple quadratic set operations which work for atoms
;; this is only used to get a list of variables and thus it doesn't
;; matter much how fast it is.
(define (union a b)
  (cond ((null? a) b)
	((memq (car a) b) (union (cdr a) b))
	(else (cons (car a) (union (cdr a) b)))))

;; constructor and selectors for unary and binary expressions
(define (make-exp op lhs rhs)
  (if rhs (list op lhs rhs) (list op lhs)))

(define op car)
(define lhs cadr)
(define rhs caddr)

;; constructor, selectors and mutators for logical variables
(define (make-logical-var name)
  (list 'logical-variable name #f 'unbound))

(define logical-var-name cadr)
(define logical-var-bound? caddr)
(define logical-var-value cadddr)

(define (logical-variable? var)
  (and (pair? var) (eq? (car var) 'logical-variable)))

(define (set-logical-var-bound! var flag)
  (set-car! (cddr var) flag))

(define (set-logical-var-value! var value)
  (set-car! (cdddr var) value))

;; bind a logical VARIABLE to a VALUE.  call the SUCCESS continuation
;; with the FAILURE continuation as an argument if the binding worked
;; or was superfluous, call the failure continuation if it failed
;; because the variable was already bound.  if the variable was bound,
;; then the failure continuation is wrapped with unbinding code so
;; that the binding will be cleaned up if needed.
(define (bind-logical-variable var value win lose)
  (if (logical-var-bound? var)		     ;is it already bound?
      (if (equal? (logical-var-value var) value)
	  (win lose)			     ;to the right value, even?
	  (lose))			     ;no, we lose

      (let ((unbind-and-lose		     ;get ready to unbind later
	     (lambda ()
	       (set-logical-var-bound! var #f)
	       (set-logical-var-value! var 'unbound)
	       (lose))))

	(set-logical-var-bound! var #t)	     ;remember it is bound
	(set-logical-var-value! var value)   ;and set the value
	(win unbind-and-lose))))	     ;win with option to unbind later

;; return a list of the variables in a logical EXPRESSION
(define (free-vars expression)
  (cond ((pair? expression)
	 (if (eq? (op expression) 'not) (free-vars (lhs expression))
	     (union (free-vars (lhs expression))
		    (free-vars (rhs expression)))))
	((symbol? expression) (list expression))
	(else '())))

;; replace all atomic objects in an EXPRESSION with values found in BINDINGS
(define (subs-vars expression bindings)
  (if (pair? expression)
      (make-exp (op expression)
		(subs-vars (lhs expression) bindings)
		(subs-vars (rhs expression) bindings))
      (let ((binding (assoc expression bindings)))
	(if binding (cdr binding) expression))))

;; satisfy an EXPRESSION which contains logical variables.  if this
;; works, then call the SUCCESS continuation with the FAILURE
;; continuation as an argument, if it fails, call the failure
;; continuation with no arguments 
(define (satisfy expression win lose)
  (cond ((logical-variable? expression)
	 (bind-logical-variable expression 'true win lose))

	((pair? expression)
	 (let ((this-op (op expression)))
	   (cond ((eq? this-op 'or)	     ;try the left hand side
		  (satisfy (lhs expression)
			   win
			   (lambda ()	     ;or if that fails, the right
			     (satisfy (rhs expression)
				      win
				      lose))))

		 ((eq? this-op 'and)	     ;make sure both sides work
		  (satisfy (lhs expression)  ;by trying first the left
			   (lambda (fail)    ;then the right
			     (satisfy (rhs expression)
				      win
				      fail))
			   lose))

		 ((eq? this-op 'not)
		  (unsatisfy (lhs expression) win lose)))))

	;; if we have an atom, we succeed only if it is true
	(else (if (eq? expression 'true) (win lose) (lose)))))

;; use demorgan's theorem to find a satisfying assignment for the
;; negation of an expression.  complementary in form to satisfy.
(define (unsatisfy expression win lose)
  (cond ((logical-variable? expression)
	 (bind-logical-variable expression 'false win lose))

	((pair? expression)
	 (let ((this-op (op (expression))))
	   (cond ((eq? this-op 'and)
		  (unsatisfy (lhs expression)
			     win
			     (lambda ()
			       (unsatisfy (rhs expression)
					  win
					  lose))))

		 ((eq? this-op 'or)
		  (unsatisfy (lhs expression)
			     (lambda (fail)
			       (unsatisfy (rhs expression)
					  win
					  fail))
			     lose))
		 ((eq? this-op 'not)
		  (satisfy (lhs expression) win lose)))))

	(else (if (eq? expression 'false) (win lose) (lose)))))


;; convert an EXPRESSION to an equivalent that uses logical variables,
;; attempt to satisfy it and then return either a list of bindings, or
;; the atom 'failed.
(define (sat expression)

  ;; convert an EXPRESSION to use logical variables so that updates one
  ;; place will be reflected everywhere in the expression
  (let* ((vars (free-vars expression))
	 (logical-vars (map make-logical-var vars))
	 (bindings (map cons vars logical-vars)))
    (satisfy (subs-vars expression bindings)
	     (lambda (fail)
	       (map (lambda (var lvar)
		      (cons var (logical-var-value lvar)))
		    vars logical-vars))
	     (lambda () 'failed))))

;; return a list of all satisfying assignments of an EXPRESSION.
;; works like sat, except, on success, we store the results and try
;; again.  on failure, we return the empty list.
(define (all-sat expression)
  ;; convert an EXPRESSION to use logical variables so that updates one
  ;; place will be reflected everywhere in the expression
  (let* ((results '())
	 (vars (free-vars expression))
	 (logical-vars (map make-logical-var vars))
	 (bindings (map cons vars logical-vars)))
    (satisfy (subs-vars expression bindings)
	     (lambda (fail)
	       (set! results
		     (cons
		      (map (lambda (var lvar)
			     (cons var (logical-var-value lvar)))
			   vars logical-vars)
			   results))
	       (fail))
	     (lambda () results))))



--
I don't think the stories are "apocryphal".  I did it :-)  .. jthomas@nmsu.edu