『数学ガール／乱択アルゴリズム』の3-SATのくだりを１ミリも知らないまま乱択アルゴリズムをSqueakで変態的に書いてみる

上のページを参考に、おそらくはこんなようなことなんじゃないかなぁと想像しつつ書いてみました。Squeak4.1J、Squeak4.2J のワークスペースなどにコピペして実行できます（alt-v でペースト後、あらためて alt-a で選択してから alt-p）。

| N 強 正 美 優 節群 |

#(く しく くなく しくなく 反転).
(ValueHolder selectors includes: #く) ifFalse: [ValueHolder
   compile: 'く ^contents';
   compile: 'しく ^self く';
   compile: 'くなく ^contents not';
   compile: 'しくなく ^self くなく';
   compile: '反転 contents := contents not';
   compile: 'printOn: stream contents printOn: stream'].

N := 4.
強 := ValueHolder new.
正 := ValueHolder new.
美 := ValueHolder new.
優 := ValueHolder new.

節群 := {
   [ 強 く | 正 しく | 美 しく ].
   [ 優 しく | 正 しく | 美 しくなく ].
   [ 強 くなく | 優 しく | 美 しく ].
   [ 強 くなく | 優 しくなく | 正 しく ].
   [ 優 しくなく | 正 しくなく | 美 しく ].
   [ 強 くなく | 正 しくなく | 美 しくなく ].
   [ 強 く | 優 しくなく | 美 しくなく ].
   [ 強 く | 優 しく | 正 しくなく ]
}.

10 timesRepeat: [
   {強. 正. 美. 優} do: [:命題 | 命題 contents: #(true false) atRandom].

   N*3 timesRepeat: [
      | 失敗節 |
      失敗節 := 節群 detect: [:節 | 節 value not] ifNone: [
         ^'充足可能である'->thisContext tempsAndValues
      ].
      (失敗節 at: 失敗節 size atRandom) 反転
   ].
].

^'おそらく充足不可能である'

ValueHolder は contents というインスタンス変数を持つ値保持用のオブジェクトを定義するクラスです。これに #く、#しく、#くなく、#しくなくといった contents のアクセッサーを定義。さらに、#反転というメソッドで contents の中身を真偽値反転できるようにするための手続きが冒頭のコンパイル式群です。この小細工により、

強 く

といった命題の表現が可能になります。変数「強」に ValueHolder のインスタンスを代入しておけば、それに対してメッセージ「く」を送ることを介して ValueHoler に定義したメソッド #くがコールされ、contents が得られる―といった感じの Smalltalk 式として機能します。

なお、このカラクリを無しにすると、同様の処理はこんなふうに書き直せます。

| N A1 A2 A3 A4 節群 |

N := 4.
A1 := ValueHolder new.
A2 := ValueHolder new.
A3 := ValueHolder new.
A4 := ValueHolder new.

節群 := {
   [ A1 contents | A2 contents | A3 contents ].
   [ A4 contents | A2 contents | A3 contents not ].
   [ A1 contents not | A4 contents | A3 contents ].
   [ A1 contents not | A4 contents not | A2 contents ].
   [ A4 contents not | A2 contents not | A3 contents ].
   [ A1 contents not | A2 contents not | A3 contents not ].
   [ A1 contents | A4 contents not | A3 contents not ].
   [ A1 contents | A4 contents | A2 contents not ]
}.

10 timesRepeat: [
   {A1. A2. A3. A4} do: [:命題 | 命題 contents: #(true false) atRandom].

   N*3 timesRepeat: [
      | 失敗節 乱択命題 |
      失敗節 := 節群 detect: [:節 | 節 value not] ifNone: [
         ^'充足可能である'->
            (#(A1 A2 A3 A4) with: {A1. A2. A3. A4}collect: [:命題名 :値 | 命題名->値])
      ].
      乱択命題 := 失敗節 at: 失敗節 size atRandom.
      乱択命題 contents: 乱択命題 contents not
   ].
].

^'おそらく充足不可能である'

DSLっぽい書き方ができなくなってしまう反面、実際の処理の内容はいくぶんかイメージしやすくなったかと思います。

Smalltalk で [...] は「ブロック」と呼ばれる無名関数の定義です。Ruby のブロックと使い方は似ていますが、ファーストクラスであるため、オブジェクトとしての性格は Proc に近いです。value というメッセージを送ることで評価して値を得ることができます。たとえば、[3+4] value なら 7 を返します。ここではブロックを使って節を定義し、一連の節の定義を { ... } で括ることで「節群」と呼ぶ配列にまとめてあります。

配列の要素で、ブロックで表現された節の値がすべて真（true）であることを確認するだけなら、

節群 allSatisfy: [:節 | 節 value]

もしくは、

節群 noneSatisfy: [:節 | 節 value not]

と書くだけでよいのですが、今は真でない節を見つけたり、全ての節が真であったなら処理を終了しないといけないなど、いろいろとすることがあるので、#detect:ifNone: を使っています。

節群 detect: [:節 | 節 value not] ifNone: [...]

この式は節、すなわちブロック、を評価した値（value）の真偽値反転（not）が true なら、つまり、節が失敗（false）ならその節を返し、失敗する節が見つからなければ ifNone: の引数のブロックを評価して充足可能であることを返しつつ処理を終える、という作業を一気に行ないます。

なお、失敗する節が見つかった場合は、節に含まれる命題のいずれかの状態を反転します。ここがこのコードでよい子がマネをしてはいけない最も変態的な部分で、ブロックオブジェクト（クロージャー）に size というメッセージを送ると、クロージャーが保持するオブジェクト（この場合、三つの命題）の数を、また、at: index でその値が得られるたまたま生じた状況を利用して、節に含まれる ValueHolder のインスタンスが保持する真偽値を反転することをしています。

乱択命題 := 失敗節 at: 失敗節 size atRandom.
乱択命題 contents: 乱択命題 contents not

最初のコードでは、ValueHolderオブジェクトの contents を反転する #反転を ValueHolder に定義してしまいましたので、もっと簡潔に書けています。

(失敗節 at: 失敗節 size atRandom) 反転

その後、充足することなく既定回数のループを終えると「おそらく充足不可能である」と返しておしまいになります。