世界一難しい数独、Alloyで解いてみたよ(RocketNews24から)

Alloy 数独

RocketNews24さんで 本当に解ける人いるの？　フィンランド人数学者が作った “世界一難しい数独” が発表されるという記事があったんで以前のAlloyの記事で使ったモデルを流用して解いてみた。

about alloy
Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks.
結論：
実は自分は数独のルールをわかっていなかった。
前回より工夫したところ：
  1. 数字をOne,Twoといったような表記ではなく、C01とか数字が入った表現にした。
  2. 数独って、9x9の枠の中でカブっちゃいけない、ってルールがあったんだ。。。。ということに気づいてルールを追加した。orz

では、以前のモデルを一部流用して解いてみます。

↓9x9のグルーピングを追加

abstract sig Index {}
sig Col extends Index {
  cell : Index -> Index
}
abstract sig G01,G02,G03 extends Col {}
one sig C01,C02,C03 extends G01{}
one sig C04,C05,C06 extends G02{}
one sig C07,C08,C09 extends G03{}

縦、横の重複禁止ルールの他に9x9の重複禁止ルールを追加

// 縦横の禁止
fact{
  all c:Col, r1,r2:Index | (r1=r2)or(not(cell[c,r1]=cell[c,r2]))
}
fact{
  all c1,c2:Col, r:Index | (c1=c2)or(not(cell[c1,r]=cell[c2,r]))
}
// 9x9の重複禁止
fact{
  all c1,c2:G01, r1,r2:G01 | (r1=r2 and c1=c2)or(not(cell[c1,r1]=cell[c2,r2]))
}
fact{
  all c1,c2:G01, r1,r2:G02 | (r1=r2 and c1=c2)or(not(cell[c1,r1]=cell[c2,r2]))
}
:

実際に解かせてみると。。。。

Executing "Run run$1 for 13"
   Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   77305 vars. 2201 primary vars. 146903 clauses. 3635ms.
   . found. Predicate is consistent. 82243ms.

82秒。

チェック結果掲載できてませんが、解答ページを見てみるとちゃんとあっていました。

f:id:dec9ue:20120704182506p:plain

ちなみに、標準的な問題を解かせてみると。。。

Executing "Run run$1 for 13"
   Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   77309 vars. 2201 primary vars. 146933 clauses. 3712ms.
   . found. Predicate is consistent. 49608ms.

50秒。

つまり、世界一難しい問題は、SATソルバからみると60～70%程度難しい問題だってことがわかりました。

いずれにせよ、Alloyって戦略を明示しなくてもいいのにコレぐらいの時間で数独が解けてしまいます。数独はAlloyがとても良くハマる問題だといえるのではないかと思います。

コードはこちら

追記： 2012/07/04 回答の図をアップしました。あと、Alloyの説明をちょっと追加。

【送料無料】 抽象によるソフトウェア設計 ALLOYではじめる形式手法 / ダニエル・ジャクソン 【...

Control.DeepSeqを使って正格評価(訂正版)

Haskell

何が酷いって、記事を見なおしてみたらfoldrとfoldlのロジックを間違えてる。コレは死ねる。。。ただ、Bangについてはそれでもちょっと怪しいので訂正版の記事を作り直したいと思います。

古い記事 は自戒の意味も込めて残しておきます。(なんの意味があるのかは不明)

モンテカルロ法で円周率を計算するために多数のIOから取り出した結果の集計を行おうとした。

しかし未評価thunkによるメモリオーバーフローが発生し、インスタンス数を増やせなかった。途中でわざとprintを行なって未評価thunkを潰してメモリリークを防いでいたのだがもちろんこれは本質的な解決ではない。

また、Bang-Patternを使用して未評価thunkを潰そうとしたが、どうもthunkが潰れてくれない。

調べてみたところ、厳密な正格評価にはControl.DeepSeqが使用できることがわかったので試して見ることにした。

 

まず、リークを起こすコードの説明から。

main :: IO ()
main = do
    (count,total)  Int -> IO Stat
takeStat func count =
    foldLN1 sum_stat (liftM point_to_stat func) count (0,0)

foldLN1 :: (a->b->a) -> IO b -> Int -> a -> IO a
foldLN1 folder m count init =
    let foldLN_sub folder m count v = if count == 0
        then v
        else let v' = unsafePerformIO m
              in foldLN_sub folder m (count -1) $! folder v v'
    in return $ foldLN_sub folder m count init

だいぶ端折っているが、foldLN1という関数で$!の形でBang-Patternを使用している。にもかかわらず、実行するとメモリオーバーフローで落ちる。(どうやら、folder関数のthunkが潰れ切らないらしい) そこで、DeepSeqを使用したコードに修正する。

foldLN1 :: (NFData a) => (a->b->a) -> IO b -> Int -> a -> IO a
foldLN1 folder m count init =
    let foldLN_sub folder m count v = if count == 0
        then v
        else let v' = unsafePerformIO m
              in foldLN_sub folder m (count -1) $!! folder v v'
    in return $ foldLN_sub folder m count init

NFDataクラスはDeepSeqモジュールの正格評価を適用できるデータのクラス。$!!はBang-Patternsにおける$!に相当する。引数を(Bang PatternsにおけるWHNFではなく、)値になるまで評価する。

そもそも、unsafePerformIO使っているし、foldを自分で書くクソダサさと、無茶しまくっている、、、 でも、確かにコレで落ちない。

ちなみに、DeepSeqを使用しなくても下記のように時々thunkを潰すような処理を入れてあげると上手く回る。

foldLN2 :: (Show a) =>(a->b->a) -> IO b -> Int -> a -> IO a
foldLN2 folder m count init =
    let foldLN_sub folder m count v = if count == 0
        then v
        else let v' = unsafePerformIO $ do
                 when (count `mod` 100000 == 0) $ print_stat v count
                 m
              in foldLN_sub folder m (count -1) $! folder v v'
    in return $ foldLN_sub folder m count init

コード： Recursion2.hs

参考：

【まとめ】Haskellでの正格評価とWHNF
http://kamonama.blogspot.jp/2011/04/haskellwhnf.html
shelarcyさんの説明
http://www.sampou.org/cgi-bin/haskell.cgi?shelarcy

補足：

$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 7.4.1
$ ghc -O Recursion.hs
[1 of 1] Compiling Main             ( Recursion.hs, Recursion.o )
Linking Recursion.exe ...

Control.DeepSeq を使用して正格評価

Haskell

本記事はfoldのアルゴリズムに対する理解がめちゃくちゃだったんで修正記事作りました。(2012/06/25)

モンテカルロ法で円周率を計算するために多数のIOから取り出した結果の集計を行おうとした。

しかし未評価thunkによるメモリオーバーフローが発生し、インスタンス数を増やせなかった。途中でわざとprintを行なって未評価thunkを潰してメモリリークを防いでいたのだがもちろんこれは本質的な解決ではない。

また、Bang-Patternを使用して未評価thunkを潰そうとしたが、どうもthunkが潰れてくれない。

調べてみたところ、厳密な正格評価にはControl.DeepSeqが使用できることがわかったので試して見ることにした。

 

まず、リークを起こすコードの説明から。

-- Simple example for Bang-Patterns leak
import Control.Monad
import Data.Foldable ( foldr' )
import System.IO

main :: IO ()
main = do
    result <- takeStat (return 100) 10000000
    print $ "result is " ++ show result

takeStat :: IO Int -> Int -> IO Int
takeStat io count =
    foldr' (liftM2 (+)) (return 0) $ replicate count io

実行するとメモリオーバーフローで落ちる。 そこで、DeepSeqを使用したコードに修正する。

takeStat :: IO Int -> Int -> IO Int
takeStat io count =
    foldr'' (liftM2 (+)) (return 0) $ replicate count io

instance NFData a => NFData (IO a) where
    rnf x = rnf $ unsafePerformIO x

foldr''  :: NFData b => (a->b->b) -> b-> [a] -> b
foldr'' folder init           = init
foldr'' folder init (head:tail) =
    (foldr'' folder $!! (folder head init)) tail

NFDataクラスはDeepSeqモジュールの正格評価を適用できるデータのクラス。$!!はBang-Patternsにおける$!に相当する。引数を(Bang PatternsにおけるWHNFではなく、)値になるまで評価する。

foldを自分で書くクソダサさとIOを今更(しかも無理に)インスタンス化したり、無茶しまくっている、、、 でも、確かにコレで落ちない。

Bang Pattern的には下記なら大丈夫な感じがしてしまうが、やっぱりメモリ不足でおちちゃう。なぜダメなんだろうなぁ。

takeStat :: IO Int -> Int -> IO Int
takeStat io count =
    return $ foldr' (+).unsafePerformIO 0 $ replicate count $ unsafePerformIO io
参考：【まとめ】Haskellでの正格評価とWHNF
http://kamonama.blogspot.jp/2011/04/haskellwhnf.html

補足：

$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 7.4.1
$ ghc -O Recursion.hs
[1 of 1] Compiling Main             ( Recursion.hs, Recursion.o )
Linking Recursion.exe ...

追記：

IOをインスタンス化するのはやっぱ嫌なのでどうせunsafePerformIOつかうなら下記がいいかな、、、

takeStat :: IO Int -> Int -> IO Int
takeStat io count =
    return $ foldr'' ((+).unsafePerformIO) 0 $ replicate count io

foldr''  :: NFData b => (a->b->b) -> b-> [a] -> b
foldr'' folder init           = init
foldr'' folder init (head:tail) =
    (foldr'' folder $!! folder head init) tail

追記２：

foldr'の根本にforceを挿してみたがこれもダメ。Bang Patternsがちゃんと動いていないのでは？

takeStat :: IO Int -> Int -> IO Int
takeStat io count =
    return $ (foldr' . force) ((+).unsafePerformIO) 0 $ replicate count io

正格評価がうまく動かない？

モンテカルロ法で円周率計算、みたいな話がちょろっと降ってきたので任意精度で計算できるようなコードをHaskellで書いてみたのだがループの中でどうもスペースリークしている。もう少しいうと、集計用の畳み込み関数が未評価のまま残ってしまうようだ。

    
main :: IO ()
main = do
    (count,total)  Int -> IO Stat
takeStat func count =
    let c   = \(x1,y1)(x2,y2) -> (x1+x2,y1+y2)
        f   = \ (x,_) -> if x then (1,1) else (0,1)
    in
    foldRN c (liftM f func) count (0,0)

みたくして、foldRN関数を次のように。(unsafePerformIOは見逃してw)

foldRN :: (Show a)=> (a->a->a) -> IO a -> Int -> a -> IO a
foldRN folder m count init =
    let foldRN_sub folder m count v
        | count == 0 = v
        | otherwise  =
            let r = unsafePerformIO $ do
                when ((count `mod` 100000) == 0) $ do
                    putStrLn $ "v: " ++ show v ++ " count: " ++ show count
                    hFlush stdout
                m
            in
            foldRN_sub folder m (count -1) $! folder v r
    in return $ foldRN_sub folder m count init

これ、whenがないとスペースリークで死んでしまう。 再帰関数のtail-recursionでBangによってthunkを潰してるはずなのに。。。 なぜ、、、、 あとMonoid使わねーの？という指摘がありましたら甘んじて受けます。

ガベージコレクタのアルゴリズムと実装（アルゴリズム編）のメモ

一章
ガベージコレクタの評価項目
・スループット
・停止時間
・使用効率
・局所性

二章
マークスウィープはメモリ全体を舐める
フラグメントがたまる
→BiBOP法（BigBagOfPages）
      phkmallocみたいなやり方
チャンク検索のコストが上がる
→サイズ別チャンク

単純なやり方ではコピーオンライトと仲が悪い
→ビットマップマーキング

遅延スウィープ
・全体を舐めなくて良い

三章
遅延参照カウント
・普段はルートからの参照をカウントしないが開放要否の判断時にカウントアップして帳尻を合わせる
スティッキー参照カウント
・カウントアップ式マークスウィープをへいようしてhappy
1ビット参照カウント
部分マークスウィープ
・デリファレンス時に子孫オブジェクトのリファレンスカウント分を差し引いてみて自分に帰ってきたら循環判定。ゼロなら抹殺

四章
普通のコピーGC
・再帰アルゴリズムで深さ優先
cheneyのアルゴリズム
・反復的で幅優先
擬似的深さ優先アルゴリズム
・近いものを近くに置ける

五章
コンパクションは空間効率がいいが時間効率が悪い
BiBOPとtwofingerを併用するアイディア
テーブル法
・連続オブジェクトをオフセットを使って管理する
・フォワードポインタが不要
immixGCは一旦飛ばす

六章
保守的GCには
・不明瞭なルート
・不明瞭なオブジェクト
の２つがある
前者は
・間接参照
・mostly copied
・ブラックリスト
で確実なGC相当のコピーGCを（リークを許容しながら）実現できる
後者はオブジェクトを移動できずマークスウィープ以外の選択肢はない

七章
Rememberセットには参照元を登録する
ライトバリアで旧世代ポインタの変更を拾うと実装しやすい
trainGCは一旦飛ばした

八章
Dijkstra 参照更新時、新しい参照先が未クロールならグレー（クロール対象）に塗る
Steele クロール済みオブジェクトに修正が入ったら再クロールの対象にする
Yuasa マーク開始時のリンクでマークし、ライトバリアでは旧オブジェクトをこぼさないように差分をフォローする。