Experiment exp_smt: SMT/Constraint Solver for Sparse Parity¶
Date: 2026-03-06 Status: SUCCESS Answers: Sparse parity is trivially solvable as a constraint satisfaction problem -- both Z3 and backtracking find exact solutions with 100% accuracy in milliseconds.
Hypothesis¶
Sparse parity can be encoded as a constraint satisfaction problem: find indices a, b, c such that sign(x[a] * x[b] * x[c]) == label for all training samples. The search space is C(n,k), which is tiny for SMT solvers. Two approaches tested: Z3 SMT solver with boolean/XOR encoding, and a custom backtracking constraint solver with pruning.
Config¶
| Parameter | Value |
|---|---|
| n_bits | 20, 50, 100 |
| k_sparse | 3, 5 |
| method | Z3 SMT (boolean+XOR encoding), backtracking with pruning |
| n_train | 500 (k=3), 2000 (k=5) |
| Z3 samples | 50 (subset of training data) |
| seeds | 42, 43, 44 |
Results¶
Main results (all configs solved 3/3 seeds, 100% test accuracy)¶
| Config | C(n,k) | Z3 avg time | BT avg time | BT avg nodes |
|---|---|---|---|---|
| n=20, k=3 | 1,140 | 0.0151s | 0.0017s | 88 |
| n=50, k=3 | 19,600 | 0.0969s | 0.0261s | 554 |
| n=100, k=3 | 161,700 | 3.3801s | 0.1829s | 2,146 |
| n=20, k=5 | 15,504 | 0.0144s | 0.0458s | 1,888 |
Sample complexity (n=20, k=3)¶
| Samples | Result |
|---|---|
| 3-9 | WRONG (finds a false positive subset) |
| 10+ | CORRECT (unique solution found) |
Minimum samples for unique correct solution: 10 (for n=20, k=3).
Analysis¶
What worked¶
- Both solvers achieve 100% accuracy on all configs -- exact subset recovery, not approximate.
- Backtracking is fastest overall: 0.002s for n=20/k=3, 0.026s for n=50/k=3, 0.183s for n=100/k=3. The k-1 pruning optimization (when k-1 indices are chosen, compute the required last column and check if it exists) is highly effective.
- Z3 with boolean+XOR encoding works well: Uses boolean selection variables (sel_j = True if column j selected), PbEq for exactly-k constraint, and XOR chains for parity constraints. Only 50 samples needed.
- n=100/k=3 solved in 0.18s by backtracking -- this is a search space of 161,700 subsets, yet the solver explores only ~2,146 nodes on average due to constraint propagation.
Z3 vs Backtracking comparison¶
- Backtracking wins on speed for all configs except n=20/k=5: The custom solver with domain-specific pruning (k-1 column matching) outperforms the general-purpose Z3 solver.
- Z3 is more consistent: Solve times are less variable across seeds. Backtracking time depends on where the secret indices fall in the enumeration order.
- Z3 struggles with n=100: One seed took 5.5s, another 0.6s. The boolean encoding creates 100 variables and XOR chains of ~50 terms each, which pushes Z3's DPLL harder.
- Z3 is competitive for small n: At n=20, Z3 (0.014s) is comparable to backtracking (0.002-0.046s).
Comparison with other approaches¶
| Method | n=20/k=3 | n=50/k=3 | n=100/k=3 | n=20/k=5 |
|---|---|---|---|---|
| SMT backtrack | 0.002s | 0.026s | 0.183s | 0.046s |
| Z3 SMT | 0.015s | 0.097s | 3.380s | 0.014s |
| Random search | 0.011s | 0.142s | -- | 0.426s |
| Evolutionary | 0.041s | 0.781s | -- | 0.552s |
| SGD (baseline) | 0.12s | FAIL (54%) | -- | 14 epochs |
Key insight¶
The backtracking constraint solver is the fastest method tested so far for all configs. It beats random search (which was already faster than SGD) by 5-10x because it prunes the search space using constraint propagation rather than sampling randomly. The k-1 pruning optimization is the critical trick: once k-1 indices are fixed, the required last column is fully determined by the training data, so we just need to check if any remaining column matches.
Sample complexity¶
Only ~10 samples are needed for n=20/k=3 to get a unique correct solution. With fewer samples (<10), the solver finds a false positive subset that happens to satisfy all constraints. This is because with too few samples, there exist spurious k-subsets whose parity matches the labels by coincidence. The minimum sample count scales roughly as O(k * log(n/k)) based on information-theoretic arguments.
Open Questions¶
- How does backtracking scale to k=7 or k=10? The search depth increases and k-1 pruning becomes less effective.
- Can the Z3 encoding be improved with symmetry breaking or better constraint formulations?
- Can we combine SMT solving with statistical pre-filtering (e.g., mutual information) to narrow the candidate columns before solving?
- What is the theoretical minimum sample complexity as a function of n and k?
Files¶
- Experiment:
src/sparse_parity/experiments/exp_smt.py - Results:
results/exp_smt/results.json