diff --git a/README.md b/README.md index 05fb80cc56e4d752af8e55414d58d03fc2937c04..4c6c65bbaa4ab5e4702dd5a1108bb8f3e943af18 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,48 @@ -# twd-solver +# 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個以上接続しないといけない) +- ライン三叉禁止制約 + + +