日々の流転

λ. Pseudo-Boolean Competition 2012 に参加

Pseudo-Boolean Competition 2012 (PB12) に簡単な自作ソルバを投稿してみた。

2011年振り返りのところで書いたように、昨年はいろんな決定手続きのアルゴリズムを書いたりして遊んでいて、どうせならコンペに出してみるかと、昨年秋に予定されていた Pseudo-Boolean Competition 2011 (PB11) の Second round を目指していた。 ただ、Second round は結局キャンセルになりその代わりに今回のPB12が開催されることになったので、今回のPB12に投稿することにしたのだった。 V. Manquinho and O. Roussel がオーガナイザとして開催するのは今回が最後の予定で、かつ Second round の予定の時点ではほとんど何も準備できていなかったので、延期でそれなりに準備できて参加できたのはラッキーだったかもしれない。

とは言っても、結局そんなに大したものはできず、基本的なSATソルバ + カウンターベースの素朴なPB制約の実装くらいしかできていない。 なので、全然 competitive なものにはできなかったんだけど、せっかくなので一応投稿はしておいた。 本当はLP緩和やMIS緩和による下界値計算、cutting plane proof system による conflict analysis 等をはじめ、やりたいことは色々あったんだけど、時間切れ。 やり残したことは悔しいけど勉強にはなったし、 ICFPC や Google Code Jam みたいなコンテストとはまた違って面白かった。 もし来年があるなら、来年までには色々何とかして、また参加したいね。

• PB12投稿版
  • PB12に投稿したバイナリ(x86_64 linux 用)
  • PB12投稿版のソース＠github
  • Win32版のバイナリ
• 2012-05-18 差し替え版: toysat-PB12-20120518-linux-x86_64.zip
• 2012-06-02 差し替え版: toysat-PB12-20120602-linux-x86_64.zip
• 最新版のソース＠github

λ. Linux版のGHCでスタティックリンク

Pseudo-Boolean Competition 2012 投稿用にスタティックリンクした Linux 向けバイナリを生成する必要があった。 それで試してみたら、GHC は -static がデフォルトだと聞いていたにも関わらず、ビルドしたら色々動的にリンクされてしまっていた。

% ldd toysat
linux-vdso.so.1 => (0x00007fffed5ff000)
libgmp.so.10 => /usr/lib/libgmp.so.10 (0x00007f84eb415000)
libffi.so.6 => /usr/lib/x86_64-linux-gnu/libffi.so.6 (0x00007f84eb20d000)
libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007f84eaf88000)
librt.so.1 => /lib/x86_64-linux-gnu/librt.so.1 (0x00007f84ead80000)
libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007f84eab7c000)
libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007f84ea7dc000)
libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007f84ea5bf000)
/lib64/ld-linux-x86-64.so.2 (0x00007f84eb69c000)

どうしたら良いか困ったが、結局 linux - Haskell program built on Ubuntu 11.10 doesn't run on Ubuntu 10.04 - Stack Overflow に従って、「cabal configure --ghc-options="-static -optl-static -optl-pthread"」とすることでスタティックリンクしたバイナリを生成できた。