Add direct SAT search for four-pin unweighted gadgets

[isPANN]

Summary

• Replace the dynamic logical-graph/rewrite search with a bounded direct SAT search for four-pin unit-weight MIS gadgets.
• Enumerate ordered pin locations and outward lattice directions in a finite triangular or KSG window, reject frames that fail G1-G4, and remove lattice-symmetry duplicates.
• Encode occupied sites, exact atom count, connectivity, and the target reduced alpha tensor in CryptoMiniSat, including negative constant offsets when permitted by the target.
• Enumerate distinct occupancy models within each fixed frame/count/offset case and independently check every candidate with the existing is_gadget_replacement verifier and check_crossing_frame.

Behavior

search_unweighted_gadgets(target_graph, target_boundary, lattice) now chooses the concrete pins, rays, and internal atoms directly. It examines min_vertices:max_vertices in increasing order and reports separate SAT-solver-call and frame-enumeration budget termination states.

The old beam/mutation/rewrite parameters and trace-only result fields are removed because that implementation is replaced rather than retained alongside SAT search.

Evidence

Case	Result
23-site triangular CROSS fixture	SAT; fixed verifier accepts offset 7
Shifted triangular target	SAT; negative offset -1
5-site KSG positive control	SAT; G1-G4 all true
KSG atom count larger than host	UNSAT
Two occupancy variables plus one free auxiliary variable	Exactly four distinct occupancy models
Missing, repeated, or duplicate pins/sites	ArgumentError

Verification

julia --project=. -e 'using Pkg; Pkg.test()'
GadgetSearch tests passed
Unweighted Search: 28 / 28

git diff --check also passes. The Typst/PDF report and autoresearch/discussion artifacts are intentionally excluded from this PR.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: a808922cc1

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

Files with missing lines	Coverage Δ
src/core/unweighted_sat.jl	100.00% <100.00%> (ø)
src/core/unweighted_search.jl	96.38% <100.00%> (-0.55%)	⬇️

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.