2002-04-21
λ. キャッシュ
考えてみたら、TDiary::Plugin#eval_rhtmlだけ測っても仕方がないよな。
とりあえず、tdiary-cache-rb.diffを当てて、しばらく生活してみることにする。この日記だと概ね10%程度速くなっているようだが、体感は出来ない。
λ. wforum-msgid.diff
関係某所で利用されているwforumのためのパッチ。メールを送るときにMessage-Id:とIn-Reply-To:を付加する。
それにしても彼らは何でこういうスクリプトを量産するかな。尻拭いする側の事も少しは考えて欲しいのだ。
2005-04-21
λ. C304 裏切りの村 4日目
[2005-06-05 追記] 4日目に出たアルビン(真占い師or狂人)吊りに関する意見を簡単に引用しておく。
- 旅人 ニコラス 午後 10時 42分
オットーがアルビン吊りに触れているが、俺にはどうも良くわからない。
アルビンは真でも偽でも人間だよな。
もし占い結果や霊能結果によって情報を得られる見込みがあるなら、狂人吊りはそのための時間稼ぎになると思うけど、そうでない場合に狂人を吊ることに何かメリットはあるのかい?- パン屋 オットー 午後 10時 47分
一匹も人狼が吊れないと一日早く終わっちゃうよ。
- パン屋 オットー 午後 10時 49分 (独り言)
ニコラス・・・その発言は怪しすぎる・・・
- 旅人 ニコラス 午後 11時 18分
オットーに言われて少し考えてみた。
カタリナを吊った後、アルビンを吊ると「6人中2人が人狼」に、それ以外を吊ると「6人中1〜2人が人狼で0〜1人が狂人」となる。
確かに後者(の最悪の場合)には人狼側が票を合わせて勝負に出る可能性があるな。だけど、前者であってもそこで判断を間違えたら結局お仕舞いだぜ。
それならば、多少のリスクは負ってでもグレーを狭めるべきだと個人的には思う。
オットーの「一匹も人狼が吊れないと一日早く終わっちゃうよ」というのはあまり正しくない。残り人数が偶数である以上、狼側が最終日以外でランダム勝負に出ない限り早く終わることはない。そして、狼側が最終日以外にランダム勝負にでる誘因というのは実は小さい。
この辺りのことをちゃんと考えて理路整然と伝えられなかったことには悔いが残る。この発言がもとでオットーに疑われてしまったようなものだし。
[2005-06-06 追記] 青年 ヨアヒムのアルビン真の議論(1,2,3)は参考になるな。次に参加するときにはこういった視点も持ちたい。
ペーター真と思わせアルビンの信用を下げる、または本当にペーター真である。の、どちらかだとは思うんだが…どっちかというと俺は前者寄り。
以下ペーター真として。
ヤコブはちょっとアルビン寄りだったし、彼が村人でアルビン偽ならペーターを襲わず白判定を出せば信用度はそのままだったと思う。
それに今確定白といえるのは共有者の２人。ここで白判定を出せば襲撃範囲は広がり狩人はちょっと手一杯で確白狙いの襲撃成功率は上がる。
黒判定で得る利点は自分の信用を利用して弁の立つ村人を吊れる、ってとこなんだけど、これは対抗のペーターを襲うと自分の信用も下がるため成功率がかなり低くなる。それに襲撃対象は共有者の２択になり正直狩人との睨み合いがキツイのではないかと。
今GJ出されると吊り回数１回増えるし、かといってグレーを襲うと村人にヒントを与えてしまう。
そんな感じでヤコブ偽黒判定の利点は少ないと思うので、俺はまだアルビン真と見てるぜー。
[2005-06-07 追記] ところで、私は4日目の時点ではカタリナ人狼という思いから霊能者ローラーに目がいってしまっていて、その後の展開を十分に考えてれていなかったようだ。私は占い師or狂人のアルビンは吊らない方向で考えていたのだけど、その場合にはカタリナを急いで吊る必要も無いはずなのだ。だから、アルビンから黒判定を出されたヤコブを吊ってカタリナに判定させて、翌日にカタリナを吊るというのも十分に選択肢になったはず。その方向で考えをまとめて意見として主張すべきだった。
2006-04-21
λ. 人狼審問 : (1371)いんげんおいしいよね村 桜だ！
学者の村のエピローグで「いんげん村」について紹介されたので、観戦してみることにした。色々と面白そう。
ツッコミルール
クインジーが>>1:504で提案しているツッコミルールが独特で面白い。
■10. 占吊の決定は基本的に多数決で決める。俺が生きている間は明日から以下のツッコミルールを適用する事を提案する。
- 誰かの占い希望もしくは吊り希望どちらかにツッコミを入れなければならない。ツッコミ入れない人は占い希望および吊り希望の両方をカウントしない。
- ツッコミは自分の占い希望と吊り希望の両方出してからする事。
- ツッコミが入ったら、反論するか希望を変えること。どちらもしない場合は、その希望（占い希望へのツッコミであれば、占い希望）はカウントしない。
- 各自、何時までツッコミが受け付けられるか明示する事。そして、それまでに必ず占い希望と吊り希望を出す事。
- 目的は議論の早回しと議論の活性化ね。ある程度時間を拘束するけど。
守護者の護衛先騙り
なんて作戦があるとは思いもしなかった。人狼は襲撃失敗の理由が守護者の護衛によるものか襲撃先が妖魔だったからかを区別できない。そのため、護衛に成功した守護者が護衛先を騙ると、人狼からすると襲撃先が妖魔だったかのように見える。それによって、状況によっては人狼の妖魔告発を誘うことが出来る。具体的にはヘンリエッタの>>5:33と>>5:167を参照。
λ. f(f(n)) = n+1
以下のような関数 f が存在する場合は実装し、 存在しない場合はそのことを証明せよ:
- nが整数なら f(n) は整数
- nが整数なら、f(f(n))=n+1
- f(x+1) = f(f(f(x))) = f(x)+1 for x∈Z
- よって、f(x) = f(0)+x for x∈Z
- したがって、1 = f(f(0)) = f(0)+f(0) = 2 f(0) より f(0) = 1/2 だが、これは条件1に矛盾
- ゆえに、そのような関数は存在しない
λ. 風邪
風邪ひいたっぽい。 喉が痛いし、なんだかだるい。
2007-04-21
λ. 風邪
また風邪引いたっぽいので、予定を色々取りやめ。 週末毎に体調崩してたら何も出来ないって…… orz
λ. WORLD ECONOMY #1 Introduction
を観た。 ODAの及ぼしうる悪影響の一つとして挙げられていた「ODA資金によって需要が増える一方で供給能力は増えずインフレが発生し、またそれによって国際競争力が低下するため産業が発展しなくなる」という話が面白かった。 というか、熱でぼーっとしていたので、ほとんどそれしか覚えていない(苦笑
2009-04-21
λ. ASPで数独を解く
こないだはIDPで数独を解くというのを書いたが、今度は解集合プログラミング(Answer Set Programming, ASP)のソルバに解かせてみることにした。
ASPとは
ASPソルバは、これまでに使ってきたParadox等と同様のモデル探索器(model finder)なんだけど、Paradox等が普通の一階述語論理に基づいていたのに対して、ASPは論理プログラミングの考え方に基づいている点が少し異なる。
論理プログラミングの考え方に基づいているので、モデルとして考えているのは最小エルブランモデルや安定モデル(stable model)の一般化である解集合に限られているし、また否定に関しても古典論理の否定(classical negation, strong negation)とは別に「デフォルトの否定(default negation)」(= 「失敗による否定(negation as failure)」)を持っている。
そのため、到達可能性などを記述できたり、知識表現を行いやすかったりするのではないかと思う。 Prolog等で論理プログラミングに親しんでいる人にとっては、一階述語論理に基づいたモデル探査機よりASPのソルバの方が、親しみやすいだろう。
今回使ったソルバ
今回はPotasscoで配布されているものを使ってみた。
Potassco, the Potsdam Answer Set Solving Collection, bundles tools for Answer Set Programming developed at the University of Potsdam, among them, the answer set solver clasp, the grounder Gringo, and their combinations Clingo and iClingo.
こないだのIDPもそうだったけど、Potasscoでもグラウンダとソルバは別々になってるのね。
問題の記述
人工知能学会誌 Vol. 23 No. 5 (2008年9月) の「論理コンピューティング」(佐藤健, Marina De Vos)にちょうど数独の例が載っていて、それをほぼそのまま用いることが出来た。
sudoku-clingo.lp:
% 位置は1から9まで
position(1..9).
% 値も1から9まで
value(1..9).
% 各X,Yについて、state(X,Y,N)を満たすNがただひとつ存在
1 {state(X,Y,N) : value(N)} 1 :- position(X), position(Y).
% ある行の中の異なる場所に同じ数字があったら矛盾
:- state(XA,Y,N), state(XB,Y,N),
position(XA), position(XB), position(Y), value(N),
XA!=XB.
% ある列の中の異なる場所に同じ数字があったら矛盾
:- state(X,YA,N), state(X,YB,N),
position(X), position(YA), position(YB), value(N),
YA!=YB.
% 範囲の定義
subRange(X,1) :- position(X), 1<=X, X<=3.
subRange(X,2) :- position(X), 4<=X, X<=6.
subRange(X,3) :- position(X), 7<=X, X<=9.
% (XA,YA)と(XB,YB)が同じボックスの中にある
sameSubSquare(XA,YA,XB,YB) :-
subRange(XA,XR), subRange(XB,XR),
subRange(YA,YR), subRange(YB,YR).
% 同じボックスの中の異なる場所に同じ数字があったら矛盾
:- state(XA,YA,N), state(XB,YB,N),
sameSubSquare(XA,YA,XB,YB), value(N), XA!=XB, YA!=YB.
% 数字の既知の配置
state(1,1,1). state(1,4,2). state(1,7,3).
state(2,2,2). state(2,5,3). state(2,8,4).
state(3,3,3). state(3,6,4). state(3,0,5).
state(4,1,6). state(4,4,4). state(4,7,5).
state(5,2,7). state(5,5,5). state(5,8,6).
state(6,3,8). state(6,6,6). state(6,0,7).
state(7,1,8). state(7,4,0). state(7,7,7).
state(8,2,0). state(8,5,1). state(8,8,8).
state(0,3,1). state(0,6,2). state(0,0,4).
ちなみに、この数字の既知の配置は以下のようなものになっている。
1 |6 |8 2 | 7 | 9 3| 8| 1 ---+---+--- 2 |4 |9 3 | 5 | 1 4| 6| 2 ---+---+--- 3 |5 |7 4 | 6 | 8 5| 7| 4
実行結果
clingo sudoku-clingo.lp として実行したら、sudoku-clingo.txtのような出力が出てきた。これを見ると「Answer: 1」に続くアトムの列が解になっており、その中に「state(1,1,1) state(1,4,2) state(1,7,3), …」の部分が、実際の割り当てを現しているようだ。
それを表の形にすると以下のようになる。
179|632|845 428|175|693 563|948|271 ---+---+--- 257|413|968 836|259|417 914|786|352 ---+---+--- 381|594|726 742|361|589 695|827|134
2010-04-21
λ. GLPKで数独を解く
去年はいろんなソルバやモデルファインダーを使って数独を解いて遊んでいて、最後にやったのが、丁度一年前の記事の「ASPで数独を解く」。 一年ぶりにまたふとやってみたくなったので、今度はフリーの線形計画法ソルバの GLPK (GNU Linear Programming Kit) を使ってやってみた。
まずは問題の構造を記述したファイル SudokuGLPK.mod:
set Number := 1..9;
param Data{Number, Number, Number} binary default 0;
var Ans{Number, Number, Number} binary;
s.t. GIVEN{x in Number, y in Number, n in Number}: Data[x,y,n] <= Ans[x,y,n];
s.t. FILLED{x in Number, y in Number}: sum{n in Number} Ans[x,y,n] = 1;
s.t. COL{n in Number, x in Number}: sum{y in Number} Ans[x,y,n] = 1;
s.t. ROW{n in Number, y in Number}: sum{x in Number} Ans[x,y,n] = 1;
s.t. BLOCK{n in Number, x0 in 0..2, y0 in 0..2}:
sum{x1 in 1..3, y1 in 1..3} Ans[3*x0+x1, 3*y0+y1, n] = 1;
「座標(x,y)の数がnであること」をAns[x,y,n]が1であることで表現して、その組み合わせに関する条件を算術的に表現している。 やっている事自体はSATで解く場合と大して変わらないんだけど、結構直観的に書けて良かった。
次に、具体的な問題のデータを記述したファイル SudokuGLPK.dat:
param Data := 1 1 1 1 1 4 2 1 1 7 3 1 2 2 2 1 2 5 3 1 2 8 4 1 3 3 3 1 3 6 4 1 3 9 5 1 4 1 6 1 4 4 4 1 4 7 5 1 5 2 7 1 5 5 5 1 5 8 6 1 6 3 8 1 6 6 6 1 6 9 7 1 7 1 8 1 7 4 9 1 7 7 7 1 8 2 9 1 8 5 1 1 8 8 8 1 9 3 1 1 9 6 2 1 9 9 4 1;
このファイルは配列Dataに対する値の割り当てを表していて、「a b c 1」という行は Data[a,b,c] が 1 であることを表している。
これで glpsol.exe -m SudokuGLPK.mod -d SudokuGLPK.dat -o ans.txt と実行すると、ans.txtのようなファイルが得られる。 このファイルの途中を見ると、以下のような感じで配列Ansに対する値の割り当てが得られる。 たとえば、Ans[1,2,4]のActivityが1なので、座標(1,2)の数が4であることが分かる。
…
No. Column name Activity Lower bound Upper bound
------ ------------ ------------- ------------- -------------
1 Ans[1,1,1] * 1 0 1
2 Ans[1,1,2] * 0 0 1
3 Ans[1,1,3] * 0 0 1
4 Ans[1,1,4] * 0 0 1
5 Ans[1,1,5] * 0 0 1
…
13 Ans[1,2,4] * 1 0 1
…
参考
2012-04-21
λ. 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投稿版
- 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"」とすることでスタティックリンクしたバイナリを生成できた。
