counterexample depth per candidate
Keep this diagram
Discard
The two searches
Fill undecided cells completes the diagram on screen.
Every marker you have set is held fixed and only the undecided cells
are searched; erase a cell (right-click) to have it re-derived. Each
SAT model is a candidate, the exhaustive verifier turns every losing
line into a clause, and only a diagram that passes the full check is
offered.
It completes diagrams; it does not solve open roots.
On a ply-16 root, four undecided cells finish in about 20 candidates,
twelve in about 560 and fourteen in about 3,900; past about fourteen it
usually will not converge. A bare root with everything undecided ran
8,919 candidates in 20 seconds without getting there, and a faster
solver would not change that: the limit is how little each
counterexample rules out, not throughput. Because your markers bound
the search, an UNSAT here means no completion of those markers
wins, not that the root is impossible.
Solve whole root is the native engine. It holds your
decided cells fixed too, so it also only fills in the undecided ones,
but it goes about it in a completely different way: it maps out every
position the diagram could ever face and decides them together, rather
than proposing a diagram and testing it. That makes it strong exactly
where auto-complete is weak — a deep root with little decided
— and useless on a shallow one, where the map is too big for a
browser. Undecide everything and its UNSAT is about the root itself,
across the entire strict language. Neither verdict has been
independently audited.