
ここにあります.
PがO'を中心とする円上を移動すると, Qは直線上を移動する.
(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で, 解はx1=0, x2=1, x3=0, x4=1 である.
(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にあるのと同様な出力が得られた. まぁこの実装は間違ってはいないようだ.
(define (neg l) (let* ((s (symbol->string l)) (w (- (string-length s) 1))) (string-set! s w (integer->char (- 88 (char->integer (string-ref s w))))) (string->symbol s)))つまりリテラル
(char->integer #\+) => 43 (char->integer #\-) => 45だからその和の88から引くと
(define (lit v s) (string->symbol (string-append ((if (number? v) number->string symbol->string) v) (symbol->string s)))) (lit 'x '+) => x+ (lit 'x '-) => x- (lit 2 '+) => 2+ (lit 2 '-) => 2-TAOCPにあるSATソルバの基本的なアルゴリズムB(F)(7222-56)は次のようだ.
(define (b f vs) (define (lit v s) (string->symbol (string-append ((if (number? v) number->string symbol->string) v) (symbol->string s)))) (let ((a '())) (define (b1 f ls vs) (display (list 'b1 f ls vs )) (newline) (cond ((member '() f) #f) ((= (length (nub f)) 1) (set! a (cons (cons (caar f) ls) a))) (else (let ((l (lit (car vs) '+))) (b1 (apb f l) (cons l ls) (cdr vs))) (let ((l (lit (car vs) '-))) (b1 (apb f l) (cons l ls) (cdr vs)))))) (b1 f '() vs) a))引数の
(b '((1+ 2-) (2+ 3+) (1- 3-) (1- 2- 3+)) '(1 2 3))と呼び出す. 内部手続きb1が途中経過を示すので, 出力は
(b1 ((2+ 3+) (3-) (2- 3+)) (1+) (2 3)) (b1 ((3-) (3+)) (2+ 1+) (3)) (b1 (()) (3+ 2+ 1+) ()) (b1 (()) (3- 2+ 1+) ()) (b1 ((3+) (3-)) (2- 1+) (3)) (b1 (()) (3+ 2- 1+) ()) (b1 (()) (3- 2- 1+) ()) (b1 ((2-) (2+ 3+)) (1-) (2 3)) (b1 (()) (2+ 1-) (3)) (b1 ((3+)) (2- 1-) (3)) => ((3+ 2- 1-))トレースの最初の行は, 後ろから見て残りの変数は2と3, リテラルは1+. 従って