SAT-Guided Neural Network Initialization

Use a SAT solver to construct weight matrices that exactly satisfy a structural constraint (here: orthonormal rows), then use them to initialize a neural network — and test, honestly, whether that helps.

Status: minimal reboot (2026-06). The original 2025 effort grew a large, sprawling codebase and a 32-week roadmap but never cleanly answered its own core question. This reboot strips the project back to a single, runnable, honestly-measured experiment. The old code is preserved under legacy/.

The actual research question

It is well known that orthogonal weight matrices help signal propagate through deep networks (dynamical isometry). But PyTorch already ships torch.nn.init.orthogonal_, which produces an exactly orthogonal matrix analytically, for free. So the question is not "does orthogonality help?" — it's:

Does a SAT-solved orthonormal matrix buy anything over the analytical orthogonal initialization we already have?

The original project never tested this: it compared its SAT init against Xavier/He/unconstrained, but never against analytical orthogonal init — and it benchmarked on an 8-dim toy task where every method saturated at ~97%, so nothing could be distinguished. (Its written "findings" claiming a 1–3% SAT advantage are not supported by its own logged data; see legacy/feasibility_spike_results.md.)

This reboot puts analytical_orthogonal front and center as the baseline to beat, on a task where initialization actually matters.

What's different in the encoding

The original encoding bit-blasted a full signed multiplier circuit to force the dot product of two vectors to zero, and never constrained the norms — so its "orthogonal" matrices were not isometries.

The reboot encodes a ternary matrix W ∈ {-1, 0, +1}^{m×n} such that:

1. every row has exactly nnz_per_row nonzeros (equal norms → scalable to orthonormal), and
2. every pair of rows is exactly orthogonal.

Pairwise orthogonality (Σ W[a]·W[b] = 0) becomes a pseudo-Boolean equality over per-column agreement/disagreement indicators (see sat_init/encoding.py). One solve yields one matrix; distinct per-seed variants are derived by orthonormality-preserving signed permutations rather than re-solving.

Solver tractability (Glucose3, this machine)

layer (m×n)	nnz/row	solve time	result
8×8	8 (dense, Hadamard)	0.01s	SAT
10×10	4	0.14s	SAT
16×16	4	4.2s	SAT
12×12	6	10s	SAT
16×16	5/6/8	>20s	times out

Full mutually-orthogonal ternary designs get hard fast; 16×16, nnz=4 (a genuinely sparse orthonormal frame) is the default experiment layer.

Results

The experiment trains a deep, narrow (depth=16, width=16) tanh MLP on an MNIST subset, initializing only the square hidden layers by each strategy (input/output projections are fixed and shared). Metrics: final test accuracy, epochs to reach a target accuracy, and init_grad_ratio — the ratio of the last hidden layer's initial gradient norm to the first's (≈1 means gradient signal is preserved through depth; ≈0 means it vanishes).

Run on this machine (depth=16, width=16, nnz=4, 6000 train / 2000 test, 15 epochs, 3 seeds; full output in results/comparison_full.json):

strategy	final test acc	init grad ratio	epochs→85%	reached target
sat_orthogonal	90.07 ± 0.2	1.020	2.7	3/3
analytical_orthogonal	90.42 ± 0.1	1.006	2.0	3/3
xavier	89.12 ± 0.3	1.225	5.7	3/3
he	86.37 ± 1.5	0.275	12.0	2/3

Honest read of these numbers:

• Orthogonality clearly helps in this deep-narrow regime. Both orthogonal inits preserve the gradient signal through depth (grad ratio ≈ 1.0) and converge in ~2–3 epochs, while He suffers vanishing gradients (ratio 0.27), trains unstably, and fails to reach target on one seed.
• But SAT buys nothing over the analytical baseline. sat_orthogonal does not beat analytical_orthogonal — analytical is marginally more accurate and converges faster, and it costs a single O(n³) call instead of a multi-second SAT solve that does not scale past ~16×16.

So, for this constraint (orthonormality), the answer to the project's core question is no: a SAT solver is not a competitive way to obtain an orthogonal initialization — PyTorch's analytical routine is better and free. This is a useful negative result, and a more defensible conclusion than the original project's unsupported positive claim.

Where SAT could still earn its keep is constraints that have no closed-form analytical solution (e.g. orthogonality combined with sparsity, sign budgets, hardware/quantization limits, or discrete structural patterns). That — not plain orthogonality — is the direction worth pursuing next.

Layout

sat_init/            # the package
  encoding.py        # ternary orthonormal-row matrix -> CNF (PB constraints)
  solve.py           # solve + orthonormality-preserving seed variants
  init.py            # init strategies: sat_orthogonal, analytical_orthogonal, xavier, he
  model.py           # deep-narrow tanh MLP (init-sensitive regime)
  data.py            # minimal MNIST loader (raw IDX, no torchvision)
  experiment.py      # train/eval loop + metrics
experiments/
  run_comparison.py  # CLI entry point
tests/
  test_encoding.py   # verifies solved matrices are truly orthonormal
legacy/              # the original 2025 codebase, archived

Setup & run

python3.11 -m venv .venv
.venv/bin/pip install -r requirements.txt

.venv/bin/python tests/test_encoding.py            # verify the encoding
.venv/bin/python experiments/run_comparison.py --quick   # ~1 min smoke test
.venv/bin/python experiments/run_comparison.py     # full run (~few min, CPU)

MNIST raw IDX files are expected under data/MNIST/raw/ (already present from the original download; data/ is gitignored as regenerable).

License

MIT (as originally intended).