[qcs] Genshin_Impact: reduce Occam circuits from 355 to 347 gates

[Mao-Kexiang]

Exact 347-gate Occam arithmetic circuits

Team

Team name	Genshin_Impact
Members	Kexiang Mao (@Mao-Kexiang)

Challenge

Challenge	Recover and minimize the hidden arithmetic circuits
Catalog issue	QuantumBFS/quantum.harness issue #71
Track	tracks/qcs/

Bottom line

This submission recovers all four hidden functions and supplies exact predictions, legal circuits, search code, and compact verification evidence. Relative to the best public baseline we located and independently audited, the total drops from 355 to 347 gates:

Instance	Function	Prior	New
A	x + y	37	37
B	abs(x - y)	49	49
C	x * y	156	152
D	x^2 + y^2	113	109

The four canonical circuits were checked on all 87,040 inputs and all 764,928 output bits with zero mismatches. This is not a claim that 347 is globally optimal.

Prior work and credit

The 355-gate starting point is Zongyue Liu's PR #156. Many thanks to Zongyue for the strong public baseline.

For prompt-injection and supply-chain safety, I did not execute code or instructions from competitor PRs. I extracted only strict plain-text netlists and independently verified them against direct arithmetic formulas. A37 and B49 retain those verified pure-data circuits. My new circuit reductions are C156 → C152 and D113 → D109.

I may team up with Zongyue in future work, but this PR does not list him as a current member or co-author without mutual confirmation.

1. Main result

Instance	Gates	Assignments	Output bits	SHA-256
A	37	65,536	589,824	56c95acceeedb40f54fdae2e5fc2840d1bf58e0989f46a950e6a56742fd20e24
B	49	16,384	114,688	289b60494a703cf7f74a4aef2f540d225aeff22d86c4d709aaa5b661cc69a0a7
C	152	4,096	49,152	67540307369fedfffdb2b1a6473eff5e0bbfeb0e4873d03fddbeceb653cd071c
D	109	1,024	11,264	cd3f317f4a0b88818e54869e40b4550fd67549f8eb4a5eb02c74db4ec6864dbd

The successful route was multi-scale relation-SAT local resynthesis with immediate rebasing:

C156
├── size 5 → C154
│   └── rebase, size 7 → C152
└── size 8 → C153

D113 ── size 6 → D109

A third C stage tested sizes 4–8 from C152; all five completed with validated exact 152-gate outputs and no further improvement.

2. Warm-up result

Circuit	Gates	Exhaustive audit
4-bit addition	17	256/256 exact; commitment match
4×4 multiplication	64	256/256 exact; commitment match

No global optimality claim is made for these practice counts.

3. Suggested-route audit

Every suggested method family received a real implementation or experiment:

Route	Result
Approximate MPS/TN completion	64 configurations; none full-domain exact; useful rank/order diagnostic
Exact Boolean/GF(2) TN	Exact, but 114/488/4,831/1,132 gates
BDD/ZDD/MaxSAT	Completed routes generalize poorly or map large; three exact research jobs remain
SAT local exact synthesis	Safe finite-window UNSAT certificates; no additional frontier candidate
Independent 0-1 IP/MILP	18 windows: 13 proven infeasible, 5 limit, 0 candidate
ABC	Exact direct C152/D109 run remains 152/109
Espresso	Attempted; Berkeley source fails to build against modern libc, so no scientific result claimed
Symbolic/template hybrid	Exact generic templates, followed by the successful relation-SAT compression

The tensor-network hint is useful structurally: interleaving variables reduces A's exact TT rank from 255 to 3, while C remains about 57–61. I therefore use TN as a cut/window oracle, not as a proxy for the final gate metric.

4. Correctness boundary

An early local-SAT encoding allowed root descendants as external divisors and could create cyclic false candidates. Those candidates are invalid and are not included.

The final safe-v3 boundary requires:

1. no removed gate in the boundary;
2. no target-root descendant in the boundary;
3. every target root uniquely determined by the boundary.

Finite-budget results: C156 has 99 UNSAT/1 TIMEOUT, C154 has 97/3, and D109 has 64/15, with zero candidates. TIMEOUT is not reported as infeasible, and local UNSAT is scoped to the fixed parent, boundary, gate library, and budget.

5. Reproduce

From the repository root:

for instance in A B C D; do
  python tracks/qcs/solutions/Genshin_Impact-71/search/audit_arithmetic_formula.py \
    "$instance" \
    "tracks/qcs/solutions/Genshin_Impact-71/frontier-347/netlists/mystery-${instance}.txt"
done

cd tracks/qcs/solutions/Genshin_Impact-71/frontier-347
sha256sum -c SHA256SUMS

The tracked snapshot contains four netlists, four exhaustive audits, manifest.json, SHA256SUMS, and an atomic COMPLETE sentinel. Heavy experiments ran through Slurm on t02-server with root seed 42. eSLIM is pinned to commit 51e9f77429627473db623058157b66a1192cbb59.

6. File map

Path	Role
mystery-{A,B,C,D}.txt	Submission-ready circuits
predictions/mystery-*/test_outputs.csv	Hidden-output predictions
frontier-347/	Immutable compact verification snapshot
search/	Exact audit, eSLIM/SAT bridge, safe windows, BDD/ZDD, and MILP
tensor_network/	Approximate MPS and rank/order route
routes/exact_tn/	Exact Boolean/GF(2) tensor-network route
routes/symbolic_hybrid/	Arithmetic templates, ABC, and Espresso

7. Issue #71 completion audit

Deliverable	Status
Legal mystery-*.txt circuits	Complete
Predicted test_outputs.csv per mystery	Complete
Search scripts	Complete
Pitch-style README	Complete
Hidden-function identification	Complete and commitment-checked
Exhaustive exact verification	Complete
Gate-count improvement	355 → 347 relative to the frozen public baseline

8. Claim boundary

This PR does not prove global optimality for B, C, or D; does not treat timeouts as UNSAT; and does not compare BDD nodes, ABC internals, PLA cubes, or TN rank directly with legal gate count. The most promising next step is safe-v3 search on C152 with exact-TT separator scores and immediate rebasing toward C151/D108.

9. Suggested reading order

1. README.md;
2. frontier-347/manifest.json and the four audit JSON files;
3. tensor_network/TN_RESULTS.md;
4. routes/exact_tn/README.md;
5. search/ip_milp/REPORT.md;