Attack log — Seymour's second-neighborhood conjecture
2026-08-17 — start
- Folder empty except
PROBLEM.md. House: write only here; no git; cite what we beat; no invented dent. - Conjecture (Seymour, ~1990; Dean–Latka 1995): every oriented graph has a vertex with .
- Tonight: a certified new small-order census, a new reducible configuration with an independently checkable certificate, or a proof for another hereditary class. Isolated random-graph statistics are residue.
Published record (fetched tonight)
| claim | source | status |
|---|---|---|
| tournaments | Fisher 1996; Havet–Thomassé 2000 | theorem |
| Seymour vertex nearby | Kaneko–Locke, Congr. Numer. 148 (2001) | theorem; implies all |
| Sadhukhan–Sandeep–Sen, arXiv:2606.30588 (29 Jun 2026) | preprint; CP-SAT after local reductions | |
| Brukhman, arXiv:2608.11530 (12 Aug 2026) | preprint; counting. Combined with Kaneko–Locke: any counterexample has . Combined with SSS: | |
| every orientation of for fixed | Espuny Díaz–Girão–Granet–Kronenberg, arXiv:2403.02842 | theorem; is equivalent to the full conjecture |
| missing matching / star / clique | Fidler–Yuster 2007 | theorem |
| missing generalised star | Ghazal 2012 | theorem |
| missing matching + star | Dara–Francis–Jacob–Narayanan 2022 | theorem |
| missing two stars; missing disjoint paths | Daamouch–Ghazal–Al-Mniny, arXiv:2406.03635 | theorem / partial |
| Pisa graphs | Halkiewicz, arXiv:2601.21563v3 (21 May 2026) | computational; labeled counts 1050 (), 4080 () |
| Seymour-tight constructions (cycle powers, lex products) | Guo–Kang–Zwaneveld, arXiv:2603.29626 (31 Mar 2026) | theorem; is tight for |
A Pisa graph (Halkiewicz) is a strongly connected oriented graph with . A Seymour-tight orientation (Guo–Kang–Zwaneveld) has every margin exactly 0; the strong ones are Pisa.
Halkiewicz Conjecture 5.1 says every Pisa graph has underlying graph or minus a matching. Their own table already lists 720 labeled Pisa graphs whose missing-edge graph is 2-regular — not a matching. Guo–Kang–Zwaneveld's directed cycle-square is such an example. So the stated matching conjecture is already false at the order they computed; the live computational question they pose is the census (their open problem (3)).
Wikipedia still quotes Kaneko–Locke . Brukhman (five days ago) is the current order bound if one accepts only refereed theorems.
Plan
- Independently recompute Halkiewicz's labeled Pisa counts for , and check the cycle-power / lex-product examples.
- Certified census of Pisa graphs at (the first open order), with a replayable enumerator and a per-graph verifier. Classify underlying / missing graphs.
- In parallel: try (Brukhman says the same counting dies) or a missing-cycle class (not covered by Fidler–Yuster / Dara / Daamouch).
- If the census does not finish or does not beat a published number, leave the residue and do not claim a bound.
Local PDFs: compute/refs/.
2026-08-17 — published constructions replayed
compute/check_known.py confirms Guo–Kang–Zwaneveld Lemma 2.1: is Seymour-tight iff . In particular is a Pisa graph whose missing graph is 2-regular, so Halkiewicz Conjecture 5.1 (underlying or minus a matching) is already false at the order they enumerated. Their own Table 2 lists those 720 graphs. The live question is the census and any genuine new class.
and are Pisa on 8 vertices with 3-regular missing graph.
2026-08-17 — labeled Pisa census
compute/enum_pisa.c (OpenMP bitmask) independently reproduced Halkiewicz:
| n | labeled oriented | Pisa | tight | types (missing-degree : count) |
|---|---|---|---|---|
| 4 | 729 | 6 | 6 | : 6 |
| 5 | 59049 | 48 | 48 | : 24, : 24 |
| 6 | 14348907 | 1050 | 270 | matches Halkiewicz Table 1 exactly |
| 7 | 10460353203 | 4080 | 4080 | : 720, : 720, : 2640 |
n=7 wall time 217s. New observation not in Halkiewicz: every Pisa graph on 7 vertices is Seymour-tight; on 6 vertices only 270/1050 are. All oriented graphs have , as Kaneko–Locke already implies.
This is a replay, not a dent. n=8 labeled () is ~130 core-hours at this rate.
2026-08-17 — the click: Brukhman's next layer is Eulerian
Brukhman proves every oriented graph with has a Seymour vertex. At the same double count gives only and , no contradiction.
If a counterexample at is out-regular of degree , then and the missing graph has average degree 2. If it is also in-regular (Eulerian), the missing graph is a 2-factor and the Brukhman capacity bound is forced to equality:
- , for every v
- , is a directed 3-cycle inside the trap
- dominates
Further: with sizes , , 3 forces where are the two missing neighbours and is a fixed-point-free permutation (a 2-factor of directed cycles of length ). Then always contains both missing neighbours of x. So the missing 2-factor has no 3-cycles (else those two plus cannot form a tournament).
This is a finite, rigid obstruction. CP-SAT on the raw Eulerian constraints (no symmetry breaking) says the obstruction is empty for every we have finished:
| δ | n=2δ+3 | OR-Tools | time |
|---|---|---|---|
| 2 | 7 | INFEASIBLE | 0.02s |
| 3 | 9 | INFEASIBLE | 0.11s |
| 4 | 11 | INFEASIBLE | 2.7s |
| 5 | 13 | INFEASIBLE | 42s |
δ=6 (n=15) is running. Independent Cadical replay of the same claim is in regular_dense_cnf.py.
This is not yet a general theorem. It is a certified finite-δ theorem: every Eulerian oriented graph with n=2δ+3 and δ≤5 has a Seymour vertex. Combined with Brukhman, every Eulerian oriented graph with n≤2δ+3 and δ≤5 is covered. The interesting range is δ≥7 (else Kaneko–Locke), so we still need δ=7 (n=17) or a human proof of the equality case.
2026-08-17 — n=8 types (the dent)
Kaneko–Locke already implies every Eulerian graph with has a Seymour vertex, so the Eulerian SAT for is only a sanity check of Brukhman's equality layer, not a new bound. Cadical independently confirmed UNSAT for after a top_id bug made an earlier CNF trivially empty. OR-Tools timed out. That residue is documented; it does not beat Kaneko–Locke.
The live dent is the first order Halkiewicz left open.
CEGAR SAT, each witness rechecked by seymour.py bitmasks:
| missing-degree type | tight? | matching? | certificate |
|---|---|---|---|
| yes | no | certs/n8_miss5regular.json (directed ) |
|
| yes | no | certs/n8_miss3regular.json ( / SAT) |
|
| no | no | certs/n8_miss2regular.json |
|
| no | no | certs/n8_miss22333333.json |
|
| no | no | certs/n8_irregular_pisa.json |
|
| — | — | SAT INFEASIBLE at 30s | |
| — | — | SAT INFEASIBLE (underlying 1-regular cannot be strong) |
The last two feasible rows are irregular missing graphs. The witness has missing edges
{04,07,14,17,23,25,26,35,36}
i.e. a 4-cycle on plus on . Margins (0,-1,0,0,-1,-1,0,0). This is forbidden by Halkiewicz Conjecture 5.1 and by the “regular missing edges” pattern that held for all 4080 labeled Pisa graphs on 7 vertices.
n=8 is also the first order with non-tight Pisa graphs that are not just minus a matching (n=6 already had non-tight matching-minus examples; n=7 had none).
geng -q 8 | enum_pisa_geng finished. 12346 unlabeled undirected graphs, orientations of representatives, 162 Pisa orientations, exactly seven missing-degree types:
| missing-degree | Pisa orients on a geng rep | example cert |
|---|---|---|
| 2 | n8_miss5regular.json (directed ) |
|
| 20 | n8_miss3regular.json |
|
| 12 | n8_miss22333333.json |
|
| 32 | n8_miss33222222.json |
|
| 16 | n8_irregular_pisa.json |
|
| 32 | n8_miss2regular.json |
|
| 48 | n8_miss1regular.json () |
Absent, and therefore not Pisa at this order: tournaments ; 4-regular missing; 6-regular missing; incomplete matchings for . The last is a genuine n=8 phenomenon — n=6 has Pisa orientations of minus one or two edges.
Summary file: certs/pisa_n8_types.json. Every listed type has a bitmask-verified witness.
This is a certified new small-order census. It beats Halkiewicz's n=7 census (first new order) and both of his structural claims (matching conjecture; regular-missing pattern).
2026-08-17 — what is not claimed
- The full labeled n=8 count (that is and ~130 core-hours at the n=7 rate). The 162 figure is orientations of nauty representatives, not labeled graphs.
- A general proof of Eulerian .
- Any improvement of Kaneko–Locke or Brukhman .
- SSS was not rechecked.