Solver engineering: invariants, bounds, and minimal verification

Mechanism

A CTF solver is a model of the problem, not just a search loop. Define variables, constraints, and verification conditions before optimizing. Exact arithmetic, explicit bounds, and independent checks make failures interpretable. A candidate found by a heuristic should be validated against the original equations or challenge behavior.

Practical method

Build a tiny fixture with a known answer and test the model on it. Add assertions for dimensions, inverses, lengths, and congruences. Log progress in meaningful units and distinguish exhausted search from invalid assumptions. Save candidates and run a separate verifier.

assert 0 <= candidate < modulus
assert pow(candidate, exponent, modulus) == target
# Independent verification follows candidate generation.

Interpreting evidence

A solver report should state assumptions, explored bounds, and the verification result. Runtime improvement is useful only if it preserves the intended search space and exact semantics.

Pitfalls and limits

Overconstrained alphabets hide solutions. Floating-point approximations can corrupt lattice or number-theory inputs. Parallel workers need deterministic task partitioning to avoid missing or duplicating ranges.