From ecee6895458d8e06934c95b687a133eddd754dad Mon Sep 17 00:00:00 2001 From: Sebastiano Tronto Date: Sun, 8 Nov 2026 18:24:35 +0100 Subject: Fix table generation (breaking change) There was a small (but kinda silly) error in the prunin table generation for H48 solvers, resulting in some positions showing a higher lower bound than they actually had. This means that the solvers where in theory broken and could have skipped some solutions - but we have not found any example, as this would be an extremely rare situation. This affected all tables from H48h2 to H48h11. This bug was found by LLM-based coding analysis in the context of the development of egg-solver: https://github.com/ArhanChaudhary/egg-solver Thanks to Arhan Chaudhary for reporting the bug. --- src/solvers/h48/checkdata.h | 74 +++++++++++++++++++++---------------------- src/solvers/h48/gendata_h48.h | 2 +- 2 files changed, 38 insertions(+), 38 deletions(-) (limited to 'src/solvers') diff --git a/src/solvers/h48/checkdata.h b/src/solvers/h48/checkdata.h index e2fa38c..749cfc7 100644 --- a/src/solvers/h48/checkdata.h +++ b/src/solvers/h48/checkdata.h @@ -43,90 +43,90 @@ struct { .max = 3, .table = { [0] = 6391286, - [1] = 55494785, + [1] = 55494787, [2] = 252389935, - [3] = 155993794, + [3] = 155993792, }, }, [3] = { .max = 3, .table = { [0] = 6686828, - [1] = 63867852, - [2] = 392789689, - [3] = 477195231, + [1] = 63867855, + [2] = 392789704, + [3] = 477195213, }, }, [4] = { .max = 3, .table = { - [0] = 77147213, - [1] = 543379415, - [2] = 1139570251, - [3] = 120982321, + [0] = 77147216, + [1] = 543379445, + [2] = 1139570223, + [3] = 120982316, }, }, [5] = { .max = 3, .table = { - [0] = 82471284, - [1] = 687850732, - [2] = 2345840746, - [3] = 645995638, + [0] = 82471289, + [1] = 687850794, + [2] = 2345840739, + [3] = 645995578, }, }, [6] = { .max = 3, .table = { - [0] = 85941099, - [1] = 804752968, - [2] = 4077248182, - [3] = 2556374551, + [0] = 85941105, + [1] = 80475305, + [2] = 4077248291, + [3] = 2556374347, }, }, [7] = { .max = 3, .table = { - [0] = 88529761, - [1] = 897323475, - [2] = 6126260791, - [3] = 7936519573, + [0] = 88529771, + [1] = 897323586, + [2] = 6126261227, + [3] = 7936519016, }, }, [8] = { .max = 3, .table = { - [0] = 1051579940, - [1] = 8136021316, - [2] = 19024479822, - [3] = 1885186122, + [0] = 1051580076, + [1] = 8136022157, + [2] = 19024479157, + [3] = 1885185810, }, }, [9] = { .max = 3, .table = { - [0] = 1102038189, - [1] = 9888265242, - [2] = 38299375805, - [3] = 10904855164, + [0] = 1102038343, + [1] = 9888266493, + [2] = 38299376032, + [3] = 10904853532, }, }, [10] = { .max = 3, .table = { - [0] = 1133240039, - [1] = 11196285614, - [2] = 64164702961, - [3] = 43894840186, + [0] = 1133240200, + [1] = 11196287163, + [2] = 64164706157, + [3] = 43894835280, }, }, [11] = { .max = 3, .table = { - [0] = 1150763161, - [1] = 12045845660, - [2] = 91163433330, - [3] = 136418095449, + [0] = 1150763320, + [1] = 12045847349, + [2] = 91163441021, + [3] = 136418085910, }, }, }; diff --git a/src/solvers/h48/gendata_h48.h b/src/solvers/h48/gendata_h48.h index 0b85e49..be06588 100644 --- a/src/solvers/h48/gendata_h48.h +++ b/src/solvers/h48/gendata_h48.h @@ -308,7 +308,7 @@ gendata_h48_runthread(void *arg) wrapthread_mutex_lock(dfsarg->shortcubes_mutex); kv = h48map_nextkvpair(dfsarg->shortcubes, dfsarg->next); - if (*dfsarg->next == dfsarg->shortcubes->capacity) { + if (kv.val == MAP_UNSET_VAL) { wrapthread_mutex_unlock(dfsarg->shortcubes_mutex); break; } -- cgit v1.3