make an executable file

.gitignore

@@ -1 +1,5 @@
 .ipynb_checkpoints/
+*.cnf
+*.sat
+*.unsat
+*.out

README.md

@@ -4,6 +4,13 @@
 
 - [fire](https://github.com/google/python-fire) python library
   - Either manually install it or use [pipenv](https://pypi.org/project/pipenv/)
-- [kissat](https://github.com/arminbiere/kissat) in `$PATH`
+- [kissat](https://github.com/arminbiere/kissat) installed and located in `$PATH`
 
 ## Usage
+
+```
+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.

lib/sat.py

@@ -89,9 +89,11 @@ def load(self, filename):
 
     def solve(self, filename="tmp"):
         self.write(f"{filename}.cnf")
-        out_code = os.system(f"kissat {filename}.cnf > {filename}.sol")
+        out_code = os.system(f"kissat {filename}.cnf {filename}.unsat > {filename}.out")
         if out_code != 2560:
             return False
-
-        self.load(f"{filename}.sol")
-        return True
+        else:
+            os.system(f"rm {filename}.unsat")
+            os.system(f"mv {filename}.out {filename}.sat")
+            self.load(f"{filename}.sat")
+            return True

main.py

@@ -1 +1,15 @@
 # TODO: copy the jupyter notebook codes to here, make it reproducable
+
+import os
+import fire
+import lib.erdos as erdos
+from lib.util import binom
+
+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 __name__ == '__main__':
+    fire.Fire(main)