adv-mixer-3 report: queue 18 launched on build-2 (box 2 reopened), SAT k=2 running

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
This commit is contained in:
igneum-labs 2026-10-07 20:13:54 +00:00
parent 9825e2453c
commit 1d85d41571

View file

@ -253,7 +253,7 @@ under a millisecond on one core. The solver at k = 1 is five orders slower than
|---|---|---|---|---|---|---|
| 20729 | 1 (smoke, build-1) | 33,873 | 112,328 | SATISFIABLE | 137 s | t = 0x49880000, index 0x20eb79 = target |
| 20729 | 1 (queue 08, build-2) | 33,873 | 112,328 | SATISFIABLE | 1,593 s (box at load 500) | the same t |
| 20729 | 2 | 68,624 | 227,767 | not run (the lease was withdrawn before it was granted) | | |
| 20729 | 2 | 68,624 | 227,767 | running since 20:13 UTC on build-2 (one-hour cap) | | |
Reading: the one-application model is a 32-variable problem with 112 k clauses of ripple-carry adders (16
constant multiplies of up to 32 adders each dominate). CaDiCaL needs minutes on it where the honest search needs
@ -284,6 +284,7 @@ CNF out of the worktree mirror into /srv/builds/_adv-mixer-3/. Both applied befo
| Queue 18 withdrawn from build-2 | build-2 | 19:35 | 0 (no lease was ever granted) | main's order: every adv-* waiter leaves box 2 until the class v5 census runs; the SAT rows k = 2..4 re-queue there afterwards |
| Priority classes in the lease (release > v5 > measure > adv) | build-1 | 19:42 | | queue 17 killed and re-submitted once under the ranked tool as `lease pool 32 --min 16` (an adv holder at 32 threads or fewer is never pre-empted); waiting on free cores at 19:43 UTC; still waiting at 19:57 behind eleven adv-class waiters |
| Queue 18 unclaimed on the shared queue | build-2 | 19:58 | | box 2 is closed to adv-* leases until the class v5 census runs; the claim was released so whichever lane has time when it reopens can run the SAT rows (CaDiCaL at ~/adv-mixer-3-tools/cadical/build/cadical on both boxes; the file is self-contained) |
| Queue 18 re-claimed and launched | build-2 | 20:13 | running | box 2 reopened to adv-* at 20:12 UTC (the class v5 census ended); `lease pool 1 --min 1` granted at once (core 8); CaDiCaL on the k = 2 CNF of day 20729 (68,624 vars, 227,767 clauses), one-hour cap, then k = 3, 4 and day 20733 |
| Queue 07 (8 random days) | build-1 | 18:5x | running | claimed and run by the sibling lane adv-mixer from the shared queue; its logs are index-<day>-k<k>.log and sac-<day>-k<k>.log under /srv/builds/_adv-mixer-3/logs/ on build-1, read by this lane |
## The round margin, stated