From c999981bf88abdfef4bb2dabb95863670bdf449a Mon Sep 17 00:00:00 2001 From: Trevor Hansen Date: Tue, 1 Sep 2026 12:07:39 +1000 Subject: [PATCH] cnf: cache the ISOP cover of each distinct cut function Cnf_ComputeClauses() calls Kit_TruthIsop() twice for every non-AND cone it turns into clauses, once for the function and once for its complement, and computes both covers from scratch every time. A cover depends on nothing but the truth table and the leaf count, and the cuts of a bit-blasted circuit are a handful of adder, mux and xor functions repeated across the netlist, so nearly all of that is recomputation. Key the covers by (truth table, leaf count) in a table that lives for one Cnf_DeriveFastClauses() call, and replay a stored cover cube for cube. Mf_ManDeriveCnfs() does the same thing where the mapper has already assigned each truth function an id. The clauses come out of the same cubes in the same order, so the CNF is unchanged. Over bit-vector queries the covers are reused nearly every time: 7.0M cover requests over 42 distinct functions on one 512-bit arithmetic query, 3.2M over 26 on a second and 2.4M over 196 on a third, with the whole table a few hundred ints. CNF derivation on those three goes 2528 -> 1643 ms, 1244 -> 754 ms and 793 -> 448 ms, a 35-44% cut, and peak memory is unchanged. Cnf_ComputeClauses() keeps its signature and its uncached behaviour for the callers outside this file. --- src/sat/cnf/cnfFast.c | 108 +++++++++++++++++++++++++++++++++++++----- 1 file changed, 95 insertions(+), 13 deletions(-) diff --git a/src/sat/cnf/cnfFast.c b/src/sat/cnf/cnfFast.c index cfcb9e2d0..19bb842ea 100644 --- a/src/sat/cnf/cnfFast.c +++ b/src/sat/cnf/cnfFast.c @@ -202,6 +202,81 @@ static inline int Cnf_ObjGetLit( Vec_Int_t * vMap, Aig_Obj_t * pObj, int fCompl return iSatVar + iSatVar + fCompl; } +/**Function************************************************************* + + Synopsis [Remembers the ISOP cover of each distinct cut function.] + + Description [The cover computed by Kit_TruthIsop() depends on nothing but + the truth table and the number of leaves, while a cut function repeats + across the AIG as often as the gate it came from: a bit-blasted circuit is + a few adder, mux and xor functions used millions of times over. Cutting + the ISOP for a function that has already been covered saves recomputing it + and, since the cover is replayed cube for cube, leaves the CNF unchanged. + Same idea as Mf_ManDeriveCnfs(), which keys off the truth table id the + mapper already assigns.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +typedef struct Cnf_IsopCache_t_ Cnf_IsopCache_t; +struct Cnf_IsopCache_t_ +{ + Vec_Mem_t * vFuncs; // the (truth table, leaf count) keys seen so far + Vec_Int_t * vCovers; // key id -> where its cover sits in vCubes + Vec_Int_t * vCubes; // per key: the cube count, then the cubes +}; + +static Cnf_IsopCache_t * Cnf_IsopCacheStart() +{ + Cnf_IsopCache_t * p = ABC_CALLOC( Cnf_IsopCache_t, 1 ); + p->vFuncs = Vec_MemAlloc( 2, 8 ); + Vec_MemHashAlloc( p->vFuncs, 1 << 10 ); + p->vCovers = Vec_IntAlloc( 1 << 10 ); + p->vCubes = Vec_IntAlloc( 1 << 12 ); + return p; +} + +static void Cnf_IsopCacheStop( Cnf_IsopCache_t * p ) +{ + Vec_MemHashFree( p->vFuncs ); + Vec_MemFree( p->vFuncs ); + Vec_IntFree( p->vCovers ); + Vec_IntFree( p->vCubes ); + ABC_FREE( p ); +} + +// Returns the cover of Truth as *pnCubes cubes. A NULL cache computes every +// time, for the callers that derive clauses for one cone at a time. +static int * Cnf_IsopCacheCover( Cnf_IsopCache_t * p, word Truth, int nLeaves, Vec_Int_t * vCover, int * pnCubes ) +{ + word Key[2]; + int c, Cube, iFunc, iCover, RetValue; + if ( p == NULL ) + { + RetValue = Kit_TruthIsop( (unsigned *)&Truth, nLeaves, vCover, 0 ); + assert( RetValue >= 0 ); + *pnCubes = Vec_IntSize( vCover ); + return Vec_IntArray( vCover ); + } + Key[0] = Truth; + Key[1] = (word)nLeaves; + iFunc = Vec_MemHashInsert( p->vFuncs, Key ); + if ( iFunc == Vec_IntSize(p->vCovers) ) + { + RetValue = Kit_TruthIsop( (unsigned *)&Truth, nLeaves, vCover, 0 ); + assert( RetValue >= 0 ); + Vec_IntPush( p->vCovers, Vec_IntSize(p->vCubes) ); + Vec_IntPush( p->vCubes, Vec_IntSize(vCover) ); + Vec_IntForEachEntry( vCover, Cube, c ) + Vec_IntPush( p->vCubes, Cube ); + } + iCover = Vec_IntEntry( p->vCovers, iFunc ); + *pnCubes = Vec_IntEntry( p->vCubes, iCover ); + return Vec_IntArray( p->vCubes ) + iCover + 1; +} + /**Function************************************************************* Synopsis [Collects nodes inside the cone.] @@ -213,11 +288,12 @@ static inline int Cnf_ObjGetLit( Vec_Int_t * vMap, Aig_Obj_t * pObj, int fCompl SeeAlso [] ***********************************************************************/ -void Cnf_ComputeClauses( Aig_Man_t * p, Aig_Obj_t * pRoot, - Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Int_t * vMap, Vec_Int_t * vCover, Vec_Int_t * vClauses ) +static void Cnf_ComputeClausesInt( Aig_Man_t * p, Aig_Obj_t * pRoot, + Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Int_t * vMap, Vec_Int_t * vCover, Vec_Int_t * vClauses, + Cnf_IsopCache_t * pCache ) { Aig_Obj_t * pLeaf; - int c, k, Cube, OutLit, RetValue; + int c, k, Cube, OutLit, nCubes, * pCubes; word Truth; assert( pRoot->fMarkA ); @@ -265,11 +341,10 @@ void Cnf_ComputeClauses( Aig_Man_t * p, Aig_Obj_t * pRoot, return; } - RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 ); - assert( RetValue >= 0 ); - - Vec_IntForEachEntry( vCover, Cube, c ) + pCubes = Cnf_IsopCacheCover( pCache, Truth, Vec_PtrSize(vLeaves), vCover, &nCubes ); + for ( c = 0; c < nCubes; c++ ) { + Cube = pCubes[c]; Vec_IntPush( vClauses, 0 ); Vec_IntPush( vClauses, OutLit ); for ( k = 0; k < Vec_PtrSize(vLeaves); k++, Cube >>= 2 ) @@ -281,12 +356,10 @@ void Cnf_ComputeClauses( Aig_Man_t * p, Aig_Obj_t * pRoot, } } - Truth = ~Truth; - - RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 ); - assert( RetValue >= 0 ); - Vec_IntForEachEntry( vCover, Cube, c ) + pCubes = Cnf_IsopCacheCover( pCache, ~Truth, Vec_PtrSize(vLeaves), vCover, &nCubes ); + for ( c = 0; c < nCubes; c++ ) { + Cube = pCubes[c]; Vec_IntPush( vClauses, 0 ); Vec_IntPush( vClauses, OutLit ^ 1 ); for ( k = 0; k < Vec_PtrSize(vLeaves); k++, Cube >>= 2 ) @@ -299,6 +372,12 @@ void Cnf_ComputeClauses( Aig_Man_t * p, Aig_Obj_t * pRoot, } } +void Cnf_ComputeClauses( Aig_Man_t * p, Aig_Obj_t * pRoot, + Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Int_t * vMap, Vec_Int_t * vCover, Vec_Int_t * vClauses ) +{ + Cnf_ComputeClausesInt( p, pRoot, vLeaves, vNodes, vMap, vCover, vClauses, NULL ); +} + /**Function************************************************************* @@ -566,6 +645,7 @@ Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs ) Vec_Int_t * vLits, * vClas, * vMap, * vTemp; Vec_Ptr_t * vLeaves, * vNodes; Vec_Int_t * vCover; + Cnf_IsopCache_t * pCache; Aig_Obj_t * pObj; int i, k, nVars, Entry, OutLit, DriLit; @@ -604,11 +684,12 @@ Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs ) vNodes = Vec_PtrAlloc( 100 ); vCover = Vec_IntAlloc( 1 << 16 ); vTemp = Vec_IntAlloc( 100 ); + pCache = Cnf_IsopCacheStart(); Aig_ManForEachNodeReverse( p, pObj, i ) { if ( !pObj->fMarkA ) continue; - Cnf_ComputeClauses( p, pObj, vLeaves, vNodes, vMap, vCover, vTemp ); + Cnf_ComputeClausesInt( p, pObj, vLeaves, vNodes, vMap, vCover, vTemp, pCache ); Vec_IntForEachEntry( vTemp, Entry, k ) { if ( Entry == 0 ) @@ -617,6 +698,7 @@ Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs ) Vec_IntPush( vLits, Entry ); } } + Cnf_IsopCacheStop( pCache ); Vec_PtrFree( vLeaves ); Vec_PtrFree( vNodes ); Vec_IntFree( vCover );