Added README.md

1 files changed, 19 insertions, 0 deletions

diff --git a/README.md b/README.md
new file mode 100644
index 0000000..f5cfd58
--- /dev/null
+++ b/README.md
@@ -0,0 +1,19 @@
+## CNF Ramsey
+
+Creates problem statements about Ramsey's theorem in CNF in the DIMACS format.  More information [here](https://jgh.xyz/posts/cnf_ramsey).
+
+## Requirements
+
+This program is written in Rust.
+
+[inline-python](https://docs.rs/inline-python/latest/inline_python/) requires Python 3.10 specifically.  Newer versions of Python don't work.  I plan to remove this dependency at some point for this reason.
+
+## Use
+
+`cargo run --release <clique size> <complete graph size> <output filename>`
+
+Example: `cargo run --release 4 17 out.cnf`
+
+The generated file can be passed to a SAT solver, like [cryptominisat](https://github.com/msoos/cryptominisat).  The SAT solver will either find that the statement is satisfiable and produce a counterexample, or that the statement isn't satisfiable.  If the statement is satisfiable, `R(r,r) > n`.  If the statement isn't satisfiable, `R(r,r) <= n`.
+
+This program will also print a labelling of the edges of the complete graph.  Any labelling of the vertices can be chosen.