--- name: soda-artifact-evaluation description: Use when deciding how code, computations, or data attach to a SODA (ACM-SIAM Symposium on Discrete Algorithms) paper — SODA itself runs no artifact track, so this skill covers computer-assisted proof evidence, implementation companions, and when to route the artifact to co-located ALENEX's formal artifact evaluation instead. --- # SODA Artifact Evaluation First, the venue truth: **SODA has no artifact-evaluation track.** Referees judge proofs, not repositories. But two kinds of computational objects still matter to a SODA author, and the co-located satellite ALENEX runs a genuine AE process — for the 2027 cycle, ALENEX's dates were: submission July 20, 2026; notification early September 2026; artifact submission September 11, 2026; AE rebuttal October 12-14; AE results by October 16, 2026, with a dedicated HotCRP AE site (`alenex27ae.hotcrp.com`; checked 2026-07-08 via search renderings of the SIAM ALENEX27 pages). ## Which of three situations are you in? | Situation | Artifact's role | Correct home | |---|---|---| | Proof relies on machine computation (case enumeration, SAT/ILP certificate, verified numerics) | Part of the proof — reviewers must be able to check it | The SODA submission itself, described in the paper, archive linked | | Implementation exists but the claim is the theorem | Supporting color; zero review weight at SODA | arXiv full version appendix + repository; one paragraph in the paper | | The experiments are the contribution (engineering, tuning, real datasets) | The reviewed object | ALENEX, with its AE process — not SODA | The routing mistake costs a cycle: an implementation-led paper at SODA reads as a theorem-light submission; a theorem-led paper at ALENEX reads as an experiment-light one. `soda-experiments` covers the boundary in detail. ## Computer-assisted proof evidence at SODA When a lemma's truth rests on computation, treat the computation like a proof step: - State in the paper *what* was computed, *why* the computation's correctness implies the lemma, and the reduction from lemma to finite check. - Prefer **certificates over executions**: a SAT unsatisfiability certificate, an LP dual solution, or an exhaustive-search transcript that an independent checker can validate is stronger than "our script printed True." - Pin the environment. A checker that needs one standard tool beats a stack of research dependencies. - Anonymity still applies at submission time (lightweight double-blind): host the archive at an anonymous URL or describe it and promise availability; a link to `github.com/yourname` defeats the author-block scrubbing. A minimal verification bundle that a skeptical theorist can run: ```text verification/ ├── README.md # lemma ↔ computation map; expected output; runtime ├── generate.py # enumerates the finite case space (deterministic) ├── check.py # validates each case; exits nonzero on failure ├── certificates/ # per-case witnesses, checkable independently └── environment.txt # exact toolchain versions ``` The README's first line should be the command that reproduces the check, and the paper should quote the total case count so a re-runner knows when they are done. ## Certificate patterns by claim type Choosing the certificate form is the design decision; everything else is plumbing. Patterns that referees can check without trusting your code: | Claim shape | Certificate | Independent check | |---|---|---| | "No object with property P exists below size k" | Exhaustive enumeration transcript + case count stated in the paper | Re-run enumeration; compare count | | "Formula/configuration is unsatisfiable" | DRAT or similar proof log from the solver | Standard proof checker, not your solver | | "This LP/SDP bound holds" | Dual solution with rational entries | Verify feasibility + objective by exact arithmetic | | "This extremal object exists" | The object itself, in a documented format | Verify its properties directly (cheap direction) | | "Constant c < 1.4142" | Interval-arithmetic evaluation script | Re-run with a different interval library | Two disciplines cut referee effort by an order of magnitude: make the *checking* program trivial even if the *searching* program was heroic, and put the case count / certificate size in the paper so a verifier knows what "done" looks like before starting. ## Routing to ALENEX AE If the artifact is the point, the ALENEX pipeline gives it real review: artifacts are submitted after paper notification (September 11, 2026 for the 2027 cycle), evaluated with a rebuttal round in mid-October, and the results feed the final paper. Practical notes for a SODA-adjacent group: - ALENEX's paper deadline (July 20, 2026) sits eleven days after SODA's — a SODA submission's experimental spin-off can be written in that gap, but the two papers must have genuinely disjoint contributions. - Prepare the artifact for a stranger's machine: pinned dependencies, dataset download scripts with checksums, a single entry point per figure/table. - The AE rebuttal (October 12-14, 2026) is for fixing evaluator blockers, not for adding features — keep a maintainer on call that week. ## Referee psychology of computer-assisted claims A theory referee meeting a machine-checked lemma asks three questions in order, and the paper should answer them in the same order: *Is the reduction from lemma to finite check proved?* (prose, in the paper, no code involved); *Could the check be wrong?* (certificates checkable by independent tools answer this; "our program says so" does not); *Can I re-run it before my review is due?* (state the runtime — an hour on a laptop invites verification, a week on a cluster invites suspicion). Papers that answer all three convert the computational step from a reviewing liability into a fully-verified component; papers that answer none of them get reviews containing the phrase "we were unable to verify," which at a proofs-are-the-product venue is close to fatal. ## Post-acceptance artifact hygiene (either venue) - Move from "anonymous archive" to a citable, versioned release (tagged repository plus an archival DOI service) referenced in the camera-ready. - The repository README should state the paper title, venue, and which claims the code supports — and, honestly, which it does not. - Freeze the version that matches the proceedings; development continues on main, but the paper points to the tag. ## Output format ```text [Artifact routing] SODA-internal proof evidence / arXiv companion / ALENEX AE [Proof-dependence audit] [Anonymity state] [AE calendar] [Release plan] ```