igneum-network/igneum
1
0
Fork 0
Code Issues Pull requests Releases Activity

adv-mixer-3 report: queue 18 withdrawn from build-2 (ledger), SAT k=2 CNF size

Browse source 
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
This commit is contained in:
igneum-labs 2026-10-07 19:41:41 +00:00
parent 9a3aeb9e8f
commit 489583c511
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
docs/analysis/cryptanalysis/report-mixer-3.md
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 | pending | pending | running | | |
| 20729 | 2 | 68,624 | 227,767 | not run (the lease was withdrawn before it was granted) | | |
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
@ -280,7 +280,8 @@ CNF out of the worktree mirror into /srv/builds/_adv-mixer-3/. Both applied befo
| Queue 16 (index 20733 k = 2..4) under the sweep lock | build-2 | 19:13 | 7 min | k = 2 was running when killed |
| Every adv-mixer-3 process killed | build-1, build-2 | 19:20:51 to 19:21:01 | | main's rule (relayed by the coordinator at 19:20 UTC): no sweep starts except through the build-server lane's `lease pool`; everything hand-started is killed now. Killed by pid file, process group: 03 (sac 20729: k = 5 at 2^24 and the 2^27 rows lost), 09 (sac0: the day 20733 2^28 rows lost), 10 (index 20733 k = 5..8 lost), 04 (sac 20733 k = 5..8 lost), 08 (CaDiCaL on k = 2 for 20729, about 7 min in, lost; k = 3, 4 and day 20733 not started), 16 (index 20733 k = 2..4 lost). Zero processes of this lane remained on either box at 19:21:01 UTC. Nothing of this lane ran until `lease pool` existed |
| Re-queue through `lease pool` | build-1 (queue 17: sac 20729 k = 5..8 and 2^27 rows, sac 20733 k = 5..8, index 20733 k = 2..8, sac0 20733 2^28 rows), build-2 (queue 18: CaDiCaL k = 2..4, both days) | 19:24 UTC (relaunched 19:2x after a guard line refused on the first start) | running | `lease pool 48 --min 16` per census (the lease sizes the harness threads to the cores it took), `lease pool 1 --min 1` per CaDiCaL; waits behind the release builds and the class v5 suites, which outrank every sweep tonight |
| v5 yield | both | 19:26, widened 19:31 | | before every lease the driver sleeps while any waiter in `lease status` is owned by class-v5 or labelled v5; both drivers restarted with the rule before their first lease was granted |
| v5 yield | both | 19:26, widened 19:31 | | before every lease the driver sleeps while any waiter in `lease status` is owned by class-v5 or labelled v5; both drivers restarted with the rule before their first lease was granted; refined 19:32 to yield by owner (class-v5, or attack-pass with v5), never to another adv- lane |
| 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 |
| 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