---

Implement

… a simple SAT solver in Scheme.

• Procedure ‘satisfiable?’
  • Implement

    <<scheme/truth-table>>
    
    (define (sat? procedure arity)
      "Determine satisfaction of the Boolean PROCEDURE with ARITY."
      (let recur ((table (truth-table procedure arity)))
        (if (null? table) #f
            (or (let ((row (car table)))
                  (or (list-ref row (- (length row) 1))
                      (recur (cdr table))))))))
    

    N.B. Builds on ‘scheme/truth-table’.

  • Test

    <<scheme/sat?>>
    
    (when (sat? (lambda (p) #f) 1) (raise #f))
    (when (sat? (lambda (p q) (and p (not p))) 2) (raise #f))
    
    (unless (sat? (lambda (p q) (and p q)) 2) (raise #f))
    (unless (sat? (lambda (p q) (or p q)) 2) (raise #f))
    
    "tests passed"
    

    tests passed
    

• Procedure ‘truth-table-satisfied’
  • Implement

    <<scheme/truth-table>>
    
    (define (sat procedure arity)
      "Return all inputs that satisfy Boolean PROCEDURE with ARITY."
      (let recur ((table (truth-table procedure arity))
                  (solutions '()))
        (if (null? table)
            (reverse solutions)
            (recur (cdr table)
                   (let ((row (car table)))
                     (if (list-ref row (- (length row) 1))
                         (cons (reverse (cdr (reverse row))) solutions)
                         solutions))))))
    

    N.B. Builds on ‘scheme/truth-table’

  • Test

    <<scheme/sat>>
    
    (unless (equal? (sat (lambda (p q) (or p q)) 2)
                    '((#f #t) (#t #f) (#t #t)))
      (raise #f))
    
    (unless (equal? (sat (lambda (p q) (and p q)) 2)
                    '((#t #t)))
      (raise #f))
    
    "tests passed"
    

    tests passed