2009-03-02 [長年日記]
λ. PPL2009参加します
今更ですが、今年もPPL2009に参加する予定です*1。色々な人にお会いできるのを楽しみにしていますので、見かけたら是非お気軽に声をかけてくださいませ。
*1 二日目の セッション8 (萌芽的研究) で発表します
λ. Maceで数独を解く
ParadoxとDarwinで解いてみたので、ついでにMace4でも試してみたのだけど、どうもうまくいかなかった。
- 入力ファイル sudoku-mace4.in
- ログ sudoku-mace4.txt
ちなみに、Mace4はこんなやつ。
Mace4 is a program that searches for finite models of first-order formulas. For a given domain size, all instances of the formulas over the domain are constructed. The result is a set of ground clauses with equality. Then, a decision procedure based on ground equational rewriting is applied. If satisfiability is detected, one or more models are printed. Mace4 is a useful complement to first-order theorem provers, with the prover searching for proofs and Mace4 looking for countermodels, and it is useful for work on finite algebras. Mace4 performs better on equational problems than our previous model-searching program Mace2.
【追記】 Sudoku with Mace4 にMace4を使って数独を解く話があった。 これを参考に入力ファイルに「assign(domain_size, 9).」を加えて、数字の9を0に置換したら普通に解けた。 Mace4では非負整数nはモデルのn番目の要素を指す項になっていて、その関係でちょっと注意が必要ということのようだ。
- 入力ファイル sudoku-mace4-2.in
- ログ sudoku-mace4-2.txt
いいなぁ．
ささださんは不参加? それは残念……