| 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:
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
[Artifact routing] SODA-internal proof evidence / arXiv companion / ALENEX AE
[Proof-dependence audit] <claims whose truth relies on computation, and their certificates>
[Anonymity state] <archive hosting compatible with double-blind: yes/no>
[AE calendar] <applicable ALENEX dates, owner per deadline>
[Release plan] <post-acceptance versioning and DOI>
