adv-mixer: cadical re-queued through lease pool, ledger updated

Internal adversarial pass, not an independent review.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
This commit is contained in:
igneum-labs 2026-10-07 19:23:02 +00:00
parent 56a0bb50e4
commit c043ca3adf

View file

@ -239,8 +239,9 @@ cadical ran 1,749 s wall on one thread (162 MB peak) and reached neither SAT nor
outcome inside the hour: the instance is a preimage-shaped search on a 2^512 space, so a cap-out bounds solver
reach only and is no evidence either way. The CNF stays on box 2 at
/srv/builds/_adv-adv-mixer/logs/adv-mixer-commute-20729.cnf (6.8 MB) for a re-queue through `lease pool` once
that subcommand exists (at 20:21 BST `lease --help` offered `lease cores` and `lease status` only). Status
BLOCKED on the lease, not on the model.
that subcommand exists (at 20:21 BST `lease --help` offered `lease cores` and `lease status` only). Re-queued
through `lease pool 1` at 20:22 BST the minute the subcommand landed (log sat-commute-20729-lease.log); RUNNING
under a fresh one-hour cap; the row lands here.
## Q1 consolidated verdict (internal adversarial pass, not an independent review)
@ -319,7 +320,7 @@ wall times above are under heavy sharing.
| Process | Box | pid-file | Killed (UTC) | Lost | Re-queue |
|---|---|---|---|---|---|
| cadical on adv-mixer-commute-20729.cnf | 2 | sat-commute-20729.log.pid | 19:20:41Z | 1,749 s of a 3,600 s cap, no SAT or UNSAT | through `lease pool` when it exists; the CNF is kept |
| cadical on adv-mixer-commute-20729.cnf | 2 | sat-commute-20729.log.pid | 19:20:41Z | 1,749 s of a 3,600 s cap, no SAT or UNSAT | RE-QUEUED 19:22:46Z (20:22 BST) through `lease pool 1 --owner adv-mixer --nice 10` the minute the subcommand landed; holding 1 pool core, 1 h cap; pid file sat-commute-20729-lease.log.pid |
| 07-adv-mixer-3-days.sh (owner adv-mixer-3) | 1 | queue-07-adv-mixer-3-days.sh.log.pid | 19:20:47Z | 50 of 56 steps unrun; the 6 done are in the owner's logs | claim released; owner or next free lane |
Both kills were the wrapper pid from the pid file plus its descendants (one cadical, one adv-mixer-3), TERM then