もう、一年ほど前のことになりますが、ひとりにしてくれの穴埋めの記事を書きました。
ひとりにしてくれの穴埋めってなんのこと？ って方はこちらとこちら。以下、これらの記事はご覧になっているものと仮定します。
でまあ、以前の記事から結果的には変わりないんですけど、PencilBoxのひとりにしてくれファイルから、Sugarを経由しないでそのままminisatに入力できるCNFファイルを出力するスクリプトをですね、書きました。
半袖さんの記事がきっかけで、ここ二日ほど夜更かしです。
なにが嬉しいかと言うと、JavaとSugarをインストールしてなくても、minisatをぽんと置くだけで使えるってことなんですが、結局minisatが必要になるのであまりハードルは下がりませんね。
PencilBox→CNFファイル変換スクリプト(a5.awk)
PencilBoxひとりにしてくれファイル、骨組み(samp.txt)
使い方 #gawk -f a5.awk samp.txt > cnf.txt
CNFファイルができるのでこれをminisatに放り込みます。
結果CNFファイル
使い方 #./minisat cnf.txt ans.txt
ans.txtに結果が格納されます。
minisat結果ファイル→PencilBoxひとりにしてくれファイル変換スクリプト(bb.awk)
ただし、元の問題が8x8、12x12,17x17の場合しか動きません
使い方 #gawk -f bb.awk ans.txt > samp_a.txt
ぼくの環境(puppy linux CD起動)ですが、17x17でも1秒かからずに終了しました。nikoli.comに投稿するんでここでは例示できませんが。
参考にさせていただいたホームページはこちら。というかほとんど内容のごく一部をそのままですね。ありがとうございます。
・ひみつ基地＠東工大 SATソルバーと数独
・まめめも SATソルバーで数独を解く方法
・soutaroにっき SATソルバを使うためにCNFを作る
