Source code for the Primer on Boolean Satisfiability

example.cnf

c FILE: aim-50-1_6-yes1-4.cnf
c
c SOURCE: Kazuo Iwama, Eiji Miyano (miyano@cscu.kyushu-u.ac.jp),
c          and Yuichi Asahiro
c
c DESCRIPTION: Artifical instances from generator by source.
c              Generators and more information in
c              sat/contributed/iwama.
c
c NOTE: Satisfiable
c
p cnf 50 80
16 17 30 0
-17 22 30 0
-17 -22 30 0
16 -30 47 0
16 -30 -47 0
-16 -21 31 0
-16 -21 -31 0
-16 21 -28 0
-13 21 28 0
13 -16 18 0
13 -18 -38 0
13 -18 -31 0
31 38 44 0
-8 31 -44 0
8 -12 -44 0
8 12 -27 0
12 27 40 0
-4 27 -40 0
12 23 -40 0
-3 4 -23 0
3 -23 -49 0
3 -13 -49 0
-23 -26 49 0
12 -34 49 0
-12 26 -34 0
19 34 36 0
-19 26 36 0
-30 34 -36 0
24 34 -36 0
-24 -36 43 0
6 42 -43 0
-24 42 -43 0
-5 -24 -42 0
5 20 -42 0
5 -7 -20 0
4 7 10 0
-4 10 -20 0
7 -10 -41 0
-10 41 46 0
-33 41 -46 0
33 -37 -46 0
32 33 37 0
6 -32 37 0
-6 25 -32 0
-6 -25 -48 0
-9 28 48 0
-9 -25 -28 0
19 -25 48 0
2 9 -19 0
-2 -19 35 0
-2 22 -35 0
-22 -35 50 0
-17 -35 -50 0
-29 -35 -50 0
-1 29 -50 0
1 11 29 0
-11 17 -45 0
-11 39 45 0
-26 39 45 0
-3 -26 45 0
-11 15 -39 0
14 -15 -39 0
14 -15 -45 0
14 -15 -27 0
-14 -15 47 0
17 17 40 0
1 -29 -31 0
-7 32 38 0
-14 -33 -47 0
-1 2 -8 0
35 43 44 0
21 21 24 0
20 29 -48 0
23 35 -37 0
2 18 -33 0
15 25 -45 0
9 14 -38 0
-5 11 50 0
-3 -13 46 0
-13 -41 43 0

normal-forms.rkt

#lang racket

(provide nnf dnf cnf)

; Converts f to NNF by first limiting operators
; to ∧,∨¬ and then pushing ¬ down to the leaves
; (literals) of the formula.
(define (nnf f)
 (nnf-neg (nnf-ops f)))

; Converts f to DNF by first converting it to NNF,
; then distributing ∧ over ∨, and finally flattening
; out nested conjunctions and disjunctions.
(define (dnf f)
  (unnest (distribute '∧ '∨ (nnf f))))

; Converts f to CNF as done for the DNF conversion but
; swapping ∧ for ∨ and vice versa.
(define (cnf f)
  (unnest (distribute '∨ '∧ (nnf f))))

; Returns a formula that is equivalent to f but
; uses only the connectives allowed by NNF: ∧∨¬.
(define (nnf-ops f)
  (match f
    [`(→ ,(app nnf-ops f1) ,(app nnf-ops f2))
     `(∨ (¬ ,f1) ,f2)]
    [`(↔ ,(app nnf-ops f1) ,(app nnf-ops f2))
     `(∧ (∨ (¬ ,f1) ,f2) (∨ (¬ ,f2) ,f1))]
    [`(,op ,fs ...)
     `(,op ,@(map nnf-ops fs))]
    [_ f]))

; Assuming that f contains only the NNF connectives,
; returns a formula that is equivalent to f but with
; negations (¬) occuring only in literals.
(define (nnf-neg f)
  (match f
    [`(¬ ⊥) `⊤]
    [`(¬ ⊤) `⊥]
    [`(¬ ,(? symbol?)) f]
    [`(¬ (¬ ,f1)) (nnf-neg f1)]
    [`(¬ (∧ ,fs ...))
     `(∨ ,@(for/list ([fi fs]) (nnf-neg `(¬ ,fi))))]
    [`(¬ (∨ ,fs ...))
     `(∧ ,@(for/list ([fi fs]) (nnf-neg `(¬ ,fi))))]
    [`(,op ,fs ...)
     `(,op ,@(map nnf-neg fs))]
    [_ f]))

; Assuming that f is in NNF, distributes ⊗ over ⊕,
; where ⊗, ⊕ ∈ { ∧, ∨ }.
(define (distribute ⊗ ⊕ f)
  (match f
    [`(,(== ⊗) ,gs ... (,(== ⊕) ,fs ...) ,hs ...)
     (distribute ⊗ ⊕
      `(,⊕ ,@(for/list ([fi fs]) `(,⊗ ,fi ,@gs ,@hs))))]
    [`(,(== ⊕) ,fs ...)
     `(,⊕ ,@(for/list ([fi fs]) (distribute ⊗ ⊕ fi)))]
    [_ f]))

; Assuming that f is in NNF, transforms it to flatten
; all nested subformulas of the form (∧ ... (∧ ...) ...)
; and (∨ ... (∨ ...) ...).
(define (unnest f)
  (match f
    [`(∨ ,gs ... (∨ ,fs ...) ,hs ...)
     (unnest `(∨ ,@gs ,@fs ,@hs))]
    [`(∧ ,gs ... (∧ ,fs ...) ,hs ...)
     (unnest `(∧ ,@gs ,@fs ,@hs))]
    [`(,op ,fs ...)
     `(,op ,@(map unnest fs))]
    [_ f]))

Primer-on-SAT.md

This gist contains the complete source code for the Primer on Boolean Satisfiability.

semantics.rkt

#lang racket

(provide (all-defined-out))

; We represent interpretations using immutable hashes
; and define the following operations on them: 
; * (assign x0 v0 x1 v1 ...) creates an interpretation
;   that assigns the value vi to the variable xi.
; * (lookup I xi) returns the value of the variable xi.
; * (extends I xi vi) returns a new interpretation that
;   is like I, except that it binds xi to vi.
(define assign hash)
(define lookup hash-ref)
(define extend hash-set)

; Returns true (#t) if I ⊨ f and false (#f) if I ⊭ f.
(define (evaluate f I)
  (match f
    ['⊤ true]
    ['⊥ false]
    [(? symbol? xi) (lookup I xi)]
    [`(¬ ,f1)       (not (evaluate f1 I))]
    [`(∧ ,fs ...)   (for/and ([fi fs]) (evaluate fi I))]
    [`(∨ ,fs ...)   (for/or  ([fi fs]) (evaluate fi I))]
    [`(→ ,f1 ,f2)   (or (not (evaluate f1 I)) (evaluate f2 I))]
    [`(↔ ,f1 ,f2)   (equal? (evaluate f1 I) (evaluate f2 I))]))

solve.rkt

#lang racket

(provide search-sat dpll read-cnf)

; The procedures search-sat and dpll assume that a CNF formula is
; given as a list of clauses, where each clause is a list of non-zero
; integers representing positive or negative literals.  

; If f is satisfiable, returns a model of f given as a list of
; integers (positive or negative literals). Otherwise returns false.
(define (search-sat f)
  (let search ([vars (variables f)] [I (list)])
    (if (evaluate f I)
        I
        (match vars
          [(list) #f]
          [(list v vs ...)
           (or (search vs (cons v I))
               (search vs (cons (- v) I)))]))))

; If f is satisfiable, returns a model of f given as a list of
; integers (positive or negative literals). Otherwise returns false.
(define (dpll f)
  (define g (bcp f))
  (match g
    [`((,lit) ...) lit]                         ; model
    [`(,_ ... () ,_ ...) #f]                    ; unsat
    [`((,assigned) ... (,lit ,_ ,_ ...) ,_ ...) ; search
     (let* ([undecided (drop g (length assigned))]
            [result    (or (dpll `((,lit) ,@undecided))
                           (dpll `((,(- lit)) ,@undecided)))])
       (and result `(,@assigned ,@result)))]))

; Applies BCP to f.
(define (bcp f)
  (match f
    [`(,ci ... (,lit) ,cj ...)
     `((,lit) ,@(bcp (unit-rule lit `(,@ci ,@cj))))]
    [_ f]))

; Applies the unit rule to f with respect to the given literal.
(define (unit-rule lit f)
  (define -lit (- lit))
  (for/list ([clause f] #:unless (member lit clause))
    (match clause
      [`(,li ... ,(== -lit) ,lj ...) `(,@li ,@lj)]
      [_ clause])))


; Returns the variables in a CNF formula f represented as a
; list of lists of integers.
(define (variables f)
  (remove-duplicates (map abs (flatten f))))

; Returns true iff I is a model of the CNF formula f
; represented as a list of lists of integers.
(define (evaluate f I)
  (for/and ([c f])
    (for/or ([l c] #:when (member l I)) #t)))

; Returns a list of lists representation of a CNF formula
; in the standard DIMACS format.
(define (read-cnf file)
  (call-with-input-file file
    (lambda (port)
      (filter-map
       (lambda (ln)
         (and (not (string-prefix? ln "c"))
              (not (string-prefix? ln "p"))
              (map string->number (drop-right (string-split ln) 1))))
       (port->lines port)))))

tseitin.rkt

#lang racket

(require "normal-forms.rkt")
(provide tseitin)

; Converts f to an equisatisfiable formula in CNF
; using Tseitin's encoding.
(define (tseitin f)
  (cnf (auxiliaries f)))

; Returns a conjunction of formulas of the form
; (∧ a ... (↔ ai fi) ...), where a's are fresh
; auxiliary variables, and fi's are f's subformulas,
; with nested subexpressions replaced by their
; corresponding auxiliary variables.
(define (auxiliaries f)
  (define aux (make-hash))
  (let intro ([f f])
    (and (list? f)
         (not (hash-has-key? aux f))
         (hash-set! aux f (gensym 'a))
         (for-each intro (cdr f))))
  `(∧ ,(hash-ref aux f f)
      ,@(for/list ([fi↦a (sort (hash->list aux) symbol<? #:key cdr)])
          (match-define (cons `(,op ,fs ...) a) fi↦a)
          `(↔ ,a (,op ,@(for/list ([fj fs]) (hash-ref aux fj fj)))))))

validity.rkt

#lang racket

(require "semantics.rkt")
(provide search-valid? deduce-valid?)

; Returns a duplicate-free list of variables that occur in f.
(define (variables f)
  (remove-duplicates (remove* '(⊤ ⊥ ¬ ∧ ∨ → ↔) (flatten f))))

; Returns true (#t) if f is valid and false (#f) otherwise,
; by checking that every interpretation satisfies f.
(define (search-valid? f)
  (let all-sat? ([vars (variables f)] [I (assign)])
    (match vars
      [(list)
       (evaluate f I)]
      [(list v vs ...)
       (and (all-sat? vs (extend I v false))
            (all-sat? vs (extend I v true)))])))

; Returns true (#t) if f is valid and false (#f) otherwise,
; by checking that all branches of f's proof tree are
; closed (i.e., contain a contradiction).
(define (deduce-valid? f)
  (let all-closed? ([facts `((I ⊭ ,f))])    ; assumption
    (match facts
      [`(,gs ... (I ⊨ (¬ ,f1)) ,hs ...)     ; (1)
       (all-closed? `((I ⊭ ,f1) ,@gs ,@hs))]
      [`(,gs ... (I ⊭ (¬ ,f1)) ,hs ...)     ; (2)
       (all-closed? `((I ⊨ ,f1) ,@gs ,@hs))]
      [`(,gs ... (I ⊨ (∧ ,fs ...)) ,hs ...) ; (3)
       (all-closed? `(,@(for/list ([fi fs]) `(I ⊨ ,fi)) ,@gs ,@hs))]
      [`(,gs ... (I ⊭ (∧ ,fs ...)) ,hs ...) ; (4)
       (for/and ([fi fs])
         (all-closed? `((I ⊭ ,fi) ,@gs ,@hs)))]
      [`(,gs ... (I ⊨ (∨ ,fs ...)) ,hs ...) ; (5)
       (for/and ([fi fs])
         (all-closed? `((I ⊨ ,fi) ,@gs ,@hs)))]
      [`(,gs ... (I ⊭ (∨ ,fs ...)) ,hs ...) ; (6)
       (all-closed? `(,@(for/list ([fi fs]) `(I ⊭ ,fi)) ,@gs ,@hs))]
      [`(,gs ... (I ⊨ (→ ,f1 ,f2)) ,hs ...) ; (7)
       (and (all-closed? `((I ⊭ ,f1) ,@gs ,@hs))
            (all-closed? `((I ⊨ ,f2) ,@gs ,@hs)))]
      [`(,gs ... (I ⊭ (→ ,f1 ,f2)) ,hs ...) ; (8)
       (all-closed? `((I ⊨ ,f1) (I ⊭ ,f2) ,@gs ,@hs))]
      [`(,gs ... (I ⊨ (↔ ,f1 ,f2)) ,hs ...) ; (9)
       (and (all-closed? `((I ⊨ (∧ ,f1 ,f2)) ,@gs ,@hs))
            (all-closed? `((I ⊭ (∨ ,f1 ,f2)) ,@gs ,@hs)))]
      [`(,gs ... (I ⊭ (↔ ,f1 ,f2)) ,hs ...) ; (10)
       (and (all-closed? `((I ⊨ (∧ ,f1 (¬ ,f2))) ,@gs ,@hs))
            (all-closed? `((I ⊨ (∧ (¬ ,f1) ,f2)) ,@gs ,@hs)))]
      [(or `(,_ ... (I ⊨ ,fi) ,_ ... (I ⊭ ,fi) ,_ ...)
           `(,_ ... (I ⊭ ,fi) ,_ ... (I ⊨ ,fi) ,_ ...))
       (printf "Contradiction on ~a: ~a\n" fi facts)
       #t]
      [_
       (printf "Open branch: ~a\n" facts)
       #f])))