Satisfaction Guaranteed

;;; Representation of clauses and formulas:
;;;    A variable is a positive integer
;;;    A literal is a positive or negative integer
;;;    The complement of a literal is the literal times -1
;;;    A clause is a list of literals
;;;    A formula is a list of clauses

;;; Example formulas

  (define f1 '((1 2) (-1 2) (1 -2) (-1 -2)))
  (define f2 '((3 4 -5) (-1 2 -3) (1 3 -4) (-2 -3 4) (3 -4 5)))

;;; Solution:

;;; Remove satisfied clauses and unsatisfied literals from a formula
;;; Input:  an integer v and a formula f
;;; Output: Formula f with clauses containing v missing and
;;;         literals containing -v missing
  (define resolve
    (lambda (l f)
      (cond ((null? f) '())
            ((member l (car f)) (resolve l (cdr f)))
            ((member (- l) (car f))
             (cons (remove (- l) (car f)) (resolve l (cdr f))))
            (else (cons (car f) (resolve l (cdr f)))))))

;;; Algorithm for solving satisfiability of a given formula
;;; Input:  Formula f
;;; Output: #t if f is satisfiable, #f if f is unsatisfiable
  (define sat
    (lambda (f)
      (cond ((member '() f) '())
            ((null? f) #t)
            (else
             (let ((pivot (car (car f))))
               (or (sat (resolve pivot f))
                   (sat (resolve (- pivot) f))))))))