THE NONACUBE TWO-CORONA SEARCH
Explore the search tree
Open folders to follow a decision path. Select a conflict leaf to inspect the exact 3D state where that visit failed.
Long single-child paths are compacted. Use Choices to inspect every decision in one. Folders load as you open them.
What this tree represents
This is the actual conflict-learning SAT traversal, grouped into 2,556 search phases. Each decision visit is a folder; each of the 529,855 recorded conflicts is a numbered leaf. Backjumps and the final contradiction are also selectable entries. Every recorded event appears exactly once.
Learned clauses can exclude whole families of branches without visiting them, and a restart can revisit an assignment with additional learned constraints. The directory records those visits; it does not invent the unvisited branches of a plain binary search tree. Branch counts mean recorded conflict leaves below that folder.
A conflict state can contain overlapping selected tiles before the solver detects the contradiction. The preview marks such overlaps in pink. The largest nonoverlapping connected patch at a settled decision state has 39 crosses, including the root, and covers 77 of the 90 root-surround cells.
Tree index · Reproduction and verification · Checked proof receipt