BrainfuckをSATへ変換する

 足し算と引き算しかしていませんが、ここまでくれば超カンタンです。足し算・引き算と同じことを繰り返せばOKなのですから。(というか夜3時なのでいよいよ時間的余裕がなくなってきた)

5秒でおさらいBrainfuck

 Brainfuckはたった8文字だけで記述するプログラミング言語です。

 Brainfuckにはメモリの概念と今現在どこを指しているかのポインタの概念、さら入力と出力があり、次の8文字(命令)を使ってそのメモリとポインタを操作します。

 Wikipediaから引用

  • ">" ポインタをインクリメントする。
    • ポインタをptrとすると、C言語の「ptr++;」に相当する。
  • "<" ポインタをデクリメントする。
    • C言語の「ptr--;」に相当。
  • "+" ポインタが指す値をインクリメントする。
    • C言語の「(*ptr)++;」に相当。
  • "-" ポインタが指す値をデクリメントする。
    • C言語の「(*ptr)--;」に相当。
  • "." ポインタが指す値を出力に書き出す。
    • C言語の「putchar(*ptr);」に相当。
  • "," 入力から1バイト読み込んで、ポインタが指す先に代入する。
    • C言語の「*ptr=getchar();」に相当。
  • "[" ポインタが指す値が0なら、対応する ] の直後にジャンプする。
    • C言語の「while(*ptr){」に相当。
  • "]" ポインタが指す値が0でないなら、対応する [ (の直後1)にジャンプする。
    • C言語の「}」に相当。

このプログラミング言語のhello worldは、例えば次のように書けます:

+++++++++[>++++++++>+++++++++++>+++++<<<-]>.>++.+++++++..+++.>-.
------------.<++++++++.--------.+++.------.--------.>+.

インタプリタがWeb上にいくつかあるので、遊んで見るのもよいでしょう: https://copy.sh/brainfuck/

 このBrainfuckは万能チューリングマシンに極めて近いです。…プログラムが激しく書きづらいところも含めて…。

 Brainfuckは万能チューリングマシンと実際に等価な力をもつチューリング完全な言語、つまり普通のコンピュータと計算能力的には等しい力をもつことが分かっています。

 今回は、このBrainfuckプログラムをSATの問題へと変換し、SATのソルバー上で実行しましょう!

論理変数の構成を設計する

 ここまでの準備があれば、もう簡単です。一番難しいのは、データ構造(=論理変数の構成)を設計する所でしょうか?

data Component =
    PC Time Int |
    IC Time Int |
    InTape Int Int |
    MC Time Int |
    MidTape Time Int Int |
    OC Time Int |
    OutTape Int Int |
    Tmp [Int]
  deriving (Eq,Show,Read,Ord)
  • PCはプログラムカウンタ:次にどの命令を実行するか
  • ICはインプットカウンタ:次に,で読むのは入力の何文字目か
  • OCはアウトプットカウンタ:次に.で書き込む先は何文字目か
  • MCは計算用中間テープカウンタ:ポインタの位置
    • それぞれ、最後のIntは何bit目かを表す(前Chapterと同じ)
  • InTape/MidTape/OutTape:入力・計算用中間テープ・出力テープの値
    • 最後から2つ目のIntは何バイト目か、最後のIntは何bit目かを表す

 SATにはgetcharもputcharもないので、入力は事前にバイト列として(論理式に変換して)与えた上で出力も論理変数の割当てから読み取ることになります。これがInTape/OutTape論理変数の役割です。

 InTapeとOutTape以外の論理変数にはTimeという型の値が付属しています。これは読んだ通り「時間」で、実体はIntです。

 どういう事かというと、まずSATには時間発展の機能がない事を確認しましょう。Brainfuckのプログラムは時々刻々とメモリの内容やポインタの位置が更新されていきますが、SATの論理変数は一度真偽が割当てられれば、それでおしまいです。ということは、ただひとつPC Intといった論理変数を一式作っただけではBrainfuckのプログラムの刻々と実行されていく現象を表現できないということになります。

 そこで、Brainfuckプログラムが実行されていくごとにメモリやポインタといったその実行途中の結果(計算機科学の教科書っぽくいえば、時点表示)を次の時間を表す論理変数に次々に代入していくように論理式を設計します。

 しかし、InTape(入力テープ)は最初から内容が不変ですし、OutTape(出力テープ)も一度値が書き込まれれば値はそれ以降不変ですから、こういった仕組みは不要です。InTape/OutTapeにTimeが入っていないのはこの事実を反映しています。

論理式の作成:初期値

 簡単です。Time=0の時のそれぞれの初期値を前Chapterの方法で代入する論理式を作り、すべてをAndでつなげるだけです。

 論理変数をプログラムだと見立てることが出来て、Andでつなぐ事は逐次実行(C++で言えば、a;b;c;...)に相当します。

論理式の作成:ステップ実行

 これも簡単です。まず、普通のプログラミング言語でBrainfuckインタプリタを作るにはどうすればいいかを考えます。…答え:「まずPCを読んで命令をチェックし、それぞれの命令に応じた処理へ分岐する」

 このうち、今まで出てこなかったテクニックは分岐です。これはorを使うと表現できます。

 例えばこのC++のソース:

 if(a){ b; }else{ c; }

は、それぞれを表す論理変数を使って、次のように書けます。

(a && b) || (!a && c)

 aの条件によってbかcのどちらがtrueになるか(=実行されるか)を制御することができるのがポイントです。

 実は両方ともtrueでも充足されてしまうのですが、複雑な構成になると両方ともtrueにすることはできなくなってくるので、事実上問題になりません。

論理式の作成:プログラム終了

 プログラムが最後まで実行されたら、それで実行は終わりです。このとき、実行が終わった後の時間の論理変数はすべて前の時間の論理変数をコピーしておくことにすると、後処理が楽です。

実際にやってみる

何はともあれ、実行しているところを眺めてみましょう。

まずは、軽いジョブとして2x2=4を計算します。

$ git clone git@github.com:ledyba/bf2sat.git
$ cd bf2sat
$ make init

% cabal run create simple.bf
** Brainfuck 2 SAT **
-- Setting --
  src:++[->++<]
  in: [0, 0]
  value-bits: 8
  addr-bits:4
  out-addr-bits:2
  sim-steps:18
-- Create SAT problem --
To CNF...
434666 clauses, 6233077 literals
Aliasing...
115584 uniq predicates
write to file
All done, have fun.

% minisat sat.txt ans.txt || true
...
SATISFIABLE

% cabal run decode simple.bf
** Brainfuck 2 SAT **
-- Result --
         Source:++[->++<]
          Input: [0, 0]
Estimated Input: [0, 0]
Estimated IDs:
0: ID {getPC = 0, getMem = [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], getPT = 0, getIC = 0, getOC = 0, getOut = []}
1: ID {getPC = 1, getMem = [1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], getPT = 0, getIC = 0, getOC = 0, getOut = []}
2: ID {getPC = 2, getMem = [2,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], getPT = 0, getIC = 0, getOC = 0, getOut = []}
3: ID {getPC = 3, getMem = [2,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], getPT = 0, getIC = 0, getOC = 0, getOut = []}
4: ID {getPC = 4, getMem = [1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], getPT = 0, getIC = 0, getOC = 0, getOut = []}
5: ID {getPC = 5, getMem = [1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], getPT = 1, getIC = 0, getOC = 0, getOut = []}
6: ID {getPC = 6, getMem = [1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0], getPT = 1, getIC = 0, getOC = 0, getOut = []}
7: ID {getPC = 7, getMem = [1,2,0,0,0,0,0,0,0,0,0,0,0,0,0,0], getPT = 1, getIC = 0, getOC = 0, getOut = []}
8: ID {getPC = 8, getMem = [1,2,0,0,0,0,0,0,0,0,0,0,0,0,0,0], getPT = 0, getIC = 0, getOC = 0, getOut = []}
9: ID {getPC = 3, getMem = [1,2,0,0,0,0,0,0,0,0,0,0,0,0,0,0], getPT = 0, getIC = 0, getOC = 0, getOut = []}
10: ID {getPC = 4, getMem = [0,2,0,0,0,0,0,0,0,0,0,0,0,0,0,0], getPT = 0, getIC = 0, getOC = 0, getOut = []}
11: ID {getPC = 5, getMem = [0,2,0,0,0,0,0,0,0,0,0,0,0,0,0,0], getPT = 1, getIC = 0, getOC = 0, getOut = []}
12: ID {getPC = 6, getMem = [0,3,0,0,0,0,0,0,0,0,0,0,0,0,0,0], getPT = 1, getIC = 0, getOC = 0, getOut = []}
13: ID {getPC = 7, getMem = [0,4,0,0,0,0,0,0,0,0,0,0,0,0,0,0], getPT = 1, getIC = 0, getOC = 0, getOut = []}
14: ID {getPC = 8, getMem = [0,4,0,0,0,0,0,0,0,0,0,0,0,0,0,0], getPT = 0, getIC = 0, getOC = 0, getOut = []}
15: ID {getPC = 9, getMem = [0,4,0,0,0,0,0,0,0,0,0,0,0,0,0,0], getPT = 0, getIC = 0, getOC = 0, getOut = []}
16: ID {getPC = 9, getMem = [0,4,0,0,0,0,0,0,0,0,0,0,0,0,0,0], getPT = 0, getIC = 0, getOC = 0, getOut = []}
17: ID {getPC = 9, getMem = [0,4,0,0,0,0,0,0,0,0,0,0,0,0,0,0], getPT = 0, getIC = 0, getOC = 0, getOut = []}
All done, have fun.

これだけのプログラムでも434666節あるので、なかなか大変です。コンピュータサイエンスの教科書にならどこにでも書いてある理論的な結果ですが、なかなか現実にやろうとすると大変だと言えるのではないでしょうか…。

 最後にズラっと並んでいるのが、「時間ごとの時点表示」です。メモリの中身がどんどん書き換わって、最後に2バイト目に4という計算結果が格納されていることがわかります。

SATはチューリング完全ではない

 さて、プログラムの実行ステップごとに論理変数を増殖させると言いましたが、どこまで増やせばよいのでしょうか?100ステップ?100000ステップ?100000000000000ステップ?

 答え:無限ステップ

 なぜなら、brainfuckは無限ループするプログラムを簡単に書けるからです。ほら: +[]

 となると、こういったbrainfuckプログラムは有限の世界に存在する我々のコンピュータではSATソルバーを使って最後まで(停止するまで)実行することが出来ないことがわかります。

 同様の議論がチューリングマシンに対してもできて、「SATはチューリング完全ではない」ことも、分かってしまいます。

 このBrainfuckの構成は、ほぼホップクロフト[1]の本で万能チューリングマシンをSATの問題に変換しているのと同じ方法を使っています。でも注意して欲しいのは、ホップクロフト[1]の本でもSATがチューリング完全であることを証明しているわけではないことです。

 ホップクロフトの本ではどういう文脈でチューリングマシンをSATに変換しているかというと、「NP完全」の文脈です。NP完全の問題が解ける時、必ずある有限のステップ数より少ないステップでチューリングマシンが止まることが(その定義から)保証できるので、上記の無限ループプログラムは考えなくてよくなります。

非決定性の機能を持たせる

 さて、ここでさらにもう少し手を加えます。最初の初期値は入力・出力・中間結果テープの全てに代入するのですが、入力テープだけ一部「何も指定しない宙ぶらりん状態」にしてみましょう。

 するとどうなるか。SATのソルバーが全力で「無限ループしないような入力」を返してくれます!

 次に実行するBrainfuckプログラムは、入力テープの最初の1バイト目が2でないと最後の[]で無限ループになるように仕込んでいます。

% cabal run create simple-nondet.bf
% minisat sat.txt ans.txt || true
...
SATISFIABLE
% cabal run decode simple-nondet.bf
** Brainfuck 2 SAT **
-- Setting --
  src:,[>++<-]>----[]
  in: [(?), 0]
  value-bits: 8
  addr-bits:4
  out-addr-bits:2
  sim-steps:22
-- Result --
         Source:,[>++<-]>----[]
          Input: [(?), 0]
Estimated Input: [2, 0]
Estimated IDs:
0: ID {getPC = 0, getMem = [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], getPT = 0, getIC = 0, 
...(略)...
21: ID {getPC = 15, getMem = [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], getPT = 1, getIC = 1, getOC = 0, getOut = []}
All done, have fun.

 Estimated Input: [2, 0]に着目すると、ちゃんとSATソルバーが正解の「2」をあててくれることが分かります。

さらに、素因数分解をさせる

 だから?っていう感じでしょうが、これはかなり強力な機能です。たとえば、入力を2つ読んで掛け算した結果がある数字Nでなければ無限ループするプログラムを書き、最初の入力2つを(?)にしておくと、素因数分解ができます。

 注意
 以下のコマンドは無茶苦茶メモリを食うので、最低32GBぐらいRAMのあるマシン以外では実行しないでください:

> cabal run create mult.bf
** Brainfuck 2 SAT **
...
-- Create SAT problem --
To CNF...
4518175 clauses, 71314123 literals
Aliasing...
1232952 uniq predicates
write to file
All done, have fun.

> minisat sat.txt ans.txt
> cabal run decode mult.bf
...
-- Result --
         Source: ,>,<
[>[>+>+<<-]>>[<<+>>-]<<<-]
>>---------------[]
          Input: [(?), (?)]
Estimated Input: [3, 5]
Estimated IDs:
0: ID {getPC = 0, getMem = [0,0,0,0,0,0,0,0], getPT = 0, getIC = 0, getOC = 0, getOut = []}
...
279: ID {getPC = 49, getMem = [0,5,0,0,0,0,0,0], getPT = 2, getIC = 2, getOC = 0, getOut = []}
All done, have fun.

 このプログラムは、入力を2つ読んで掛け算して、結果が15でなければ[]で無限ループするプログラムです。Estimated Input: [3, 5]を見ると、15=3x5であると計算できています。

 10年ほど前まではこの問題の反対側にある「ある数値が素数か否か」はNP完全だと思われていましたが、今は素数であることの判定はPだと分かっています。素因数分解そのものに関しては、今でもよく分かっていません。

次は?

 そもそもNP完全ってなんだっけという所から振り返り、「テトリスはNP完全」「ぷよぷよはNP完全」とはどういう意味だったかを考え、最後に今回の「BrainfuckのソースをSATに変換する」とはどういう意味を持っていたのかを考えます。と、言いたい所だが。

参考文献

[1] オートマトン言語理論 計算論2 <第2版>,
ジョン・E・ホッブクロフト (著), R・モトワニ (著), J・D・ウルマン (著), 野崎 昭弘 (翻訳)
http://www.amazon.co.jp/dp/4781910270/ref=cm_sw_r_tw_dp_6O2Gwb1YRB125

results matching ""

    No results matching ""