ld231782@longs.LANCE.ColoState.Edu (Lawrence Detweiler) (10/14/90)
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
ted@nmsu.edu (Ted Dunning) (10/24/90)
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