pub fn ramsey(s: usize, t: usize, n: usize) -> (DimacsCnf, ExpectedVerdict)Expand description
The Ramsey formula Ramsey(s, t; n): 2-colour the edges of the complete graph K_n (one
Boolean per edge — true = red, false = blue) avoiding every red K_s and every blue K_t. For each
s-clique a clause forbids all its edges being red; for each t-clique a clause forbids all blue.
Such a colouring exists iff n < R(s, t), so the formula is UNSAT exactly when n ≥ R(s, t).
A genuinely different geometry from pigeonhole/parity — clique structure, not covering or counting —
and a classic CDCL stress family (Ramsey(3,3;6) is the smallest UNSAT case). Panics for (s, t)
whose Ramsey number is unknown (so the verdict is never guessed); see ramsey_number.