---

Implement

… a simple SAT solver in Scheme.

• Procedure ‘satisfiable?’
  • Implement

    (define (boolean-product length)
      "Return a list of all Boolean sequences of LENGTH."
      (let more-rows ((row (- (expt 2 length) 1)))
        (if (< row 0) (list)
            (cons (let more-columns ((column (- length 1)))
                    (if (< column 0) (list)
                        (cons (even? (quotient row (expt 2 column)))
                              (more-columns (- column 1)))))
                  (more-rows (- row 1))))))
    (define (truth-table procedure arity)
      "Return a truth table for PROCEDURE with ARITY."
      (map (lambda (inputs)
             (append inputs (list (apply procedure inputs))))
           (boolean-product arity)))
    
    (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

    
    
    (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

    (define (boolean-product length)
      "Return a list of all Boolean sequences of LENGTH."
      (let more-rows ((row (- (expt 2 length) 1)))
        (if (< row 0) (list)
            (cons (let more-columns ((column (- length 1)))
                    (if (< column 0) (list)
                        (cons (even? (quotient row (expt 2 column)))
                              (more-columns (- column 1)))))
                  (more-rows (- row 1))))))
    (define (truth-table procedure arity)
      "Return a truth table for PROCEDURE with ARITY."
      (map (lambda (inputs)
             (append inputs (list (apply procedure inputs))))
           (boolean-product arity)))
    
    (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

    (define (boolean-product length)
      "Return a list of all Boolean sequences of LENGTH."
      (let more-rows ((row (- (expt 2 length) 1)))
        (if (< row 0) (list)
            (cons (let more-columns ((column (- length 1)))
                    (if (< column 0) (list)
                        (cons (even? (quotient row (expt 2 column)))
                              (more-columns (- column 1)))))
                  (more-rows (- row 1))))))
    (define (truth-table procedure arity)
      "Return a truth table for PROCEDURE with ARITY."
      (map (lambda (inputs)
             (append inputs (list (apply procedure inputs))))
           (boolean-product arity)))
    
    (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))))))
    
    (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