「充足可能性問題(3-SAT)を解く乱択アルゴリズム」 by Egison

egison

Last updated at 2014-12-31Posted at 2014-12-31

前置き

元ネタは、結城浩氏著の「数学ガール乱択アルゴリズム」。
新しい言語を覚えるとき、慣れるために「充足可能性問題（3-SAT）を解く乱択アルゴリズム」（p.353）を実装するという癖をつけていました¹。

ということで、久々に。個人的に研究中の Egison ( http://www.egison.org/ ) で試してみました。

開発環境・動作確認環境

Mac OSX 10.9.5²
Egison 3.3.15/3.5.1³⁴

コード

例1：関数型プログラミングを強く意識したコード

まずは関数型プログラミングとしての実装例。Egison が標準で用意してくれている関数は素直になるべく利用するようにしました。

rw3sat_f.egi

;; rw3sat_f.egi

(define $sample
  (lambda [$xs]
    (nth (pure-rand 1 (length xs)) xs)))

(define $clause.apply
  (lambda [$c $a]
    (let {[$p (lambda [$i $b] (if b a_i (not a_i)))]}
      (any p c))))

(define $w4                                                 ; W4
  (lambda [$n]
    (generate-array [$i] n (sample {#t #f}))))

(define $random-walk-3-sat
  (lambda [$f $n $R]
    (letrec {[$rw3sat.loop
      (match-lambda [integer integer something]
        {[[,0 ,0  _] "おそらく充足不可能である"]            ; W17
         [[,0 $r  _] (rw3sat.loop (* n 3) (- r 1) (w4 n))]  ; W5,W6,W15,W16
         [[$k $r $a] 
          (if (all (clause.apply $ a) f)                    ; W7
              "充足可能である"                              ; W8
              (letrec
                {[$c  (sample (filter (lambda [$c'] (not (clause.apply c' a))) f))] ; W10
                 [$x  (match (sample c) [integer bool] {[[$i _] i]})]               ; W11
                 [$a' (generate-array [$i] n (if (eq? i x) (not a_i) a_i))]}        ; W12
                  (rw3sat.loop (- k 1) r a')))]})]}                                 ; W13,W14
      (rw3sat.loop (* n 3) R (w4 n)))))                                             ; W2,W3

(define $p1 {[1 #t] [2 #t] [3 #t]})
(define $p2 {[4 #t] [2 #t] [3 #f]})
(define $p3 {[1 #f] [4 #t] [3 #t]})
(define $p4 {[1 #f] [4 #f] [2 #t]})
(define $p5 {[4 #f] [2 #f] [3 #t]})
(define $p6 {[1 #f] [2 #f] [3 #f]})
(define $p7 {[1 #t] [4 #f] [3 #f]})
(define $p8 {[1 #t] [4 #t] [2 #f]})

(define $f {p1 p2 p3 p4 p5 p6 p7 p8})
;(define $f {p1 p2 p3 p4 p5 p6 p8})

(define $main
  (lambda [$args]
    (print (random-walk-3-sat f 4 3))))

簡単に解説。

3-5行目。nth は Collection の n番目の要素（1-origin）を取り出す関数。length は Collection の長さを算出する関数。
pure-rand は指定した範囲の乱数を返す関数（副作用を伴う関数）。
これらを組み合わせることで「Collection の要素を1つ乱択する関数 sample」を実装。
7-10行目。clause（変数（正確には literal）のいくつかの論理和）に実際の変数を割り当てて真偽値を算出する関数の定義。
let、if は expression、not、any は標準ライブラリ関数。
なお第2引数 $a は Array⁵ を想定。
12-14行目。書籍に載っている仮想コードの W4 行に相当する処理、true / false いずれかの値からなる「n 変数の割当を乱択」する関数。
なお #t/#f は Egison の bool値リテラル。
16-30行目。3-SAT の本体。Egison には（手続き型言語で言うところの）ループ制御は存在しないので、再帰関数を定義してパラメータの値でループ処理を実現。関数型プログラミングの定石ですね。
中で行われている処理も、対応する仮想コードの行番号を記述しておいたので書籍をお持ちの方はそれと対比して見ていただけると良いと思います。
32-39行目。各 clause の定義。
なお literal は、「『integer値（変数のインデックス）』と『bool値（#tならそのまま、#fなら真偽値反転）』からなる tuple」で表現。
41行目。充足可能かどうかを評価する対象の 3-CNF を（clause のリストとして）定義。
44-47行目。実行、結果表示。

ここまで書けば、あとは書籍を見たり、他の方や私が過去に書いた他言語版の 3-SAT 実装例を見ていただければ、だいたいどんなことしてるのかはお分かりいただけるかと思います。
1つ、掘り下げて説明が必要そうだと思うのは、19行目の match-lambda expression ですかね。
他処にも出てくる lambda expression は、単純な「関数（lambda）定義」。
他に、27行目に match expression というものが出てきますが、こちらは「パターンマッチ定義」。
これを組み合わせたもので、引数をパターンマッチさせてその結果を返す関数を定義しています。Haskell でも似たような書き方ができますよね。

例2：パターンマッチ指向で（再）構築したコード

Egison はなんと言っても「パターンマッチ指向」。expression や primitive関数以外の標準添付関数も、（primitive関数や）パターンマッチの組合せで定義されています。
ということで、パターンマッチで書けるところは全てパターンマッチで、また関数も primitive関数（≒組込関数）とそのソースコード内で定義した関数のみ使用しそれ以外の標準添付関数を使用しないようにして書き直してみました。意外と疲れた。

rw3sat.egi

;; rw3sat.egi

(define $reject
  (lambda [$pred $xs]
    (match xs (list something)
      {[<nil> {}]
       [<cons ?pred $ys> (reject pred ys)]
       [<cons $y $ys> {y @(reject pred ys)}]})))

(define $sample
  (lambda [$xs] 
    (match xs (list something)
      {[(loop $i [1 $n] <cons $x_i ...> <nil>)
        x_(io (rand 1 n))]})))

(define $literal [integer bool])

(define $clause (list literal))
(define $clause.apply
  (lambda [$c $a]
    (let {[$p (lambda [$i $b] (eq? b a_i))]}
      (match c clause
        {[<nil> #f]
         [<cons ?p _> #t]
         [<cons _ $cs> (clause.apply cs a)]}))))

(define $CNF (list clause))
(define $CNF.apply
  (lambda [$f $a]
    (match f CNF
      {[<nil> #t]
       [<cons ?(clause.apply $ a) $fs> (CNF.apply fs a)]
       [_ #f]})))

(define $w4                                                 ; W4
  (lambda [$n]
    (generate-array [$i] n (sample {#t #f}))))

(define $random-walk-3-sat
  (lambda [$f $n $R]
    (letrec
      {[$rw3sat.w6                                          ; W6-W14
        (lambda [$a]
          (letrec
            {[$c  (sample (reject (clause.apply $ a) f))]   ; W10
             [$x  (match (sample c) literal {[[$i _] i]})]  ; W11
             [$a' (generate-array [$i] n                    ; W12 
               (if (eq? i x) (eq? #f a_i) a_i))]}
            {(CNF.apply f a) @(rw3sat.w6 a')}))]
       [$rw3sat.w3                                          ; W3-W16
        (lambda [] {(rw3sat.w6 (w4 n)) @(rw3sat.w3)})]}
      (match (rw3sat.w3) (list (list bool))
        {[^(loop $k [1 (* 3 n)] <cons (loop $r [1 R] <cons ,#f ...> _) ...> _)  ; W2,W3,W5,W6,W7,W13,W15
            "充足可能である"]                               ; W8
         [_ "おそらく充足不可能である"]}))))                ; W17

(define $p1 {[1 #t] [2 #t] [3 #t]})
(define $p2 {[4 #t] [2 #t] [3 #f]})
(define $p3 {[1 #f] [4 #t] [3 #t]})
(define $p4 {[1 #f] [4 #f] [2 #t]})
(define $p5 {[4 #f] [2 #f] [3 #t]})
(define $p6 {[1 #f] [2 #f] [3 #f]})
(define $p7 {[1 #t] [4 #f] [3 #f]})
(define $p8 {[1 #t] [4 #t] [2 #f]})

(define $f {p1 p2 p3 p4 p5 p6 p7 p8})
; (define $f {p1 p2 p3 p4 p5 p6 p8})

(define $main
  (lambda [$args]
    (print (random-walk-3-sat f 4 3))))

簡単に解説。

3-8行目。例1で filter+not で実現していた処理をまとめて実施する reject関数をパターンマッチを利用して独自に定義。
第2引数で指定した Collection の要素のうち、第1引数 pred で評価した結果が #t のものを取り除いた Collection を返す関数です。
10-14行目。例1の sample 関数のリプレース。パターンマッチで loop パターンというものを利用することで、Collection に含まれる各要素とそのインデックス、および要素数を取り出し、要素を1つを乱択。pure-rand 関数は (io (rand s e)) と定義されている（io は expression、rand は primitive関数）のでそのようにそのまま置換。
16行目。literal という matcher の定義（とりあえず typedef による型の（別名）定義のようなものだと思っていただければ）。
integer と bool からなる tuple を literal と定義しています。
18行目。clause という matcher の定義（同上）。
literal のリストを clause と定義しています。
19-25行目。例1の clause.apply 関数（7-10行目）のリプレース。主に any 関数を match expression を利用して置き換えただけ。パターンで割と特殊なことをしてますが詳解は余力があれば(^-^;。
27行目。CNF という matcher の定義。
clause のリストを CNF と定義しています。
28-33行目。例1の23行目にあった (all (clause.apply $ a) f) のリプレース。主に all 関数を match expression を利用して置換。
35-37行目。例1の 12-14行目まま。
39-55行目。3-SAT の本体。内容がらっと変わってます。
例1では「ループの代わりに再帰関数を定義してループを実現」していましたが、今回は再帰関数は「次々に新しいパラメータで評価する仕組み」を定義して、その評価結果を順次受け取れるリストを返すようになっています。ただし遅延評価なので、実際にその値を取り出そうとするときに初めて実際の評価が行われるので、見た目無限ループのようですが必要な箇所のみ処理が行われるので問題ありません。
それを loop パターンを利用して「規定回数 #f が続くかどうか」を見ています。途中で中断したら充足解が見つかったと言うことなので "充足可能である" を返し、そうでなければ "おそらく充足不可能である" を返す。という仕組みです。
57行目以降は、例1の32行目以降と同一です。

やはり仮想コードの対応する行番号をコメントで付加してありますので、書籍や他の実装例と照らし合わせてみてください。
7行目・24行目・32行目の Predicate パターン（?の後に bool値を返す関数を指定して、「結果が #t である⇔マッチする」というパターン指定）や、13行目と53行目の loop パターンが肝ですね。これらが使いこなせればかなり多くのことができそうな感じです。
特に loop パターン。色々な書き方ができて、文字通り（手続き型言語の）ループ処理のリプレースになりそうな可能性を持っていそうなので、もっと探ってみたいと思います。

参考

私が過去に実装した他言語での実装例

Ruby版: https://gist.github.com/960956
JavaScript版: https://gist.github.com/966408
CoffeScript版: https://gist.github.com/1000913
R版: https://gist.github.com/2811277
Python版: https://gist.github.com/2818831
Haxe版: https://gist.github.com/4148331

その他の実装例・関連記事

Egison の技術情報

Basics of Syntax and Semantics
Basics of Patterns : Syntax and Semantics
Egison Cheat Sheet
その他 egison.org 内参照。

http://antimon2.hatenablog.jp/entry/2012/05/27/214406, http://antimon2.hatenablog.jp/entry/2012/12/09/230230 ↩
そいやまだYosemiteにアップグレードしてなかった。 ↩
公式サイトのパッケージインストーラを使用せず、ghc + cabal-install で共存インストールしています。 ↩
紹介しているプログラムは、Egison v3.5.0 では動作しません。v3.5.1（以降）にアップデートしましょう。 ↩
Egison には複数の集合型があり、Collection（一般的なリスト）とArray（所謂配列）は別物です。（がんばれば）互いに変換することもできますが扱い方は全く異なります。 ↩

You get articles that match your needs
You can efficiently read back useful information
You can use dark theme

What you can do with signing up