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.

```
#lang racket
;; Author: Guannan Wei
#| Input format:
((n_1 n_2 (not n_3)) ...)
|#
(define (get-var var)
(match var
[`(not ,var^) var^]
[else var]))
(define (not-neg? var)
(match var
[`(not ,var^) #f]
[else #t]))
(define (neg var)
(match var
[`(not ,var^) var^]
[_ `(not ,var)]))
(define (unit? cls) (eq? 1 (length cls)))
(define (has-unit? f)
(define unit-vars (map car (filter unit? f)))
(if (empty? unit-vars) #f
(car unit-vars)))
(define (get-all-vars cls) (apply set (foldl append '() cls)))
(define (has-pure? f)
(define pure-vars
(foldl append '()
(filter (λ (vs) (eq? 1 (length vs)))
(group-by get-var (set->list (get-all-vars f))))))
(if (empty? pure-vars) #f (car pure-vars)))
(define (assgn-update* a1 a2)
(foldl (λ (kv m) (hash-set m (car kv) (cdr kv))) a1 (hash->list a2)))
(define mt-assgn (make-immutable-hash))
(define (not-contains v) (λ (cls) (if (member v cls) #f #t)))
(define remove-var (curry remove))
(define (elim-unit f uv)
(define assgn (make-immutable-hash (if (not-neg? uv) `((,uv . #t)) `((,(neg uv) . #f)))))
(define new-f (map (remove-var (neg uv)) (filter (not-contains uv) f)))
(values new-f assgn))
(define (pick-var f) (car (car f)))
(define (dpll f assgn)
(cond [(memf (compose zero? length) f) #f]
[(zero? (length f)) assgn]
[(has-unit? f)
=> (λ (uv)
(define-values (new-f new-assgn) (elim-unit f uv))
(dpll new-f (assgn-update* assgn new-assgn)))]
[(has-pure? f)
=> (λ (pv) (dpll (cons `(,pv) f) assgn))]
[else
(define v (pick-var f))
(cond [(dpll (cons `(,v) f) assgn)
=> (λ (assgn) assgn)]
[else (dpll (cons `((not ,v)) f) assgn)])]))
(define (check-sat f)
(define result (dpll f mt-assgn))
(if result #t #f))
```

Some tests:

```
(requrie rackunit)
(check-true (check-sat '((1 2 3))))
(check-true (check-sat '((1 2) ((not 1) (not 2)))))
(check-true (check-sat '((1 (not 5) 4)
((not 1) 5 3 4)
((not 3) (not 4)))))
(check-false (check-sat '(())))
(check-false (check-sat '(() (1))))
(check-false (check-sat '((1 2 3) (2 3 4) ())))
(check-false (check-sat '((1) ((not 1)))))
; 2 queen problem
(check-false (check-sat '((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)))))
```