From ec9593e2ff0856d78b37df3a977a753be82bfddc Mon Sep 17 00:00:00 2001 From: Sebastiano Tronto Date: Wed, 17 Dec 2025 17:36:16 +0100 Subject: Fix alignment --- doc/h48.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'doc/h48.md') diff --git a/doc/h48.md b/doc/h48.md index 2487aad..d9ef192 100644 --- a/doc/h48.md +++ b/doc/h48.md @@ -225,6 +225,8 @@ of 1, 2 or 3 can be used directly as a lower bound of b+1, b+2 and b+3 respectively. However, a value of 0 could mean that the actual lower bound is anything between 0 and b, so we cannot take b as a lower bound. +#### Fallback tables + To be able to still use some sort of pruning value even when we get a 0 read, we use a **fallback table**. Inspired by nxopt, this table is interleaved with the main table for cache efficiency: every 254 entries @@ -235,6 +237,16 @@ when looking up the minimum value in the fallback table after a 0 read. Smaller lines (of 256 or 128 bits) have been tried, but they do not give any significant improvement over 512 bit lines. +This trick provides the gratest performance benefits if the main pruning +table is properly aligned. Unfortunately, as a design choice, the +solver is implemented here as a library that defer all memory allocation +business to the implementor. We do make sure that the table is properly +aligned in the programs provided in this repository (for example, the +rudimentary shell and the tools), but we do not enforce this in the +main library code. + +#### Additional (fast) lookups + Moreover, as an additional heuristic, in case of a 0 read we also look up another pruning value in a table that takes into account only the position of the edges. This table is small (around 1MB), so repeated -- cgit v1.3