soda-artifact-evaluation

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>