SATソルバ

TAOCP 7.2.2.2にはSATソルバのアルゴリズムがいくつか登場する.

今回はそのうちAlgorithm 7222Aを話題としたい. ただこのアルゴリズムの背景を初めから述べるのは大変なので, TAOCPのその辺を読んである読者を対象に書くことで勘弁して貰いたい.

TAOCPのアルゴリズムは自然言語であるだけでなく, 非常に簡潔な記述なので, 前後の説明をよく理解していないと, なんのことだか分からないことが多い. そういう場合にSchemeで記述したこのブログのプログラムは理解の助けになのではないか. とにかく実際に動くプログラムとして存在するから だ.

TAOCPにも, あるデータを例としての説明はある. 7.2.2.2-6と7の式



で, (6)は充足不能, (7)は充足可能な例である.

まず(7)について, 次のようなデータを用意する.



配列L, F, B, Cは添字が0から30で, Lには(7)の節が置いてある. L(10)から始まる9,7,3は(7)の最後の節の3-,4-,1-を4,3,1の順にし, 正のリテラルは変数番号を2倍し, 負のリテラルは2倍して1足したものなので, 9,7,3になっている. Cの対応する場所の7は, 7番目の節を示す.

L(13)以降も同様である.

FとBは両方向リンクで, F(2)つまりリテラル1+が現れる場所はL(30)であり, F(30)=24は次がL(24)であることを示す. Bは逆向きの情報である.

リンク構造なのは, リテラルや節を削除/挿入するのに便利なためである.

C(2)からC(9)まではそれぞれのリテラルが何個あるかを示す.

それらの下のSTARTは, それぞれの節の先頭の位置; SIZEは節にあるリテラルの個数である.

Schemeで実装したプログラムは以下のようだ.

(define (algorithm7222a)
(define (and1 n) (if (even? n) 0 1))
;1とのandをとる
(define (xor1 n) ((if (even? n) + -) n 1))
;1とのxorをとる. リテラルの正負を反転する
(define (? b) (if b 1 0))
;iverson notation [b]=b?1:0

(define n 4) (define m 7)
(define ls '(0 0 0 0 0 0 0 0 0 0 9 7 3 8 7 5 6 5 3 8 4 3
 8 6 2 9 6 4 7 4 2))
(define fs '(0 0 30 21 29 17 26 28 22 25 9 7 3 8 11 5 6 15 12
 13 4 18 19 16 2 10 23 20 14 27 24))
(define bs '(0 0 24 12 20 15 16 11 13 10 25 14 18 19 28 17 23
 5 21 22 27 3 8 26 30 9 6 29 7 4 2))
(define cs '(0 0 2 3 3 2 3 3 3 2 7 7 7 6 6 6 5 5 5 4 4 4
 3 3 3 2 2 2 1 1 1))
(define size '(0 3 3 3 3 3 3 3))
(define start '(0 28 25 22 19 16 13 10))

(define ms (map (lambda (x) 0) (a2b 0 (+ n 1))))

(define l 0) (define a 0) (define d 0) (define p 0) 
(define i 0) (define j 0) (define q 0) (define r 0) 
(define s 0)

(call-with-current-continuation
 (lambda (exit)

(define (a1)
 (set! a m) (set! d 1)
 (a2))
(define (a2)
 (set! l (* 2 d))
 (if (<= (list-ref cs l) (list-ref cs (+ l 1)))
  (set! l (+ l 1)))
 (list-set! ms d (+ (and1 l) 
  (* 4 (? (= (list-ref cs (xor1 l)) 0)))))
 (newline) (display (list 'ms (take (+ d 1) ms)))
 (if (= (list-ref cs l) a) (begin (newline)
  (do ((i 1 (+ i 1))) ((> i n)) 
   (display (and1 (xor1 (list-ref ms i)))))
  (exit 'satisfiable)))
 (a3))

(define (a3back)
 (if (>= p (+ n n 2)) (begin
  (set! j (list-ref cs p))
  (set! i (list-ref size j))
  (list-set! size j (+ i 1))
  (set! p (list-ref bs p))
  (a3back)) (a5)))

(define (a3loop)
 (if (>= p (+ n n 2)) (begin
 (set! j (list-ref cs p))
 (set! i (list-ref size j))
 (if (> i 1) (begin
   (list-set! size j (- i 1)) 
   (set! p (list-ref fs p)) (a3loop))
  (begin (set! p (list-ref bs p)) (a3back))))
(a4)))

(define (a3)
 (set! p (list-ref fs (xor1 l)))
 (a3loop))

(define (a4loop)
 (if (>= p (+ n n 2)) (begin
  (set! j (list-ref cs p))
  (set! i (list-ref start j))
  (set! p (list-ref fs p)) 
  (do ((s i (+ s 1))) ((= s (+ i (list-ref size j) -1)))
   (set! q (list-ref fs s))
   (set! r (list-ref bs s))
   (list-set! bs q r)
   (list-set! fs r q)
   (list-set! cs (list-ref ls s)
    (- (list-ref cs (list-ref ls s)) 1)))
  (a4loop))))

(define (a4)
 (set! p (list-ref fs l))
 (a4loop)
 (set! a (- a (list-ref cs l))) (set! d (+ d 1)) 
 (a2))

(define (a5)
 (if (< (list-ref ms d) 2) (begin 
  (list-set! ms d (- 3 (list-ref ms d)))
  (set! l (+ (* 2 d) (and1 (list-ref ms d)))) (a3))
 (a6)))

(define (a6)
 (if (= d 1) (exit "unsatisfiable")
  (begin (set! d (- d 1))
   (set! l (+ (* 2 d) (and1 (list-ref ms d)))) (a7))))

(define (a7loop)
 (if (>= p (+ n n 2)) (begin
  (set! j (list-ref cs p))
  (set! i (list-ref start j))
  (set! p (list-ref bs p))
  (do ((s i (+ s 1))) ((= s (+ i (list-ref size j) -1)))
   (set! q (list-ref fs s))
   (set! r (list-ref bs s))
   (list-set! bs q s)
   (list-set! fs r s)
   (list-set! cs (list-ref ls s)
    (+ (list-ref cs (list-ref ls s)) 1)))
 (a7loop))))

(define (a7)
 (set! a (+ a (list-ref cs l)))
 (set! p (list-ref bs l))
 (a7loop)
 (a8))

(define (a8loop)
 (if (>= p (+ n n 2)) (begin
  (set! j (list-ref cs p))
  (set! i (list-ref size j))
  (list-set! size j (+ i 1))
  (set! p (list-ref fs p))
  (a8loop))))

(define (a8)
 (set! p (list-ref fs (xor1 l)))
 (a8loop)
 (a5))

(a1)))
)
(algorithm7222a)

途中, ステップA2で動作状況を示すmsを印字しながらの実行結果は

(ms (0 1))
(ms (0 1 0))
(ms (0 1 0 1))
(ms (0 1 0 1 4))
0101
;... done
;Value: satisfiable

で, 解はx₁=0, x₂=1, x₃=0, x₄=1 である.

TAOCPには(6)の実行中のmsの値も掲載してあるから

(define n 4) (define m 8)
(define ls '(0 0 0 0 0 0 0 0 0 0 9 5 2 9 7 3 8 7 5 6 5 3 8 4
 3 8 6 2 9 6 4 7 4 2))
(define fs '(0 0 33 24 32 20 29 31 25 28 9 5 2 10 7 3 8 14 11
 6 18 15 16 4 21 22 19 12 13 26 23 17 30 27))
(define bs '(0 0 12 15 23 11 19 14 16 10 13 18 27 28 17 21 22
 31 20 26 5 24 25 30 3 8 29 33 9 6 32 7 4 2))
(define cs '(0 0 3 3 3 3 3 3 3 3 8 8 8 7 7 7 6 6 6 5 5 5 4 4
 4 3 3 3 2 2 2 1 1 1))
(define size '(0 3 3 3 3 3 3 3 3))
(define start '(0 31 28 25 22 19 16 13 10))

として(6)もやってみると

(ms (0 1))
(ms (0 1 1))
(ms (0 1 1 0))
(ms (0 1 1 3 1))
(ms (0 1 2 1))
(ms (0 1 2 1 1))
(ms (0 1 2 2 1))
(ms (0 2 1))
(ms (0 2 1 1))
(ms (0 2 1 1 1))
(ms (0 2 1 2 1))
(ms (0 2 2 1))
(ms (0 2 2 2 1))
;... done
;Value 11: "unsatisfiable"

のように, TAOCPにあるのと同様な出力が得られた. まぁこの実装は間違ってはいないようだ.