A SAT Solver in 70 Lines

Modern sophisticated SMT solvers (SAT solvers + theories) like Z3 are very powerful in verification and synthesis of programming languages. Yet developing a super fast SAT (satisfiability) solver needs much less efforts, for example, miniSAT only constitutes of ~600 lines of C code. This post presents a simple Racket implementation of DPLL algorithm for solving SAT problem.

A satisfiability problem is asking for an interpretation for boolean variables that makes the formula true. Usually SAT problem expressed in conjunctions of disjunctions form (CNF), and used numbers to represent variabels. For example, this is an CNF boolean formula in S-Expression (the de facto format for SAT solver is DIMACS format, which also supported by my tiny solver):

'((1 2 (not 3)) 
  (2 3 4))

By translating to propsitional logic, it is $ (1 \lor 2 \lor \lnot 3) \land (2 \lor 3 \lor 4) $. This formula is a satisfiable formula, since we can find some assignments to these variables that make the whole formula true.

The core part of DPLL only takes 70 lines of code. This solver can tell you whether the formula is satisfiable, while can not give you an assignment of variables, but it is not difficult to track the assignment histroy. The solver is small, and also usable for small problem – solving a problem with 144 variables and ~2600 clauses just takes seconds. But larger problems seem intractable for it.

The code and tests also can be found in my Github repo.

; Guannan Wei
#| Input format:
((n_1 n_2 (not n_3)) ...)
|#

#lang racket
(define (get-var var)
  (match var
    [`(not ,var^) var^]
    [else var]))

(define (not-neg? var)
  (match var
    [`(not ,var^) #f]
    [else #t]))

(define (propagate var val clauses)
  (define (propagate-clause clause)
    (cond [(empty? clause) clause]
          [(eq? (get-var (first clause)) var)
           (if (eq? (not-neg? (first clause)) val) #f ; we can eliminate this clause
               (propagate-clause (rest clause)))]
          [else (match (propagate-clause (rest clause))
                  [#f #f]
                  [lst (cons (first clause) lst)])]))
  (filter-map propagate-clause clauses))

(define (iter-propagate vars val-f init-clauses)
  (let loop ([vars vars] 
             [clauses init-clauses])
    (cond [(empty? vars) clauses]
          [else (loop (rest vars)
                      (propagate (get-var (first vars))
                                 (val-f (first vars))
                                 clauses))])))

(define (get-unit-clauses clauses)
  (for/list ([clause clauses] #:when (eq? (length clause) 1))
    (first clause)))

(define (eliminate-unit-clause clauses)
  (iter-propagate (get-unit-clauses clauses) not-neg? clauses))

(define (get-all-variables clauses)
  (apply set (foldl append '() clauses)))

(define (appear-only-once? v cmp lst)
  (cond [(empty? lst) #f]
        [(cmp v (first lst))
         (not (appear-only-once? v cmp (rest lst)))]
        [else (appear-only-once? v cmp (rest lst))]))

(define (get-pure-variables clauses)
  (let ([all-vars (set->list (get-all-variables clauses))])
    (filter (λ (v) (appear-only-once? v
                    (λ (x y) (equal? (get-var x)
                                     (get-var y)))
                    all-vars)) all-vars)))

(define (eliminate-pure-variables clauses)
  (iter-propagate (get-pure-variables clauses) not-neg? clauses))

(define (choose-var clauses)
  (cond [(empty? clauses) (error "empty clauses")]
        [else (first (first clauses))]))

(define (dpll clauses)
  (cond [(zero? (length clauses)) #t] ;immediately sat
        [(memf (compose zero? length) clauses) #f] ;immediately unsat
        [else (let ([clauses (eliminate-pure-variables
                              (eliminate-unit-clause clauses))])
                (cond [(zero? (length clauses)) #t]
                      [(memf (compose zero? length) clauses) #f]
                      [else (let ([new-var (get-var (choose-var clauses))])
                              (or (dpll (propagate new-var #t clauses))
                                  (dpll (propagate new-var #f clauses))))]))]))

Some tests:

(requrie rackunit)

(check-true (dpll '((1 2 3))))
(check-true (dpll '((1 2) ((not 1) (not 2)))))
(check-true (dpll '((1 (not 5) 4)
                    ((not 1) 5 3 4)
                    ((not 3) (not 4)))))

(check-false (dpll '(())))
(check-false (dpll '(() (1))))
(check-false (dpll '((1 2 3) (2 3 4) ())))
(check-false (dpll '((1) ((not 1)))))
; 2 queen problem
(check-false (dpll '((1 2)
                     ((not 1) (not 2))
                     (3 4)
                     ((not 3) (not 4))
                     (1 3)
                     ((not 1) (not 3))
                     (2 4)
                     ((not 2) (not 4))
                     ((not 2) (not 3))
                     ((not 1) (not 4)))))