… as a computational problem of determining

satisfiability of a given molecular statement,

typically in the conjunctive normal form.

NP-complete with 3 or more literals per clause (3SAT).

… 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

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

- Implement

- Assign hard-to-satisfy vars first, to cut down the search space.
- Can be made into an optimization problem of minimizing unsat clauses.

© 2024 Rudolf Adamkovič under GNU General Public License version 3.

Made with Emacs and secret alien technologies of yesteryear.