Add certified unweighted gadget search and optimization

[isPANN]

Summary

This PR adds a complete two-stage framework for four-pin unweighted MIS gadgets on triangular and king-grid lattices.

1. Stage I — certified search

   • Joint occupancy-and-frame SAT searches a blank finite window for occupied sites, four pins, and outward rays in one CNF.
   • Frame-first SAT enumerates canonical G1–G4 port geometry and solves the smaller fixed-frame occupancy problem.
   • Exact-cardinality selection, reduced-alpha witnesses and bounds, and direct layered connectivity are encoded in CNF and solved with Kissat.
   • Every model is checked by the unchanged gadget verifier and crossing-geometry checker.

2. Stage II — certified optimization

   • Structural rewrite rules contract valid boundary structures without arbitrary vertex deletion.
   • Fixed-frame SAT re-synthesizes a smaller interior after a one-step interface rewrite.
   • Every fixed-frame solve has a 100,000-conflict cap. Unresolved calls are counted and reported as sat_unknown instead of being mistaken for a fixed point.
   • Direct descendants are explored to closure, and every accepted step is independently re-verified.

The public stages remain separately schedulable. The recommended end-to-end workflow is search followed by optimization.

Behavior and API

• Adds search_unweighted_gadget_joint for blank-window joint SAT discovery.
• Keeps search_unweighted_gadgets as deterministic frame-first finite-window search.
• Adds checkpoint/resume support and read_unweighted_search_checkpoint progress reporting.
• Adds optimize_unweighted_gadget with a replayable certified rewrite trace, bounded per-call SAT effort, and unresolved_sat_evaluations accounting.
• Replaces the old per-edge arrival connectivity formulation with direct layered reachability.
• Uses one Kissat implementation on Linux and macOS; removes the CryptoMiniSat dependency, Windows implementation, and Windows CI jobs.
• Removes superseded connectivity modes and obsolete joint/frame encodings.

Verified outcomes

Target	Stage I	Stage II	Offset	Outcome
CROSS	28 sites	23 sites	10 → 7	reduced and verifier-valid
CROSS+EDGE	9 sites	9 sites	1 → 1	no smaller result within 256 SAT evaluations; verifier-valid

The CROSS+EDGE outcome is budget-relative, not a proof of global minimality.

Correctness coverage

• Direct layered connectivity is compared with explicit connected-subset enumeration on small hosts.
• Fixed-frame and joint positive controls pass the unchanged verifier.
• CROSS and CROSS+EDGE are both searched and then passed through Stage II.
• The historical independently discovered 28-site CROSS is accepted by production constraints and reduced through certified rewrites to 23 sites.
• Forced conflict-limit exhaustion verifies that UNKNOWN work is not reported as a fixed point.
• Search checkpoints are interrupted, inspected, resumed, and compared with full finite traversal.

Verification

JULIA_NUM_THREADS=1 julia --project=. test/core/unweighted_search.jl

• Unweighted search: 409 / 409 passed

JULIA_NUM_THREADS=1 julia --project=. -e "using Pkg; Pkg.test()"

• GadgetSearch tests passed
• git diff --check passed

The included Typst/PDF report explains the SAT encodings, independent certification boundary, two-stage workflow, and the interface-signature principle used to derive reusable rewrite rules. Temporary HPC logs, exploratory benchmarks, deferred queues, and research artifacts are intentionally excluded.

[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

❌ Patch coverage is 98.96014% with 12 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
src/core/unweighted_sat.jl	98.43%	12 Missing ⚠️

Files with missing lines	Coverage Δ
src/core/unweighted_search.jl	98.12% <100.00%> (+1.19%)	⬆️
src/core/unweighted_sat.jl	98.43% <98.43%> (ø)

... and 1 file with indirect coverage changes

🚀 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.