Think Stitch
  最近の更新


Pthread Model Checker でペグソリティアを解く

Photo by Gnsin (https://commons.wikimedia.org/wiki/File:Solitaire_01.jpg)

ペグソリティアは写真のようなゲームです.石を1つ飛び越すと飛び越された石を取り除くことができます.これを繰り返して最後1つだけにすることが目的です.

これを Pthread Model Checker を使って解いてみます.本来の十字形だと状態数的に厳しいので,5 x 5 の正方格子でやってみることにします.

0  どうしてモデル検査ツールでパズルが解けるのか?

どうして Pthread Model Checker でパズルが解けるのかというと,モデル検査ツールは原理的に探索機械だからです.ゲームの状態と遷移をモデル化して,ゴールの条件を assert にすれば探索してくれます.

1  モデル

さっそくモデルを見てもらいましょう.状態を減らすために,ややハードコード気味です.

石の配置を 5 x 5 = 25 bit の整数で表します.初期状態は 0x01FFFF7F で,1ヶ所だけ空いている状態です.

ここからはじめて以下のことを繰り返します.

  1. 非決定的選択構文 AMB を使ってボード上の位置 (x, y) を任意に1つ選びます.
  2. 次に上下左右の方向を任意に選びます.
  3. 選んだ方向に飛越しができる場合は飛び越します.

そして,最後に1つだけになった状態 0x20000 になることはないという assert を入れます.

const int N = 5;
uint32_t g;

uint32_t bit(int8_t x, int8_t y)
{
    return 1 << (x + y * N);
}

int main(void)
{
    g = 0x01FFFF7F;
    while (true) {
        int8_t x, y;
        AMB x = 0; OR AMB x = 1; OR AMB x = 2; OR AMB x = 3; OR x = 4;
        AMB y = 0; OR AMB y = 1; OR AMB y = 2; OR AMB y = 3; OR y = 4;
        uint32_t m = g;
        assert(m != 0x20000);
        if (m & bit(x, y)) {
            AMB {
                if (y >= 2 && (m & bit(x, y - 1)) && !(m & bit(x, y - 2))) {
                    g = (m & ~(bit(x, y) | bit(x, y - 1))) | bit(x, y - 2);
                }
            } OR AMB {
              if (y < N - 2 && (m & bit(x, y + 1)) && !(m & bit(x, y + 2))) {
                  g = (m & ~(bit(x, y) | bit(x, y + 1))) | bit(x, y + 2);
              }
            } OR AMB {
                if (x >= 2 && (m & bit(x - 1, y)) && !(m & bit(x - 2, y))) {
                  g = (m & ~(bit(x, y) | bit(x - 1, y))) | bit(x - 2, y);
              }
            } OR {
              if (x < N - 2 && (m & bit(x + 1, y)) && !(m & bit(x + 2, y))) {
                  g = (m & ~(bit(x, y) | bit(x + 1, y))) | bit(x + 2, y);
              }
            }
        }
    }
    return 0;
}

2  解

検査を実行すると 388 ステップの解が見つかります.内部計算の遷移があるので 24 ステップというわけにはいきません.状態数は 176,995,157 状態でした.

パスから変数の値だけ取り出して,ボードっぽく加工しました.

----------------
 O  O  O  O  O 
 O  O     O  O 
 O  O  O  O  O 
 O  O  O  O  O 
 O  O  O  O  O 
----------------
 O  O  O  O  O 
 O  O  O  O  O 
 O  O     O  O 
 O  O     O  O 
 O  O  O  O  O 
----------------
 O  O  O  O  O 
 O  O  O  O  O 
       O  O  O 
 O  O     O  O 
 O  O  O  O  O 
----------------
    O  O  O  O 
    O  O  O  O 
 O     O  O  O 
 O  O     O  O 
 O  O  O  O  O 
----------------
    O  O  O  O 
 O  O  O  O  O 
       O  O  O 
    O     O  O 
 O  O  O  O  O 
----------------
       O  O  O 
 O     O  O  O 
    O  O  O  O 
    O     O  O 
 O  O  O  O  O 
----------------
       O  O  O 
 O     O  O  O 
 O        O  O 
    O     O  O 
 O  O  O  O  O 
----------------
       O  O  O 
 O     O  O  O 
 O     O       
    O     O  O 
 O  O  O  O  O 
----------------
       O  O  O 
 O     O  O  O 
 O     O  O    
    O        O 
 O  O  O     O 
----------------
       O  O  O 
 O     O  O  O 
 O  O          
    O        O 
 O  O  O     O 
----------------
    O        O 
 O     O  O  O 
 O  O          
    O        O 
 O  O  O     O 
----------------
    O        O 
       O  O  O 
    O          
 O  O        O 
 O  O  O     O 
----------------
    O        O 
       O  O  O 
 O  O          
    O        O 
    O  O     O 
----------------
    O          
       O  O    
 O  O        O 
    O        O 
    O  O     O 
----------------
    O          
    O  O  O    
 O           O 
             O 
    O  O     O 
----------------
               
       O  O    
 O  O        O 
             O 
    O  O     O 
----------------
               
       O  O    
       O     O 
             O 
    O  O     O 
----------------
               
          O    
             O 
       O     O 
    O  O     O 
----------------
               
          O  O 
               
       O       
    O  O     O 
----------------
               
          O  O 
               
       O       
          O  O 
----------------
               
          O  O 
               
       O       
       O       
----------------
               
       O       
               
       O       
       O       
----------------
               
       O       
       O       
               
               
----------------
               
               
               
       O       
               
----------------

2017/10/20

© 2013-2017 PRINCIPIA Limited