タグ : Regex

正規表現でSATを(完全に)解こう!

SATを解きましょう

Augurio Buonanno! 正規表現でやってみたシリーズ第一弾(?)です. SATを解きましょう. → 充足可能性問題

変数の組み合わせ to 正規表現

まず正規表現で問題を扱うには, 対象を文字列にエンコードしなおす必要があります.

X1,X2,…Xnなn個数の変数を真を1, 偽を0と解釈して並べると

/[01]{n}/ #これは(0|1),「0または1」のn回繰り返し

で変数の組み合わせを表現できますね. つまりn文字の2進列に対して

  • n番目の文字が1<->Xnは真
  • n番目の文字が0<->Xnは偽

とするわけです. よしよし, 変数の組み合わせは攻略しました. あとは論理式を正規表現に直せれば良いわけです.

論理式 to 正規表現

Wikipediaにある具体例を標的にしましょう.

まず第一節目について考えてみます. X1かX2が真な節. 正規表現でも or, ∨ (= |) が使えるので

/(1[01]|[01]1)/

と書くことができます. そうですよね, この正規表現にマッチする文字列は

  • 11
  • 10
  • 01

ですね. この節だけ限定して考えればこの文字列は論理式を満たす変数の組み合わせ「X1かX2が真」です!!

問題は and, ∧ です. しかし and 演算(どちらの正規表現にもマッチする)は正規表現の能力を超えていないので認めちゃいましょう. そうすると先の論理式全体は, 正規表現

/(1[01]|[01]1)&(1[01]|[01]0)&(0[01]|[01]0)/

と記述できます. ね, 簡単でしょ?

この「正規表現にマッチする全文字列」は, 先の「論理式を充足する変数の組み合わせ」に一対一対応します.

実質, 変数の組み合わせを文字列にエンコードした時点で仕事は終わっちゃいました ;-)

正規表現 to 受理文字列

理屈だけ納得してもつまらないですよね. 「どこが”完全”に解いてるの?」「普通の正規表現には’&’無いじゃん!」みたいな.

ということで宣伝にもなっちゃいますが, 僕の作ってる正規表現エンジン Regen ではなんと

  • 正規表現にマッチするテキストの生成
  • &, !(not), &&(xor) 演算

に対応しています.

Regen 内の正規表現ツール recon で上述の正規表現(論理式)にマッチする文字列を全列挙してみましょう.

SHINYA% ./recon -E -t '(1[01]|[01]1)&(1[01]|[01]0)&(0[01]|[01]0)'
10
SHINYA%

10はX1が真, X2が偽なので上述の論理式を充足しますね! 充足不可能な式は?

当然なにも出力しません.

SHINYA% ./recon -E -t '(1[01]|[01]1)&(0[01]|[01]1)&(1[01]|[01]0)&(0[01]|[01]0)'
SHINYA%

生成するテキストは正規表現が受理する全文字列(後述)なので, 充足する変数の組み合わせを全列挙してくれます.

SHINYA% ./recon -E -t '(1[01]|[01]1)'
01
10
11
SHINYA%

正規表現, 楽しいですね :-)

補足

正規表現でのand

形式言語的な意味での拡張正規表現(Extended Regular Expression)は, 正規表現に’&'(積集合演算)と’!'(否定演算)が使えます.この拡張正規表現は正規表現の能力は超えません(記述の複雑さは変わりますが). 否定の正規表現の話題はshibuya.pmでも発表しました. 否定とorさえあればandもできますね.

Regenについて

この記事で紹介したツールは Regen をインストールすると使えます(ちなみに「レーゲン」と読みます. ドイツ語カッコいい.). githubから取ってきて使ってやって下さい.まだ色々実装が足りないので資料など皆無(コマンドのヘルプすら!)ですが,

% git clone git@github.com:sinya8282/Regen.git
% cd Regen/src
% make recon REGEN_ENABLE_PARALLEL=no REGEN_ENABLE_XBYAK=no
% ./recon -h
USAGE: regen [OPTIONS]* PATTERN
Regex selection and interpretation:
  -E   PATTERN is an extended regular expression(&,!,&&,||,,,)
  -f   obtain PATTERN from FILE
Output control:
  -t   generate acceptable strings
  -d   generate DFA graph (Dot language)
  -m   minimizing DFA
%

という風に, 今回紹介した生成系は使え(ま|るはずで)す.

(‘-E’ オプションは拡張演算子on, ‘-t’で受理文字列のモード)

他の機能やオプションも説明したいですが, それは次の機会で…(手抜き)

全文字列の列挙?

説明中では「正規表現にマッチする全文字列を列挙」と書きましたが, これは嘘です.例えば

/a*/

みたいなKleene閉包が使われる正規表現は

"", "a", "aa", "aaa",...

と無限の文字列にマッチしうるので, 全列挙は不可能です.

じゃあ, どうするか? (無限はむりでも数を限定すればなんとかなりそうです.)

この辺りは面白い話なので是非次の記事辺りで説明したいと思います!

後方参照でSATを解く

ここでは完全にpureな正規表現でもSATを解けることを紹介しました.調べてみるとPerlなどでお馴染みの後方参照を使って解く方法も解説されてました. まめめも: 後方参照のある正規表現の能力(ただし, 後方参照使うと非正規表現ですよ!)正規表現でSATを解く, 思いついた時にはいかにもありそうなネタと思っていましたが, 検索した範囲で見当たらなかったので記事にしました.正規表現, 楽しいですね :-)

追記

会場で @shinh さんに「Perlなら先読み(?=)あるから/R1&R2/みたいな正規表現は/(?=R1)R2/でいけるよね.」というアドバイスをお受けしました. なるほど.
今回のSATの例も先読みを使えば「SATを充足する変数組み合わせを受理する正規表現」は記述できます.
ちなみに Perlな正規表現の受理文字列生成とかできる module とかあるんでしょうか? (全文字列を生成して通す, というアプローチでなく)
Perlでの先読みは(実装は)オートマトン的ではなく, 再帰を使って実装されています(と思う). ゆえに「先読みってオートマトン理論的にどうなの?」というお話もありますが, このあたりも非常に面白い話なので次回の記事あたりでまとめたいと思います.

Shibuya.pm 〜夏の正規表現祭り〜 で好きなこと喋ってきた.

夏だ祭りだ正規表現だ!!

ということで, 行ってきました Shibuya.pm @ mixi

僕はありがたくも「正規表現の限界」とLT・宣伝で「僕の考えた世界最強の正規表現エンジン」と2つの枠で発表させてもらいました.

「正規表現の限界」の方は, 割と皆さん面白いと行ってくれて本当に嬉しかった. 発表するまで「こんなの当たり前じゃん」とか「誰得」とか切り捨てられないかな… とかネガティブループしてたんですが, 発表してみるとやっぱり楽しかった.

計算量だとかアルゴリズム詳細とかは末尾の資料を参照してください. つっこみがあれば修正したいです.

というかつっこみがなくても修正しなくちゃな… チラッと触れて説明してないところ多いし :-)

メモメモ

以下, 心に残った言葉, 印象深かったことをメモ

最後に, 懇親会でこれを聞けて嬉しかった

「キャプチャ"する"括弧こそ特別な表記にすべきじゃないですか?」と @ さんに聞いたら, 「Perlの父 Larry もそこは後悔している」みたいなことを聞けて少しスッキリした. ダンさんも聞きまくったらしいw #shibuyapm
@sinya8282
Ryoma SHINYA

 
Better Tag Cloud