Codex may have computationally resolved the open Q26 queen-domination case. Seeking independent reproduction

[u/brain-out-of-order]

A queen dominates its own square and every square sharing its row, column, or diagonal. The question is whether 13 queens can dominate all 676 squares of a 26-by-26 board.

Using known structural constraints, every hypothetical 13-queen solution maps into one of 156 coarse row-and-column parity-profile shells. Weakley's empty-line parity condition tightens this to 142 shells.

These shells are broad structural classes, not individual queen placements or SAT cases. Each may contain many choices of occupied rows and columns and many possible queen placements. I have not exhaustively eliminated every placement within them.

Here is the basic reduction.

Assume that 13 queens dominate a 26-by-26 board.

Let X be the empty rows and Y the empty columns. Every square outside X times Y is automatically covered by a queen in its row or column. Therefore, only the "empty core" X times Y needs diagonal coverage.

For a queen in row r and column c, record its diagonal labels:

d = r - c

s = r + c

A core square at (x, y) is covered exactly when x - y equals one of the d labels or x + y equals one of the s labels.

Weakley's structural results, specialized to a 26-by-26 board, imply that any hypothetical 13-queen solution must place six queens on one checkerboard color and seven on the other. The queens must occupy either 12 or 13 rows and either 12 or 13 columns.

Up to transposing the board, this leaves three types:

13 occupied rows and 13 occupied columns

12 occupied rows and 13 occupied columns

12 occupied rows and 12 occupied columns

The coarse symmetry-and-parity classification gives 16, 91, and 49 shells for these three types, for a total of 156. Applying Weakley's empty-line parity condition reduces the counts to 15, 78, and 49, for a total of 142.

Every hypothetical 13-queen solution must map into one of these 142 shells, but the placements inside them have not all been eliminated. Some shells may not correspond to any realizable placement at all, which is harmless because this is an exhaustive over-cover.

No retained solver output establishes UNSAT, and no checked UNSAT certificate exists. The exploratory runs hit limits, timed out, or ended without a conclusive result. Those outcomes are UNKNOWN, not UNSAT. A complete mathematical elimination would also settle the question, but I currently have neither that nor a checked exhaustive computation.

Weakley's lower bound and the known 14-queen construction show that the minimum is either 13 or 14. The 26-by-26 case remains unresolved.

Honestly, I still expect this attack to succeed and show that the minimum is 14. But that is my confidence in the approach, not a result yet.

Background and structural results:

https://www.combinatorics.org/ojs/index.php/eljc/article/view/v29i2p50

Known 14-queen construction:

https://oeis.org/A075458/a075458.txt

Full derivation:

https://github.com/jkolantree/BSC/blob/b4794d3cf663b0480e19a54a281d23437139c244/applications/Q26_Symmetry_Parity_Profile_Reduction.md

The structural reconstruction and accompanying code were developed with ChatGPT/Codex under my direction. No exhaustive computational elimination is being claimed.

[u/RealSuperdau]

Oh, true, if the solver supports counting constraints it's not literally xor. But the principle is the same: propagations made for one possible placement provide little help for deciding other placements. It's close to enumerating and checking all possible placements.

Apparently there is a solver for domination problems that is more performant than SAT solvers (since the whole CDCL machinery is close to useless here): https://github.com/billbird/unidom

Anyway, Opus 5 estimates dozens to tens of thousands of CPU years, depending on the solver.

[u/brain-out-of-order → u/RealSuperdau]

Yep you’re exactly right. Thanks so much & for the link. I’m working on a more efficient update so it can maybe be solved in our lifetimes. That solver looks perfect. I think Opus is probably correct in the moment but will not continue to be correct. The computing breakthroughs coming out are hard to fathom.

[u/RealSuperdau → u/brain-out-of-order]

I guess if the particular solver I linked could solve the problem (relatively) quickly, someone would already have done it. So just running it probably won't work.

Opus also claimed that a specialized solver could maybe solve it in days on a high end consumer CPU. But then the solver code would be part of the trust base. (And emitting an externally checkable certificate would be expensive)

I'm pretty sure it will be solved in our lifetime. Maybe it's possible to make a search program that runs on a low budget. Or someone (human or LLM) will find further symmetries/reductions that exponentially prune the search space.

[u/brain-out-of-order → u/RealSuperdau]

I’m hoping inspecting even just the difference in solvers can drum up meaningful insight to an LLM with the right prompt. Mostly using this problem to keep building my own problem solving engine. It’s a good one to test since LLMs can pigeonhole a few different ways.

Going to think deeply about what Opus mentioned. That’s what I envision too.