update program + readme

README.md

@@ -1,4 +1,27 @@
-# An SAT encoding of Erdos-Szekeres conjecture
+# An SAT encoding of Erdős-Szekeres conjecture
+
+This program is a part of a research paper by 
+[Jineon Baek](https://jcpaik.github.io/) and [Martin Balko](https://kam.mff.cuni.cz/~balko/) 
+in preparation.
+
+The _Erdős–Szekeres conjecture_ states that 
+$2^{n-2} + 1$ points on a plane, with no three on a line,
+should contain a set of $n$ points forming the vertices of a convex polygon.
+This software solves a hypergraph generalization of the problem defined as the following.
+
+- The input values are $n, a, b$ and $N$.
+- Every subsets of size 3 of the set $[N] = \{1, 2, \dots, N\}$ should be colored by either red or blue.
+- Any increasing sequence $1 \leq a_1 < \cdots < a_m \leq N$ is a _red chain_ (resp. _blue chain_) if the set of each three consecutive values $\{a_i, a_{i+1}, a_{i+2}\}$ is colored red (resp. blue).
+- A pair of a red chain of length $a$ and a blue chain of length $b$ sharing the same leftmost and rightmost value is called an _$n$-gon_ where $n = a + b - 2$. 
+
+The program either 
+
+- finds a coloring of all size 3 subsets of $[N]$ with no $n$-gon, red chain of size $a$ or blue chain of size $b$
+- or prove that no such coloring exists
+
+using the [Kissat](https://github.com/arminbiere/kissat) SAT solver.
+
+More details on why is this problem a generalization of the Erdős–Szekeres conjecture will be in our upcoming draft.
 
 ## Dependencies
 
@@ -11,6 +34,19 @@
 ```
 python main.py n a b N
 ```
-checks if `N` points with no `n`-gon, `a`-cap and `b`-cup exists. The SAT
-instance is produced as `cnf` file, and either the solution or unsatisfiabilty
-proof is generated as `.sat` or `.unsat` file respectively.
+
+If using pipenv, one can run `pipenv install` and then `pipenv shell` 
+then run the command above. 
+Otherwise, one should install the [fire](https://github.com/google/python-fire) python library.
+
+If a coloring exists, the program stores a coloring in `.color` file, which is a text file
+with each line `i j k C` denoting the coloring `C` (either `R` or `B` for red or blue respectively) 
+of the set $\{i, j, k\}$.
+If a coloring does not exist, the program stores a proof of unsolvability in `.unsat` file.
+
+The default `filename` used is `etv_n_a_b_N` where the corresponding values of n, a, b and N are replaced with their actual values. This can be overriden using `--filename` option.
+
+The program also spawns the following files as well.
+
+- `filename.cnf` for the actual SAT instance used
+- `filename.out` for the output of the Kissat solver

lib/sat.py

@@ -90,7 +90,8 @@ def load(self, filename):
     def solve(self, filename="tmp"):
         self.write(f"{filename}.cnf")
         out_code = os.system(f"kissat {filename}.cnf {filename}.unsat > {filename}.out")
-        if out_code != 2560:
+        successful = (out_code == 2560)
+        if not successful:
             return False
         else:
             os.system(f"rm {filename}.unsat")

main.py

@@ -9,7 +9,17 @@ def main(n, a, b, N, filename=None, signotope=False):
     inst = erdos.etv(n, a, b, N)
     if not filename:
         filename = f"etv_{n}_{a}_{b}_{N}"
-    inst.solve(filename)
+    if inst.solve(filename):
+        print("Solution found")
+        sol_filename = filename + ".color"
+        with open(sol_filename, "w") as f:
+            for triple, var in inst.v.items():
+                color = 'R' if var.solution() else 'B'
+                line = f"{triple[0]+1} {triple[1]+1} {triple[2]+1} {color}"
+                f.write(line + "\n")
+        print("Solution stored in " + sol_filename)
+    else:
+        print("Solution not found")
 
 if __name__ == '__main__':
     fire.Fire(main)