SMT solver Yices を使ってみました。

SMT

研究で SMT (Satisfiability Modulo Theories) solver を使ってなにかしてみようというお話になったので、よくある数独ソルバーを作ってみました。
SMT solver とは、 SAT solver の便利バージョンのようなもので、変数、配列、関数などを定義できて、それらが満たすべき制約を等式や不等式を使って列挙して、それら制約を満たす変数、関数の割り当ての例を求めることができます。
SMT solver は SAT solver と密接に関係していて、数値の比較の式と、それらを結ぶ論理式に分けた時に、論理式を満たす真理値割り当てを求めるのに SAT solver が使われ、その真理値となる変数の割り当てを求めるのにSMT の理論が使われているようです。
例えば、(a == b and (a + b <= -1 or a + b >= 1)) を満たす変数の割り当てを知りたかったら、論理式を A and (B or C) として SAT solver にかけ, 真理値割り当てが A = true, B = false, C = true,を得られた場合、 {a == b, a + b > -1, a + b >= 1} を満たす変数の割り当てをさがして、これは {a = b = 1} が満たす (ここで失敗したら、SAT で違う割り当て探す。)、という感じのアルゴリズムだそうです。


以下のサイトを参考というか丸パ(ry しているので真新しいことはないけれど(；´∀｀)
SAT ソルバで数独を解く方法 - まめめも
SMT solver 入門 - suer のブログ


問題は、16x16の数独にしてみました。
3076 -- Sudoku
この問題は C++ でも単純な枝刈り探索だと何分待っても解が見つからず、数独を Exact cover 問題に変換して、Knuth's Algorithm X - Wikipedia を適用して枝刈り探索を効率化しないと、現実的な時間で解くことができない問題です。


問題の変換方法は先程の素晴らしいサイトにほとんど書いてあるので言うことはないのですが、いちおうプログラムを置いておきます。
https://github.com/halwhite/SmtSudoku16


実行時間は、数独の最小限のルール(行、列、ブロック内の変数は互いに異なる)のみを使った場合、4分くらいかかりましたが、すべてのnにたいして、各行、列、ブロック内のいずれかのマスはnと等しい、というヒントを追加した場合、2秒程度で終わり、その強力さがわかりました。
ちなみに、C++ で実装した Knuth's algorithm X で解いた場合、0.2秒程度で解けますが、結構しんどいです。

null instanceof Object ?

Java

java の言語仕様では、 o instanceof C の結果は、o が null だったら必ず false になると決まっているそうです。
Java Puzzlers, puzzle 50 より。

public class Point {
  private int x_, y_;
  // ...
  @Override
  public boolean equals(Object o) {
    if (!(o instanceof Point))
      return false;
    Point p = (Point) o;
    return x_ == p.x_ && y_ == p.y_;
  }
}

よくこんな風に equals を Override するけれど、o が null だったらとか今まで真面目に考えてなかったけれど、instanceof したときに弾かれてるからヌルポにならないんだということを知りました。

Cocoa Ema久

Misc

Carbon Emacs -> Cocoa Emacs に移行してみた。
http://www.emacsformacosx.com/ からダウンロードした。

よく使っていた機能がいくつか動かなかったのでメモ。

Font

carbon-fontが効かなくなったので。
英文がMonaco, 日本語がヒラギノ角ゴ、10px。
ただ全角1文字!≡半角2文字になってしまった(´∞`)
要調査。

(when (eq window-system 'ns)
  (create-fontset-from-ascii-font "Monaco-10:weight=normal:slant=normal" nil "monacokakugo")
  (set-fontset-font "fontset-monacokakugo"
                    'unicode
                    (font-spec :family "Hiragino Kaku Gothic ProN"
                               :size 10)
                    nil
                    'append)
  (add-to-list 'default-frame-alist '(font . "fontset-monacokakugo")))

fullscreen

どこからかコピペしてきたこのコードが動かず、ns-toggle-fullscreenとかいう関数もなかったので、初emacs-lisp書いてみた。
元のフルスクリーン化は広くていいのだけど、マウスでDockのアイコンが選べなくなるのが嫌だったのでちょうどいいです。

(defvar frame-toggle-state t)
(defun maximize-frame (frame)
  (set-frame-position frame 0 0)
  (set-frame-size frame 1000 1000))
(defun normal-size-frame (frame)
  (set-frame-size frame 100 50))
(defun toggle-fullscreen ()
  (interactive)
  (let ((frame (selected-frame)))
    (if frame-toggle-state
        (maximize-frame frame)
      (normal-size-frame frame))
    (setq frame-toggle-state (not frame-toggle-state))))
(global-set-key "\C-c\C-j" 'toggle-fullscreen)

この二つを直したら違和感なく使えるようになった気がする。

やっとzshとtmuxを入れました。

Misc

早く慣れたいです。

友人におすすめされてscreenではなくtmuxを入れてみたのですが、ライトユーザーなので違いはあまりわかりませんが、デフォルトで使いやすくできてて、とっつきやすいような気はします。

ただ、tmuxは使っているとすぐフリーズして困りました。(Mac OS X 10.6.4, tmux 1.3)
http://www.mail-archive.com/tmux-users@lists.sourceforge.net/msg00712.html
↑これによると、定期的に killall -SIGWINCH tmux してあげると良いらしいです。

  • tmux_defrost.sh
#!/bin/sh
CHECK=`ps -ef | grep "tmux_defrost.sh" | grep "/bin/sh" | wc -l`
if [ $CHECK = 0 ]
then
  while true
  do
    CHECK=`ps -ef | grep "/opt/local/bin/tmux" | grep -v grep | wc -l`
    if [ $CHECK > 0 ]
    then
      killall -SIGWINCH tmux
    fi
    sleep 3
  done
fi

こんな感じのシェルスクリプトを作って、.zshrc で ~/tmux_defrost.sh & みたいに呼んであげたら固まらなくなりました。

いろいろ手探りです(´∞`)