#112: the directed Ramsey number k(3,4) is exactly 21

The problem (erdosproblems.com/112, OPEN). Write k(n,m) for the least N such that every oriented graph on N vertices contains an independent set of size n or a transitive tournament of order m. Erdős asked for its growth; nobody knows it. The exact values are scarce: k(3,3) = 9, and for k(3,4) the certified interval in our August report was 21 ≤ k(3,4) ≤ 25, the lower bound from eight explicit cyclic 20-vertex witnesses, the upper bound from the literature (the Ihringer–Rajendraprasad–Weinert bound of 24 having been withdrawn). Six order-21 SAT instances, one per "root profile", were left unresolved after minutes of solver time.

The split. Take any vertex v of a hypothetical 21-vertex witness. Its out- and in-neighbourhoods are oriented graphs with no independent triple and no transitive triangle (else v completes an I₃ or an L₄), so each has at most 8 vertices; its non-neighbourhood is a tournament (two non-neighbours of v that are non-adjacent form an I₃ with v) with no transitive 4-subtournament, so at most 7 vertices. That gives the six profiles. The step the August run missed: those neighbourhoods have very few shapes. Up to isomorphism there is exactly one (I₃,L₃)-free oriented graph on 8 vertices, 7 on 7 vertices, 31 on 6, 25 on 5; and exactly one L₄-free tournament on 7 vertices (Paley) and one on 6. We counted them twice, by unrelated methods — SAT enumeration with orbit blocking, and nauty's graph generator over underlying graphs with independence number ≤ 2 and no K₄ followed by all cyclic-triangle orientations — and the counts agree. Fixing each neighbourhood of v to a labelled copy of each type is lossless (relabel inside each part), so order 21 is exactly 3 + 21 + 31 + 49 + 25 + 217 = 346 cases, each with the only free decisions being the pair states between the three parts.

The run. Every case is a DIMACS file written from the definition (one state per pair, no independent triple, no transitive 4-set) plus the valid redundant degree bounds. On 274 of the 346 cases cadical returned UNSAT inside the per-case budget, with DRAT proof logging, and drat-trim replayed every proof to s VERIFIED. The remaining 72 timed out plain, and all 72 are cases whose fixed neighbourhoods have symmetry (the Paley tournament on 7 vertices alone has an automorphism group of order 21). Every automorphism of a fixed part extends to an automorphism of that case's CNF, so adding the lex-leader constraints x ≤_lex σ(x) for every non-identity σ in Aut(N⁺) × Aut(N⁻) × Aut(N⁰) (Crawford–Ginsberg–Luks–Roy; group orders 3 to 3,528 here) keeps at least one solution of every orbit. A cadical/kissat race then closed all 72 symmetry-broken cases, the longest in under seven minutes, again with DRAT proofs replayed by drat-trim. Total solver time 51.4 CPU-hours, longest case 2163 s, on a 16-core box at low priority.

Controls. The same generator at order 20, pointed at the exact case of one of the known cyclic witnesses (connection set {1, 2, 4, 14, 15, 17}, root profile (6,6,7)), returns SAT and the model validates from the definition — so the encoding is not over-constrained — and it stays SAT with a valid model after the same symmetry breaking (its non-neighbourhood is the Paley tournament, so it carries a group of order 21). The symmetry breaking also has a per-case control: for each of the 72 cases, random cross-part pair-state vectors were orbited under an independently recomputed group, and the appended clauses accepted the lex-minimum of every orbit and rejected the lex-maximum and a random other member (219 draws, 0 failures) — the extra clauses lose nothing and are not vacuous. Four of the 72 (p776_o6_i6_n0, p767_o2_i13_n0, p767_o6_i26_n0, p767_o6_i29_n0 — group orders 147, 21, 147 and 588) were also re-run plain with a four-hour budget as a decorrelated check: all four UNSAT in 15–21 minutes, every proof replayed by drat-trim to s VERIFIED.

Therefore no 21-vertex oriented graph is (I₃,L₄)-free, and with the 20-vertex witnesses, k(3,4) = 21.

Labels and what isn't claimed. The reduction and the type census are elementary plus an exhaustive enumeration with two independent implementations; the 346 UNSATs are (d) computer-assisted with machine-checked proofs, 72 of them resting additionally on the lex-leader theorem (standard, and tested per case). This is one exact value in a table the problem asks to understand asymptotically; it says nothing about k(n,m) in general. We found no publication of the value; the question "instead asks for r(I₃,L₄)" in the Ihringer–Rajendraprasad–Weinert paper is exactly this number. No priority claim beyond that.