CNF Ramsey

Creates problem statements about Ramsey's theorem in CNF in the DIMACS format. Blog post here.

Requirements

This program is written in Rust.

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. 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 is not 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.