Add exhaustive search methods for provable optimality

- Add prune_exhaustive: searches ALL weight combinations in range
to find globally optimal magnitude (not just local improvements)

- Rewrite prune_neuron to be truly exhaustive: for each neuron,
searches all weight configs for remaining neurons to prove
whether neuron is necessary (not just greedy zeroing)

- Add config options: exhaustive_range, exhaustive_max_params

- Add method aliases: 'exh', 'brute' for exhaustive search

These methods enable provable optimality for small circuits where
evolutionary/annealing methods get stuck in local minima.

prune.py

@@ -138,9 +138,13 @@ class Config:
     run_gate_subst: bool = True
     run_symmetry: bool = True
     run_fanin: bool = True
+    run_exhaustive: bool = True
 
     magnitude_passes: int = 100
 
+    exhaustive_range: int = 2
+    exhaustive_max_params: int = 12
+
     evo_generations: int = 2000
     evo_pop_size: int = 0
     evo_elite_ratio: float = 0.05
@@ -1730,44 +1734,125 @@ def prune_annealing(circuit: AdaptiveCircuit, evaluator: BatchedEvaluator, cfg:
 
 
 def prune_neuron(circuit: AdaptiveCircuit, evaluator: BatchedEvaluator, cfg: Config) -> PruneResult:
-    """Neuron-level pruning."""
+    """
+    Truly exhaustive neuron-level pruning.
+
+    For each neuron, fix its parameters to zero and exhaustively search
+    all weight configurations for the REMAINING neurons. If any config
+    works, the neuron is provably unnecessary.
+    """
     start = time.perf_counter()
-    weights = circuit.clone_weights()
-    original = circuit.stats(weights)
+    original = circuit.stats()
 
     neuron_groups = defaultdict(list)
-    for key in weights.keys():
+    for key in circuit.weights.keys():
         parts = key.rsplit('.', 1)
         neuron_name = parts[0] if len(parts) == 2 else key.split('.')[0]
         neuron_groups[neuron_name].append(key)
 
+    neuron_names = list(neuron_groups.keys())
+    weight_keys = list(circuit.weights.keys())
+    weight_shapes = {k: circuit.weights[k].shape for k in weight_keys}
+    weight_sizes = {k: circuit.weights[k].numel() for k in weight_keys}
+    n_total_params = sum(weight_sizes.values())
+
     if cfg.verbose:
         print(f"    Found {len(neuron_groups)} neuron groups")
+        print(f"    Total parameters: {n_total_params}")
 
-    removed = 0
-    for neuron_name, keys in neuron_groups.items():
-        saved = {k: weights[k].clone() for k in keys if k in weights}
+    search_range = cfg.exhaustive_range
+    values = list(range(-search_range, search_range + 1))
 
-        for k in keys:
-            if k in weights:
-                weights[k] = torch.zeros_like(weights[k])
+    def vector_to_weights(vec):
+        weights = {}
+        idx = 0
+        for k in weight_keys:
+            size = weight_sizes[k]
+            weights[k] = torch.tensor(vec[idx:idx+size], dtype=torch.float32, device=cfg.device).view(weight_shapes[k])
+            idx += size
+        return weights
 
-        if evaluator.evaluate_single(weights) >= cfg.fitness_threshold:
-            removed += 1
+    def get_neuron_param_indices(neuron_name):
+        indices = []
+        idx = 0
+        for k in weight_keys:
+            size = weight_sizes[k]
+            if k in neuron_groups[neuron_name]:
+                indices.extend(range(idx, idx + size))
+            idx += size
+        return indices
+
+    best_weights = circuit.clone_weights()
+    best_neurons_removed = 0
+    removed_neuron_names = []
+
+    for neuron_name in neuron_names:
+        neuron_indices = set(get_neuron_param_indices(neuron_name))
+        other_indices = [i for i in range(n_total_params) if i not in neuron_indices]
+        n_other_params = len(other_indices)
+
+        if n_other_params > cfg.exhaustive_max_params:
+            if cfg.verbose:
+                print(f"    [{neuron_name}] Skipping: {n_other_params} remaining params > max {cfg.exhaustive_max_params}")
+            continue
+
+        search_space = (2 * search_range + 1) ** n_other_params
+
+        if cfg.verbose:
+            print(f"    [{neuron_name}] Testing removal: searching {search_space:,} configs for {n_other_params} remaining params")
+
+        found_valid = False
+        best_config = None
+        best_mag = float('inf')
+        tested = 0
+        report_interval = max(1, search_space // 10)
+
+        for combo in product(values, repeat=n_other_params):
+            tested += 1
+
+            full_vec = [0] * n_total_params
+            for i, val in zip(other_indices, combo):
+                full_vec[i] = val
+
+            weights = vector_to_weights(full_vec)
+            fitness = evaluator.evaluate_single(weights)
+
+            if fitness >= cfg.fitness_threshold:
+                mag = sum(abs(v) for v in combo)
+                if not found_valid or mag < best_mag:
+                    found_valid = True
+                    best_mag = mag
+                    best_config = full_vec
+
+            if cfg.verbose and tested % report_interval == 0:
+                elapsed = time.perf_counter() - start
+                pct = 100 * tested / search_space
+                print(f"      [{elapsed:6.1f}s] {pct:5.1f}% | valid={'YES' if found_valid else 'no '} | best_mag={best_mag if found_valid else '-'}")
+
+        if found_valid:
             if cfg.verbose:
-                print(f"      Removed: {neuron_name}")
+                print(f"      [REMOVABLE] {neuron_name} can be removed! Best remaining mag={best_mag}")
+            removed_neuron_names.append(neuron_name)
+            best_neurons_removed += 1
+            best_weights = vector_to_weights(best_config)
         else:
-            for k, v in saved.items():
-                weights[k] = v
+            if cfg.verbose:
+                print(f"      [REQUIRED] {neuron_name} is necessary")
+
+    if cfg.verbose:
+        elapsed = time.perf_counter() - start
+        print(f"    [NEURON COMPLETE] {best_neurons_removed} neurons removable out of {len(neuron_names)}")
+        print(f"    Removable: {removed_neuron_names if removed_neuron_names else 'none'}")
+        print(f"    Time: {elapsed:.1f}s")
 
     return PruneResult(
         method='neuron',
         original_stats=original,
-        final_stats=circuit.stats(weights),
-        final_weights=weights,
-        fitness=evaluator.evaluate_single(weights),
+        final_stats=circuit.stats(best_weights),
+        final_weights=best_weights,
+        fitness=evaluator.evaluate_single(best_weights),
         time_seconds=time.perf_counter() - start,
-        metadata={'neurons_removed': removed}
+        metadata={'neurons_removed': best_neurons_removed, 'removed_names': removed_neuron_names}
     )
 
 
@@ -2571,6 +2656,128 @@ def prune_fanin(circuit: AdaptiveCircuit, evaluator: BatchedEvaluator, cfg: Conf
     )
 
 
+def prune_exhaustive(circuit: AdaptiveCircuit, evaluator: BatchedEvaluator, cfg: Config) -> PruneResult:
+    """
+    Exhaustive search over all integer weight combinations.
+
+    Unlike evolutionary/annealing methods that perturb existing weights,
+    this searches ALL possible combinations within a range. Can find
+    globally optimal solutions but only feasible for small circuits.
+
+    Complexity: O((2*range+1)^n_params) - exponential in parameter count.
+    """
+    start = time.perf_counter()
+    original = circuit.stats()
+
+    n_params = original['total']
+    search_range = cfg.exhaustive_range
+
+    if n_params > cfg.exhaustive_max_params:
+        if cfg.verbose:
+            print(f"    [EXHAUSTIVE] Skipping: {n_params} params exceeds max {cfg.exhaustive_max_params}")
+            print(f"    [EXHAUSTIVE] Search space would be {(2*search_range+1)**n_params:,} combinations")
+        return PruneResult(
+            method='exhaustive',
+            original_stats=original,
+            final_stats=original,
+            final_weights=circuit.clone_weights(),
+            fitness=evaluator.evaluate_single(circuit.weights),
+            time_seconds=time.perf_counter() - start,
+            metadata={'skipped': True, 'reason': 'too_many_params'}
+        )
+
+    search_space = (2 * search_range + 1) ** n_params
+
+    if cfg.verbose:
+        print(f"    [EXHAUSTIVE] Parameters: {n_params}")
+        print(f"    [EXHAUSTIVE] Range: [{-search_range}, {search_range}]")
+        print(f"    [EXHAUSTIVE] Search space: {search_space:,} combinations")
+
+    weight_keys = list(circuit.weights.keys())
+    weight_shapes = {k: circuit.weights[k].shape for k in weight_keys}
+    weight_sizes = {k: circuit.weights[k].numel() for k in weight_keys}
+
+    best_weights = circuit.clone_weights()
+    best_mag = original['magnitude']
+    best_fitness = evaluator.evaluate_single(best_weights)
+
+    values = list(range(-search_range, search_range + 1))
+
+    tested = 0
+    valid_found = 0
+    report_interval = max(1, search_space // 100)
+    last_report_time = start
+
+    def vector_to_weights(vec):
+        weights = {}
+        idx = 0
+        for k in weight_keys:
+            size = weight_sizes[k]
+            weights[k] = torch.tensor(vec[idx:idx+size], dtype=torch.float32, device=cfg.device).view(weight_shapes[k])
+            idx += size
+        return weights
+
+    if cfg.verbose:
+        print(f"    [EXHAUSTIVE] Starting search...")
+        print(f"    [EXHAUSTIVE] Progress updates every 1%")
+
+    for combo in product(values, repeat=n_params):
+        tested += 1
+
+        weights = vector_to_weights(combo)
+        fitness = evaluator.evaluate_single(weights)
+
+        if fitness >= cfg.fitness_threshold:
+            valid_found += 1
+            mag = sum(abs(v) for v in combo)
+
+            if mag < best_mag:
+                best_mag = mag
+                best_weights = {k: v.clone() for k, v in weights.items()}
+                best_fitness = fitness
+
+                if cfg.verbose:
+                    elapsed = time.perf_counter() - start
+                    print(f"      [{elapsed:6.1f}s] NEW BEST: magnitude={mag}, weights={combo}")
+
+        if cfg.verbose and tested % report_interval == 0:
+            now = time.perf_counter()
+            elapsed = now - start
+            interval_time = now - last_report_time
+            rate = report_interval / interval_time if interval_time > 0 else 0
+            overall_rate = tested / elapsed if elapsed > 0 else 0
+            eta = (search_space - tested) / overall_rate if overall_rate > 0 else 0
+            pct = 100 * tested / search_space
+            print(f"      [{elapsed:6.1f}s] {pct:5.1f}% | {tested:,}/{search_space:,} | "
+                  f"valid: {valid_found:,} | best: {best_mag:.0f} | "
+                  f"{rate:,.0f}/s (avg {overall_rate:,.0f}/s) | ETA: {eta:.0f}s")
+            last_report_time = now
+
+    if cfg.verbose:
+        elapsed = time.perf_counter() - start
+        print(f"    [EXHAUSTIVE COMPLETE]")
+        print(f"      - Combinations tested: {tested:,}")
+        print(f"      - Valid solutions found: {valid_found:,}")
+        print(f"      - Best magnitude: {best_mag:.0f} (original: {original['magnitude']:.0f})")
+        print(f"      - Reduction: {(1 - best_mag/original['magnitude'])*100:.1f}%")
+        print(f"      - Time: {elapsed:.1f}s ({tested/elapsed:.0f} combos/s)")
+
+    return PruneResult(
+        method='exhaustive',
+        original_stats=original,
+        final_stats=circuit.stats(best_weights),
+        final_weights=best_weights,
+        fitness=best_fitness,
+        time_seconds=time.perf_counter() - start,
+        metadata={
+            'search_space': search_space,
+            'tested': tested,
+            'valid_found': valid_found,
+            'search_range': search_range
+        }
+    )
+
+
 def export_coq(circuit: AdaptiveCircuit, weights: Dict[str, torch.Tensor], cfg: Config) -> Path:
     """
     Export threshold circuit to Coq for formal verification.
@@ -2682,6 +2889,7 @@ def run_all_methods(circuit: AdaptiveCircuit, cfg: Config) -> Dict[str, PruneRes
         ('gate_subst', cfg.run_gate_subst, lambda: prune_gate_substitution(circuit, evaluator, cfg)),
         ('symmetry', cfg.run_symmetry, lambda: prune_symmetry(circuit, evaluator, cfg)),
         ('fanin', cfg.run_fanin, lambda: prune_fanin(circuit, evaluator, cfg)),
+        ('exhaustive', cfg.run_exhaustive, lambda: prune_exhaustive(circuit, evaluator, cfg)),
         ('random', cfg.run_random, lambda: prune_random(circuit, evaluator, cfg)),
         ('evolutionary', cfg.run_evolutionary, lambda: prune_evolutionary(circuit, evaluator, cfg)),
         ('annealing', cfg.run_annealing, lambda: prune_annealing(circuit, evaluator, cfg)),
@@ -2890,7 +3098,7 @@ def main():
         all_methods = ['magnitude', 'zero', 'quantize', 'evolutionary', 'annealing',
                        'neuron', 'lottery', 'topology', 'structured', 'sensitivity',
                        'weight_sharing', 'random', 'pareto', 'depth', 'gate_subst',
-                       'symmetry', 'fanin']
+                       'symmetry', 'fanin', 'exhaustive']
         for m in all_methods:
             setattr(cfg, f'run_{m}', False)
 
@@ -2913,7 +3121,8 @@ def main():
                 'depth': 'depth',
                 'gate': 'gate_subst', 'gate_subst': 'gate_subst', 'subst': 'gate_subst',
                 'sym': 'symmetry', 'symmetry': 'symmetry',
-                'fanin': 'fanin', 'fan': 'fanin'
+                'fanin': 'fanin', 'fan': 'fanin',
+                'exhaustive': 'exhaustive', 'exh': 'exhaustive', 'brute': 'exhaustive'
             }
             if m in method_map:
                 setattr(cfg, f'run_{method_map[m]}', True)