# SAT-based solver

- minisatを使って配置配線パズルを解くよ

- 定数
    - 盤面幅 W
    - 盤面高 H
    - ブロック数 N
    - ライン数 M


### 変数リテラル
- 変数リテラルは2種類
    -  ブロック配置 bn_x_y
    -  ライン配線 lm_x_y
    - WH(N+M)個のリテラル

##### ブロック配置
- bn_x_y
    - 1 <= n <= N
    - 0 <= x < W
    - 0 <= y < H
    - e.g. ```b1_0_2=1```はブロック1を座標(0,2)に配置することを意味する


##### ライン配線
- lm_x_y
    - 1 <= m <= M
    - 0 <= x < W
    - 0 <= y < H
    - e.g. ```l1_0_2=1```は座標(0,2)のマスをライン1で配線することを意味する


### 制約
- ブロックone-hot 制約
- ライン重複禁止制約
- ブロックの盤面はみ出し禁止制約
- ブロック上のライン位置決定制約
- ブロック重複禁止制約
- 端点制約(ブロック上のラインは2個以上接続してはいけない)
- ライン孤立禁止制約
- 非端点制約(ブロック上にないラインは2個以上接続しないといけない)
- ライン三叉禁止制約