;;; 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