SATソルバのお試し（前編）

以前から使ってみたかったSATソルバを使ってみたので、その記録。

SATソルバのひとつminisatというのが、非常に高速と評判なので、これを使ってみよう。
SATソルバへは、連言標準形の形式で命題論理式を与える必要がある。
業界標準？では、DIMACS CNFという記法が一般的らしいけど、命題論理が全て数値で記述されており、とても読みにくい。
式が大きくなると書くだけで大変になるのは明白である。
そこで、命題論理式を書く部分を多少なりとも楽にするために、今回はRubyからminisatを利用できるruby-minisatを使ってみる。

以下、Ubuntu-14.04上で実行した。

$ sudo gem install ruby-minisat
Building native extensions.  This could take a while...
ERROR:  Error installing ruby-minisat:
        ERROR: Failed to build gem native extension.

        /usr/bin/ruby1.9.1 extconf.rb
/usr/lib/ruby/1.9.1/rubygems/custom_require.rb:36:in `require': cannot load such file -- mkmf (LoadError)
        from /usr/lib/ruby/1.9.1/rubygems/custom_require.rb:36:in `require'
        from extconf.rb:1:in `<main>'

Gem files will remain installed in /var/lib/gems/1.9.1/gems/ruby-minisat-2.2.0 for inspection.
Results logged to /var/lib/gems/1.9.1/gems/ruby-minisat-2.2.0/ext/minisat/gem_make.out
$

いきなりエラー。

そこで、このページを参考にして、ruby-devとg++をインストール。

$ sudo apt-get install ruby-dev
（略）
$sudo apt-get install g++
（略）
$

その後、以下の通りして、ruby-minisatのインストール完了。

$ sudo gem install ruby-minisatBuilding native extensions.  This could take a while...
Successfully installed ruby-minisat-2.2.0
1 gem installed
Installing ri documentation for ruby-minisat-2.2.0...
Installing RDoc documentation for ruby-minisat-2.2.0...
$

まずは、ruby-minisatのWebサイトにある、例題を解かせてみる。

例題は、以下の通りの簡単なもの。

# solve (a or b) and (not a or b) and (a or not b)

require "minisat"
solver = MiniSat::Solver.new

a = solver.new_var
b = solver.new_var

solver << [a, b] << [-a, b] << [a, -b]
p solver.solve  #=> true (satisfiable)

p solver[a]  #=> true
p solver[b]  #=> true

冒頭のコメント行にもある通り、
(a or b)、(not a or b)、(a or not b)の全てを満たす、aとbの組み合わせは存在するか？
という問題。
ここでのaとかbは、TrueかFalseの2値を取る。
この問題では、aとbが両方ともTrueの時に、命題全体が成立する。

これをsample.rbとして保存して実行。
結果は、以下の通りとなった。

$ ruby sample.rb
true
true
true
$ 

命題論理を与えるときに、

solver << [a, b] << [-a, b] << [a, -b]

なんて書けちゃうところが、大変楽チン。

ruby-minisatを作って下さった方に感謝。

というわけで、とりあえず、最初の一歩を踏み出した。
後編では、もうちょっとパズルっぽい問題を解かせてみたいと思う。