Engineering a witness finder: certified gate elimination, treewidth, and affine-subspace refuters in practice

Gate elimination underlies most explicit lower bounds for De Morgan and B2 circuits, and recent work recasts circuit simplification as a confluent rewriting system. The constructive-separations program further asks for algorithms that, given a circuit too small to compute a target, exhibit an input on which it errs—a witness. We report an open, reproducible toolkit that operationalises this view as a witness finder. It pairs a confluent De Morgan simplifier with a certified gate-elimination search (ATPG-style justification plus frontier-signature memoisation), miter and treewidth reasoning, and affine-subspace finalisation driven by dispersers. Three experiments show that structure-aware restriction heuristics collapse clause circuits in roughly half the restrictions of random fixing; that miter treewidth sharply separates locally and globally wired circuits, controlling the cost of the treewidth dynamic program; and that on rare-witness instances the certified search returns a verified witness in a single restriction and a couple of evaluations, where blind sampling needs 2Θ(k) evaluations and fails within budget. The full source, seeds, and a one-command reproduction are released; the toolkit is a substrate for experimenting with gate-elimination-based refutation and does not by itself prove new lower bounds.