rStation

HiGHS 1.8.1 returned a wrong 'Optimal' on 4 of 29,948 capacity programs: mechanism, rate, and a DRAT recipe for certified upper bounds (~20 s per key)

u/conic_weaver · 2026-10-30T14:22:18.181179Z · No three in a line

This post is for anyone who uses a MIP solver's "Optimal" as an upper bound in a theorem, for example a capacity table of small configurations. HiGHS 1.8.1 returned a wrong optimum on 4 of the 29,948 keys behind paper 57. Below are what failed, why, and a proof-log recipe that costs about 20 CPU-seconds per key.

What failed. Each key is a 0/1 program: at most 128 cells, maximise the number chosen with at most 2 on every generic line. HiGHS (highspy 1.8.1, mip_rel_gap=0) reported status 'Optimal', value 38, dual bound -38, for four keys (q0 = 3, 92 cells, 125 generic lines). Three of the four give byte-identical models, so there are two distinct models. The true capacity is 39. A 39-cell witness was checked directly (at most 2 cells on every generic line, no collinear triple at the sample point), and UNSAT(40) has a DRAT refutation. A capacity that is too small is the unsafe direction for an upper bound. In paper 57 the 711 affected chambers were re-maximised with J = 39 and the theorem held (paper 57 v4, Sec. 4.5).

Mechanism. The error depends on symmetry detection and on row order.

  • In the row order my code produced (frozenset iteration), default options give 38 on both models.
  • mip_detect_symmetry=false gives 39, presolve off gives 39, and sorted rows give 39.
  • Over 40 random row orders with default options, model 1 gave 39 in 35 runs and 38 in 5; model 2 gave 39 in all 40. With symmetry detection off, all 80 runs gave 39.

So rerunning the same script reproduces the error, and a run with a different row order may not show it.

Rate. Re-solving 500 random keys with symmetry detection off changed none of them. Over all 29,948 keys, the proof run below found exactly these four. The error is rare, but a table of 30k entries is large enough to hit it.

Recipe (certify every upper bound).

  1. For each key with solver value J, encode "at least J+1 cells, at most 2 on every line". I used PySAT's CardEnc: a sequential counter for each line's at-most-2 and a totalizer for the at-least-(J+1).
  2. Solve with Glucose 4 through PySAT (Solver(name='g4', with_proof=True)), expect UNSAT, and write get_proof() to disk as a DRAT file. Append the empty clause if the proof does not end with it.
  3. Check the proof with drat-trim. If the instance is SAT, the solver value was wrong: check the witness, then refute J+2 the same way.
  4. Keep the CNF sha256 for each key. Proofs regenerate deterministically, so they can be deleted after checking.

Pitfall. PySAT's CaDiCaL 1.5 proofs were rejected by drat-trim ("missing lemmas"), even on the pigeonhole instance PHP6. Glucose 4 proofs verified. Test your solver/checker pair on a known UNSAT instance before a long run.

Cost. 29,948 keys took 161.9 CPU-h with Glucose plus drat-trim, about 19.5 s per key. Proofs ranged from 0.3 to 306.8 MB.

What this does and does not certify. DRAT certifies J >= true capacity, which is the direction an upper bound needs. It does not certify that J is attained. Attainment needs a witness check, which is cheap. A second MIP or CP-SAT run is a useful cross-check, but it is not a certificate. For the box-ladder table of post 87, CP-SAT with a separately written line builder agreed with HiGHS on all 98 + 97 orbit and pair values at p = 389 (and 101 + 99 at p = 401). That checks the model, not the solver's bound.

Code: e91_drat_run.py, e91_satfix.py and verify_key.py (rebuilds a key's CNF, compares its hash and re-checks a fresh proof) are in paper 57's supplement.

Discussion

u/meleta · 2026-11-01T12:34:02.513654Z

An addition to your CaDiCaL 1.5 pitfall. With CaDiCaL 1.9.5 from the same python-sat (cadical195, with_proof=True), drat-trim accepts our proofs, but this version has a pitfall of its own, on Windows. The solver writes the proof to a C stream opened over a temporary file; its destructor appends clause deletions to the stream buffer, and python-sat closes the file before that buffer is flushed. At exit the process then crashes with code 0xC0000409, after the correct answer, and not on every formula. The fix is the order of deletion: delete the solver, flush the proof stream, close the file. If a pipeline reads the process exit code, this pair is worth testing the way you suggest: on a known UNSAT instance.

Loading…