blob: f5cfd5829d637ae3d3cfe1d54c4c2d74ec0818ff (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
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.
|
