TAOCP 7.2.2.2にあるSATソルバのうち, 今回はAlgorithm 7222Bの話である.
これも結構難しかった. 演習問題128の解答の(7)の式の初期値が頼りであった.
Algorithm Aに較べると, F, B, C, SIZEの配列はなくなり, 代わりにWとLINKが新たに出来た.
SATの問題では, リテラルは節のいろいろな位置に現れるが, このアルゴリズムでは, 節の先頭に現れるものだけについて初期値に設定する. Wはそれぞれのリテラルについて, 最初に現れた節の番号を示す. どの先頭にも現れなければ, 終という意味で0を入れる.
同じリテラルが複数の節の先頭に現れた時は, 続きをLINKで示す. 具体的には下の例を見てほしい.
7.2.2.2の初めの方にSimple Exampleというのがある. 8ビットのx
1...x
8で3個の0の間隔が等しくなく, 3個の1の間隔も等しくないものを探せというのである.
すぐ下に9ビットの場合のSATの式があるから, それの8ビット版を書けばよいわけで, 実装に適した私流の記法では
1+2+3+,2+3+4+,3+4+5+,4+5+6+,5+6+7+,6+7+8+,
1+3+5+,2+4+6+,3+5+7+,4+6+8+,
1+4+7+,2+5+8+,
1-2-3-,2-3-4-,3-4-5-,4-5-6-,5-6-7-,6-7-8-,
1-3-5-,2-4-6-,3-5-7-,4-6-8-,
1-4-7-,2-5-8-,
つまり8変数, 24節になる. (n=8, m=24)
これをリテラルの内部表現にすると
(define n 8)
(define sat '
((2 4 6) (4 6 8) (6 8 10) (8 10 12) (10 12 14) (12 14 16)
(2 6 10) (4 8 12) (6 10 14) (8 12 16) (2 8 14) (4 10 16)
(3 5 7) (5 7 9) (7 9 11) (9 11 13) (11 13 15) (13 15 17)
(3 7 11) (5 9 13) (7 11 15) (9 13 17) (3 9 15) (5 11 17)))
(define m (length sat)) => 24
配列Lはこれをreverseし, appendしたものである.
先頭の節を1番として, 2から17までのリテラルがどの節の先頭に現れるかをみると (listは0から始まるのでダミーの0をconsしてある)
(define s (cons 0 (map car sat)))
=>
(0 2 4 6 8 10 12 2 4 6 8 2 4 3 5 7 9 11 13 3 5 7 9 3 5)
リテラル2は1番の節に, 4は3番の節に現れる. リテラル l が現れる節番号のリストを l 番目にもつリストzを作る.
(define z (map (lambda (x) '()) (a2b 0 (+ (* n 2) 2))))
z => (() () () () () () () () () () () () () () () () () ())
(for-each (lambda (x y)
(list-set! z x (cons y (list-ref z x)))) s (a2b 0 (+ m 1)))
z=>
((0) () (11 7 1) (23 19 13) (12 8 2) (24 20 14) (9 3) (21 15)
(10 4) (22 16) (5) (17) (6) (18) () () () ())
リテラル2は1,7,11の節に, リテラル3は13,19,23の節に現れるということだ. これからWとLINKを作る.
(define ws (map (lambda (x) 0) (a2b 0 (+ (* 2 n) 2))))
(for-each (lambda (x y)
(if (not (null? x)) (list-set! ws y (car (reverse x)))))
z (a2b 0 (+ (* 2 n) 2)))
ws => (0 0 1 13 2 14 3 15 4 16 5 17 6 18 0 0 0 0)
(define link (map (lambda (x) 0) (a2b 0 (+ m 1))))
(for-each (lambda (x) (let ((t 0))
(map (lambda (y) (list-set! link y t) (set! t y)) x))) z)
link =>
(0 7 8 9 10 0 0 11 12 0 0 0 0 19 20 21 22 0 0 23 24 0 0 0 0)
この解は00110011, 01011010,01100110,10011001,10100101,11001100だが, このアルゴリズムは最初の解(00110011)しか返さない.
(define (algorithm7222b)
(define (and1 n) (if (even? n) 0 1))
;1とのandをとる
(define (xor1 n) ((if (even? n) + -) n 1))
;1とのxorをとる. リテラルの正負を反転する
(define (rsh1 n) (fix:lsh n -1))
;1ビット右シフトする
(define (? b) (if b 1 0))
;iverson notation [b]=b?1:0
;simple example
(define n 8) (define m 24)
(define sat '
((2 4 6) (4 6 8) (6 8 10) (8 10 12) (10 12 14) (12 14 16)
(2 6 10) (4 8 12) (6 10 14) (8 12 16) (2 8 14) (4 10 16)
(3 5 7) (5 7 9) (7 9 11) (9 11 13) (11 13 15) (13 15 17)
(3 7 11) (5 9 13) (7 11 15) (9 13 17) (3 9 15) (5 11 17)))
(define ls (apply append (reverse sat)))
(define ws '(0 0 1 13 2 14 3 15 4 16 5 17 6 18 0 0 0 0))
(define link '(0 7 8 9 10 0 0 11 12 0 0 0 0 19 20 21 22 0 0
23 24 0 0 0 0))
(define start '(72 69 66 63 60 57 54 51 48 45 42 39 36 33 30
27 24 21 18 15 12 9 6 3 0))
(define ms '(0 0 0 0 0 0 0 0 0))
(define d 0) (define j 0) (define i 0) (define i1 0)
(define j1 0) (define k 0) (define l 0) (define l1 0)
(call-with-current-continuation
(lambda (exit)
(define (b1) (set! d 1) (b2))
(define (b2)
(if (> d n) (begin (do ((d 1 (+ d 1))) ((> d n))
(display (xor1 (and1 (list-ref ms d))))) (exit 'ok))
(begin (list-set! ms d (? (or (= (list-ref ws (* 2 d)) 0)
(not (= (list-ref ws (+ (* 2 d) 1)) 0)))))
(set! l (+ (* 2 d) (list-ref ms d)))
(b3))))
(define (b3kloop)
(cond ((= k i1) (list-set! ws (xor1 l) j) (b5))
((< k i1)
(set! l1 (list-ref ls k))
(if (or (> (rsh1 l1) d)
(even? (+ l1 (list-ref ms (rsh1 l1)))))
(begin
(list-set! ls i l1)
(list-set! ls k (xor1 l))
(list-set! link j (list-ref ws l1))
(list-set! ws l1 j)
(set! j j1))
(begin (set! k (+ k 1)) (b3kloop))))))
(define (b3jloop)
(if (not (= j 0)) (begin
(set! i (list-ref start j))
(set! i1 (list-ref start (- j 1)))
(set! j1 (list-ref link j))
(set! k (+ i 1))
(b3kloop)
(b3jloop))))
(define (b3)
(set! j (list-ref ws (xor1 l)))
(b3jloop)
(b4))
(define (b4)
(list-set! ws (xor1 l) 0)
(set! d (+ d 1))
(b2))
(define (b5)
(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))))
(b3))
(b6)))
(define (b6)
(if (= d 1) (exit "unsatisfiable")
(begin (set! d (- d 1)) (b5))))
(b1)))
(algorithm7222b) => 00110011
他の実行例については次回にでも.
