From a7517688c64432d57b9394f53545b99b4787812b Mon Sep 17 00:00:00 2001 From: Trevor Hansen Date: Sun, 4 Oct 2026 17:55:56 +1100 Subject: [PATCH] cnf: bound the ISOP cover table Nothing bounds how many distinct cut functions a circuit can present. The table is keyed by (truth table, leaf count) and inserts on every miss, so its size is bounded only by two entries per cone, which is O(AIG): at 32 bytes plus four per cube, and a 6-input ISOP running to 32 cubes over the symmetric functions, a twelve-million-gate blast could in principle reach a gigabyte of table. It does not happen because the reuse is extreme and concentrated -- four functions answer all 146,304 requests of a 293k-AND multiplier -- but nothing in the code relied on that. Bound it at 1024 entries, about 200 KB with the initial allocation. Replaying the five request streams measured so far against a bound of 1024, an LRU of 1024 and a direct-mapped 1024 gives the same hit rate as an unbounded table to three decimal places: 99.997% on the multiplier, 81.265% on i10, which presents 160 distinct functions and is the most diverse of them. LRU and the bound are identical to the digit at every size from 256 up, and direct-mapped is slightly worse because collisions evict functions that are still hot. So the policy is the simplest one that bounds the table: past the bound a function already stored is still replayed, and one that is not is computed and not stored. The memo is a pure function of its key, so declining to store an entry cannot change a clause. Checked rather than assumed: with the bound at 4, so the unstored path runs on nearly every request, the CNF is byte-identical to the unbounded build over two multipliers, a ripple adder and i10 at four synthesis settings each, 16 of 16. --- src/sat/cnf/cnfFast.c | 28 +++++++++++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) diff --git a/src/sat/cnf/cnfFast.c b/src/sat/cnf/cnfFast.c index 90e163bac..8ce907001 100644 --- a/src/sat/cnf/cnfFast.c +++ b/src/sat/cnf/cnfFast.c @@ -222,6 +222,18 @@ static inline int Cnf_ObjGetLit( Vec_Int_t * vMap, Aig_Obj_t * pObj, int fCompl SeeAlso [] ***********************************************************************/ +// Entries the table will hold. Nothing bounds how many distinct cut functions +// a circuit can present -- at most two per cone, so O(AIG) -- while the reuse +// is extreme and concentrated: on a 293k-AND multiplier four functions answer +// 146,304 of 146,304 requests. Replaying the five request streams measured so +// far against a bound of 1024, an LRU of 1024 and a direct-mapped 1024 gives +// the same hit rate as an unbounded table to three decimal places, the most +// distinct functions any of them presents being 166. So the table is bounded +// here and the policy left as simple as it can be: past the bound a function +// already stored is still replayed, and one that is not is computed and not +// stored. +#define CNF_ISOP_CACHE_MAX 1024 + typedef struct Cnf_IsopCache_t_ Cnf_IsopCache_t; struct Cnf_IsopCache_t_ { @@ -264,7 +276,21 @@ static int * Cnf_IsopCacheCover( Cnf_IsopCache_t * p, word Truth, int nLeaves, V } Key[0] = Truth; Key[1] = (word)nLeaves; - iFunc = Vec_MemHashInsert( p->vFuncs, Key ); + if ( Vec_IntSize(p->vCovers) < CNF_ISOP_CACHE_MAX ) + iFunc = Vec_MemHashInsert( p->vFuncs, Key ); + else + { + // Full: serve what is stored, compute the rest without storing it. + int * pSpot = Vec_MemHashLookup( p->vFuncs, Key ); + if ( *pSpot == -1 ) + { + RetValue = Kit_TruthIsop( (unsigned *)&Truth, nLeaves, vCover, 0 ); + assert( RetValue >= 0 ); + *pnCubes = Vec_IntSize( vCover ); + return Vec_IntArray( vCover ); + } + iFunc = *pSpot; + } if ( iFunc == Vec_IntSize(p->vCovers) ) { RetValue = Kit_TruthIsop( (unsigned *)&Truth, nLeaves, vCover, 0 );