From 1da47298415b36decb8bbd669a64f4a40b993662 Mon Sep 17 00:00:00 2001
From: tawada <tawada@togawa.cs.waseda.ac.jp>
Date: Tue, 23 Jul 2019 14:58:54 +0900
Subject: [PATCH] Update README.md

---
 README.md | 47 ++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 46 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 05fb80c..4c6c65b 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個以上接続しないといけない)
+- ライン三叉禁止制約
+
+
+
 
 
-- 
2.22.0