Loading README.md +46 −1 Changes for README.md: 46 added lines, 1 removed line. Original line number Diff line number Diff line # 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個以上接続しないといけない) - ライン三叉禁止制約 Loading
README.md +46 −1 Changes for README.md: 46 added lines, 1 removed line. Original line number Diff line number Diff line # 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個以上接続しないといけない) - ライン三叉禁止制約
