Skip to content

Bounded-Domain Exhaustive Search

Exhaustive-search tool — instantiates Computability Boundary Mapping

Turns a question that is undecidable in general into a decidable one by fixing a finite bound and mechanically checking every case inside it.

When a class is undecidable or intractable in general, one honest response is to stop asking the general question. Bounded-Domain Exhaustive Search fixes a finite bound — inputs up to size k, boards of n cells, traces of depth d — and then simply checks every case inside that fence. Its defining property is that correctness within the bound is total and certificate-bearing: nothing is estimated, nothing is approximated, every case is actually examined, so a "no counterexample exists" verdict is airtight — but only up to the fence, and completely silent beyond it. The bound is both the entire trick that restores decidability and the entire limit on what the result can claim.

Example

What is the fewest given clues a Sudoku puzzle can have and still admit a unique solution? The space of clue-arrangements is finite but astronomically large, so the question is decidable in principle yet far too big to reason about by hand. A large exhaustive computer search settles it by construction: it enumerates every essentially distinct arrangement of sixteen clues and checks each for a unique completion, finds that none qualifies, and thereby establishes that the minimum is seventeen. The answer is exact and complete — within the bound of sixteen clues. It says nothing, and claims nothing, about any other question; its authority comes entirely from having actually looked at every case in a precisely delimited space.

How it works

The mechanism enumerates the entire finite instance space that the bound defines, tests each case against the property, and aggregates the results. Termination is guaranteed by finiteness alone — not by any insight into the problem — which is exactly why it works where cleverness fails. Symmetry reduction (collapsing equivalent cases) and pruning (skipping provably empty branches) shrink the space dramatically but change nothing about the guarantee: the claim still covers every case, just enumerated more efficiently. The one non-negotiable is a precise encoding of the instance space, so that "every case" is unambiguous and no case is missed or double-counted.

Tuning parameters

  • Bound size — how large the finite fence is. A larger bound makes a stronger claim but usually costs exponentially more; this is the dial that trades reach against feasibility.
  • Symmetry reduction — how aggressively isomorphic cases are collapsed into one representative. Strong reduction can shrink the space by orders of magnitude without weakening the result.
  • Pruning and ordering — which branches are skipped as provably irrelevant and in what order the rest are visited; good ordering finds a witness (if any) sooner.
  • Witness retention — whether the search keeps the actual case it found or returns only a yes/no. Retaining the witness makes the result independently checkable.

When it helps, and when it misleads

Its strength is a complete, checkable answer that needs no cleverness — ideal when the genuinely interesting cases are provably finite, and often the fastest route to certainty in a bounded regime. Its failure modes are the flip side of brute force: state-space explosion[1] means the finite space is frequently too large to finish, and — crucially — a result never generalizes past the bound. Checking up to k says exactly nothing about k+1. The classic misuse is presenting "verified up to bound k" as though it settled the unbounded claim — the bounded-model-checking trap, where a clean finite result is quietly promoted to a universal one. The discipline is to report the bound alongside the result, always, and to treat everything outside it as unestablished.

How it implements the components

  • termination_condition — finiteness of the bounded space is the termination guarantee: the search halts because there are only finitely many cases to examine.
  • instance_representation_contract — it must pin an exact encoding of the finite instance space so that "check every case" is well-defined, exhaustive, and free of gaps or duplicates.

Outside the fence it says nothing — the unbounded "yes-or-run-forever" case belongs to Enumeration and Dovetailing, and whether the unbounded class is decidable at all is settled by Constructive Algorithm and Correctness Proof or Diagonalization Impossibility Proof; this tool decides only inside a finite bound.

References

[1] State-space explosion — the number of configurations grows exponentially in the problem's parameters, so a search that is finite in principle can be wholly infeasible in practice. It is the standard limit on how far a bound can be pushed. ↩