From b5c3992b6b00c64cfd20a553858fb7c25f1fedac Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 8 Dec 2011 19:43:08 -0800 Subject: Proof-logging in the updated solver. --- src/sat/bsat/satProof.c | 463 +++++++++++++++++++++++++++++++++------------- src/sat/bsat/satSolver2.c | 2 +- src/sat/bsat/satSolver2.h | 2 +- 3 files changed, 334 insertions(+), 133 deletions(-) (limited to 'src') diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index 3b30910d..f817ab3d 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -34,8 +34,70 @@ ABC_NAMESPACE_IMPL_START Root clauses are given by their handles. They are marked by bitshifting by 2 bits up and setting the LSB to 1 */ -/* +// data-structure to record resolvents of the proof +typedef struct Rec_Int_t_ Rec_Int_t; +struct Rec_Int_t_ +{ + int nShift; // log number of entries on a page + int Mask; // mask for entry number on a page + int nSize; // the total number of entries + int nLast; // the total number of entries before last append + Vec_Ptr_t * vPages; // memory pages +}; +static inline Rec_Int_t * Rec_IntAlloc( int nShift ) +{ + Rec_Int_t * p; + p = ABC_CALLOC( Rec_Int_t, 1 ); + p->nShift = nShift; + p->Mask = (1<vPages = Vec_PtrAlloc( 50 ); + return p; +} +static inline int Rec_IntSize( Rec_Int_t * p ) +{ + return p->nSize; +} +static inline int Rec_IntSizeLast( Rec_Int_t * p ) +{ + return p->nLast; +} +static inline void Rec_IntPush( Rec_Int_t * p, int Entry ) +{ + if ( (p->nSize >> p->nShift) == Vec_PtrSize(p->vPages) ) + Vec_PtrPush( p->vPages, ABC_ALLOC(int, p->Mask+1) ); + ((int*)p->vPages->pArray[p->nSize >> p->nShift])[p->nSize++ & p->Mask] = Entry; +} +static inline void Rec_IntAppend( Rec_Int_t * p, int * pArray, int nSize ) +{ + assert( nSize <= p->Mask ); + if ( (p->nSize & p->Mask) + nSize >= p->Mask ) + { + Rec_IntPush( p, 0 ); + p->nSize = ((p->nSize >> p->nShift) + 1) * (p->Mask + 1); + } + if ( (p->nSize >> p->nShift) == Vec_PtrSize(p->vPages) ) + Vec_PtrPush( p->vPages, ABC_ALLOC(int, p->Mask+1) ); +// assert( (p->nSize >> p->nShift) + 1 == Vec_PtrSize(p->vPages) ); + memmove( (int*)p->vPages->pArray[p->nSize >> p->nShift] + (p->nSize & p->Mask), pArray, sizeof(int) * nSize ); + p->nLast = p->nSize; + p->nSize += nSize; +} +static inline int Rec_IntEntry( Rec_Int_t * p, int i ) +{ + return ((int*)p->vPages->pArray[i >> p->nShift])[i & p->Mask]; +} +static inline int * Rec_IntEntryP( Rec_Int_t * p, int i ) +{ + return (int*)p->vPages->pArray[i >> p->nShift] + (i & p->Mask); +} +static inline void Rec_IntFree( Rec_Int_t * p ) +{ + Vec_PtrFreeFree( p->vPages ); + ABC_FREE( p ); +} + +/* typedef struct satset_t satset; struct satset_t { @@ -55,10 +117,12 @@ struct satset_t /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static inline satset* Proof_NodeRead (Vec_Int_t* p, cla h ) { return satset_read( (veci*)p, h ); } -static inline cla Proof_NodeHandle (Vec_Int_t* p, satset* c) { return satset_handle( (veci*)p, c ); } -static inline int Proof_NodeCheck (Vec_Int_t* p, satset* c) { return satset_check( (veci*)p, c ); } -static inline int Proof_NodeSize (int nEnts) { return sizeof(satset)/4 + nEnts; } +static inline satset* Proof_NodeRead (Vec_Int_t* p, cla h ) { return satset_read( (veci*)p, h ); } +static inline cla Proof_NodeHandle (Vec_Int_t* p, satset* c) { return satset_handle( (veci*)p, c ); } +static inline int Proof_NodeCheck (Vec_Int_t* p, satset* c) { return satset_check( (veci*)p, c ); } +static inline int Proof_NodeSize (int nEnts) { return sizeof(satset)/4 + nEnts; } + +static inline satset* Proof_ResolveRead (Rec_Int_t* p, cla h ) { return (satset*)Rec_IntEntryP(p, h); } // iterating through nodes in the proof #define Proof_ForeachNode( p, pNode, h ) \ @@ -74,6 +138,7 @@ static inline int Proof_NodeSize (int nEnts) { return sizeo #define Proof_NodeForeachFaninLeaf( p, pLeaves, pNode, pFanin, i ) \ for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pLeaves, pNode->pEnts[i] >> 2) : Proof_NodeRead(p, pNode->pEnts[i] >> 2)); i++ ) + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -289,132 +354,9 @@ Vec_Int_t * Proof_CollectUsedRec( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hR } return vUsed; } - -/**Function************************************************************* - - Synopsis [Performs one resultion step.] - - Description [Returns ID of the resolvent if success, and -1 if failure.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -satset * Proof_ResolveOne( Vec_Int_t * p, satset * c1, satset * c2, Vec_Int_t * vTemp ) -{ - satset * c; - int i, k, hNode, Var = -1, Count = 0; - // find resolution variable - for ( i = 0; i < (int)c1->nEnts; i++ ) - for ( k = 0; k < (int)c2->nEnts; k++ ) - if ( (c1->pEnts[i] ^ c2->pEnts[k]) == 1 ) - { - Var = (c1->pEnts[i] >> 1); - Count++; - } - if ( Count == 0 ) - { - printf( "Cannot find resolution variable\n" ); - return NULL; - } - if ( Count > 1 ) - { - printf( "Found more than 1 resolution variables\n" ); - return NULL; - } - // perform resolution - Vec_IntClear( vTemp ); - for ( i = 0; i < (int)c1->nEnts; i++ ) - if ( (c1->pEnts[i] >> 1) != Var ) - Vec_IntPush( vTemp, c1->pEnts[i] ); - for ( i = 0; i < (int)c2->nEnts; i++ ) - if ( (c2->pEnts[i] >> 1) != Var ) - Vec_IntPushUnique( vTemp, c2->pEnts[i] ); - // move to the new one - hNode = Vec_IntSize( p ); - Vec_IntPush( p, 0 ); // placeholder - Vec_IntPush( p, 0 ); - Vec_IntForEachEntry( vTemp, Var, i ) - Vec_IntPush( p, Var ); - c = Proof_NodeRead( p, hNode ); - c->nEnts = Vec_IntSize(vTemp); - return c; -} - -/**Function************************************************************* - - Synopsis [Checks the proof for consitency.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -satset * Proof_CheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vResolves, int iAnt ) -{ - satset * pAnt; - if ( iAnt & 1 ) - return Proof_NodeRead( vClauses, iAnt >> 2 ); - assert( iAnt > 0 ); - pAnt = Proof_NodeRead( vProof, iAnt >> 2 ); - assert( pAnt->Id > 0 ); - return Proof_NodeRead( vResolves, pAnt->Id ); -} - -/**Function************************************************************* - Synopsis [Checks the proof for consitency.] - Description [] - - SideEffects [] - SeeAlso [] - -***********************************************************************/ -void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot ) -{ - Vec_Int_t * vUsed, * vResolves, * vTemp; - satset * pSet, * pSet0, * pSet1; - int i, k, Counter = 0, clk = clock(); - // collect visited clauses - vUsed = Proof_CollectUsedRec( vProof, NULL, hRoot ); -// vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); - Proof_CleanCollected( vProof, vUsed ); - // perform resolution steps - vTemp = Vec_IntAlloc( 1000 ); - vResolves = Vec_IntAlloc( 1000 ); - Vec_IntPush( vResolves, -1 ); - Proof_ForeachNodeVec( vUsed, vProof, pSet, i ) - { - pSet0 = Proof_CheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] ); - for ( k = 1; k < (int)pSet->nEnts; k++ ) - { - pSet1 = Proof_CheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] ); - pSet0 = Proof_ResolveOne( vResolves, pSet0, pSet1, vTemp ); - } - pSet->Id = Proof_NodeHandle( vResolves, pSet0 ); -//printf( "Clause for proof %d: ", Vec_IntEntry(vUsed, i) ); -//satset_print( pSet0 ); - Counter++; - } - Vec_IntFree( vTemp ); - // clean the proof - Proof_CleanCollected( vProof, vUsed ); - // compare the final clause - printf( "Used %6.2f Mb for resolvents.\n", 4.0 * Vec_IntSize(vResolves) / (1<<20) ); - if ( pSet0->nEnts > 0 ) - printf( "Cound not derive the empty clause. " ); - else - printf( "Proof verification successful. " ); - Abc_PrintTime( 1, "Time", clock() - clk ); - // cleanup - Vec_IntFree( vResolves ); - Vec_IntFree( vUsed ); -} /**Function************************************************************* @@ -449,6 +391,7 @@ Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_ return vCore; } + /**Function************************************************************* Synopsis [Computes UNSAT core.] @@ -591,10 +534,7 @@ void Sat_ProofReduce( veci * pProof, veci * pRoots ) pNode->Id = hNewHandle; hNewHandle += Proof_NodeSize(pNode->nEnts); Proof_NodeForeachFanin( vProof, pNode, pFanin, k ) if ( pFanin ) - { - assert( (pNode->pEnts[k] >> 2) == Proof_NodeHandle(vProof, pFanin) ); pNode->pEnts[k] = (pFanin->Id << 2) | (pNode->pEnts[k] & 2); - } } // update roots Proof_ForeachNodeVec( vRoots, vProof, pNode, i ) @@ -618,6 +558,267 @@ void Sat_ProofReduce( veci * pProof, veci * pRoots ) Vec_IntShrink( vProof, hNewHandle ); } + + + + +#if 0 + +/**Function************************************************************* + + Synopsis [Performs one resultion step.] + + Description [Returns ID of the resolvent if success, and -1 if failure.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +satset * Proof_ResolveOne( Vec_Int_t * p, satset * c1, satset * c2, Vec_Int_t * vTemp ) +{ + satset * c; + int i, k, hNode, Var = -1, Count = 0; + // find resolution variable + for ( i = 0; i < (int)c1->nEnts; i++ ) + for ( k = 0; k < (int)c2->nEnts; k++ ) + if ( (c1->pEnts[i] ^ c2->pEnts[k]) == 1 ) + { + Var = (c1->pEnts[i] >> 1); + Count++; + } + if ( Count == 0 ) + { + printf( "Cannot find resolution variable\n" ); + return NULL; + } + if ( Count > 1 ) + { + printf( "Found more than 1 resolution variables\n" ); + return NULL; + } + // perform resolution + Vec_IntClear( vTemp ); + for ( i = 0; i < (int)c1->nEnts; i++ ) + if ( (c1->pEnts[i] >> 1) != Var ) + Vec_IntPush( vTemp, c1->pEnts[i] ); + for ( i = 0; i < (int)c2->nEnts; i++ ) + if ( (c2->pEnts[i] >> 1) != Var ) + Vec_IntPushUnique( vTemp, c2->pEnts[i] ); + // move to the new one + hNode = Vec_IntSize( p ); + Vec_IntPush( p, 0 ); // placeholder + Vec_IntPush( p, 0 ); + Vec_IntForEachEntry( vTemp, Var, i ) + Vec_IntPush( p, Var ); + c = Proof_NodeRead( p, hNode ); + c->nEnts = Vec_IntSize(vTemp); + return c; +} + +/**Function************************************************************* + + Synopsis [Checks the proof for consitency.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +satset * Proof_CheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vResolves, int iAnt ) +{ + satset * pAnt; + if ( iAnt & 1 ) + return Proof_NodeRead( vClauses, iAnt >> 2 ); + assert( iAnt > 0 ); + pAnt = Proof_NodeRead( vProof, iAnt >> 2 ); + assert( pAnt->Id > 0 ); + return Proof_NodeRead( vResolves, pAnt->Id ); +} + +/**Function************************************************************* + + Synopsis [Checks the proof for consitency.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot ) +{ + Vec_Int_t * vUsed, * vResolves, * vTemp; + satset * pSet, * pSet0, * pSet1; + int i, k, Counter = 0, clk = clock(); + // collect visited clauses + vUsed = Proof_CollectUsedRec( vProof, NULL, hRoot ); +// vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); + Proof_CleanCollected( vProof, vUsed ); + // perform resolution steps + vTemp = Vec_IntAlloc( 1000 ); + vResolves = Vec_IntAlloc( 1000 ); + Vec_IntPush( vResolves, -1 ); + Proof_ForeachNodeVec( vUsed, vProof, pSet, i ) + { + pSet0 = Proof_CheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] ); + for ( k = 1; k < (int)pSet->nEnts; k++ ) + { + pSet1 = Proof_CheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] ); + pSet0 = Proof_ResolveOne( vResolves, pSet0, pSet1, vTemp ); + } + pSet->Id = Proof_NodeHandle( vResolves, pSet0 ); +//printf( "Clause for proof %d: ", Vec_IntEntry(vUsed, i) ); +//satset_print( pSet0 ); + Counter++; + } + Vec_IntFree( vTemp ); + // clean the proof + Proof_CleanCollected( vProof, vUsed ); + // compare the final clause + printf( "Used %6.2f Mb for resolvents.\n", 4.0 * Vec_IntSize(vResolves) / (1<<20) ); + if ( pSet0->nEnts > 0 ) + printf( "Cound not derive the empty clause. " ); + else + printf( "Proof verification successful. " ); + Abc_PrintTime( 1, "Time", clock() - clk ); + // cleanup + Vec_IntFree( vResolves ); + Vec_IntFree( vUsed ); +} + +#endif + +/**Function************************************************************* + + Synopsis [Performs one resultion step.] + + Description [Returns ID of the resolvent if success, and -1 if failure.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +satset * Proof_ResolveOne( Rec_Int_t * p, satset * c1, satset * c2, Vec_Int_t * vTemp ) +{ + satset * c; + int i, k, Var = -1, Count = 0; + // find resolution variable + for ( i = 0; i < (int)c1->nEnts; i++ ) + for ( k = 0; k < (int)c2->nEnts; k++ ) + if ( (c1->pEnts[i] ^ c2->pEnts[k]) == 1 ) + { + Var = (c1->pEnts[i] >> 1); + Count++; + } + if ( Count == 0 ) + { + printf( "Cannot find resolution variable\n" ); + return NULL; + } + if ( Count > 1 ) + { + printf( "Found more than 1 resolution variables\n" ); + return NULL; + } + // perform resolution + Vec_IntClear( vTemp ); + Vec_IntPush( vTemp, 0 ); // placeholder + Vec_IntPush( vTemp, 0 ); + for ( i = 0; i < (int)c1->nEnts; i++ ) + if ( (c1->pEnts[i] >> 1) != Var ) + Vec_IntPush( vTemp, c1->pEnts[i] ); + for ( i = 0; i < (int)c2->nEnts; i++ ) + if ( (c2->pEnts[i] >> 1) != Var ) + Vec_IntPushUnique( vTemp, c2->pEnts[i] ); + // create new resolution entry + Rec_IntAppend( p, Vec_IntArray(vTemp), Vec_IntSize(vTemp) ); + // return the new entry + c = Proof_ResolveRead( p, Rec_IntSizeLast(p) ); + c->nEnts = Vec_IntSize(vTemp)-2; + return c; +} + +/**Function************************************************************* + + Synopsis [Checks the proof for consitency.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +satset * Proof_CheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Rec_Int_t * vResolves, int iAnt ) +{ + satset * pAnt; + if ( iAnt & 1 ) + return Proof_NodeRead( vClauses, iAnt >> 2 ); + assert( iAnt > 0 ); + pAnt = Proof_NodeRead( vProof, iAnt >> 2 ); + assert( pAnt->Id > 0 ); + return Proof_ResolveRead( vResolves, pAnt->Id ); +} + +/**Function************************************************************* + + Synopsis [Checks the proof for consitency.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot ) +{ + Rec_Int_t * vResolves; + Vec_Int_t * vUsed, * vTemp; + satset * pSet, * pSet0, * pSet1; + int i, k, Counter = 0, clk = clock(); + // collect visited clauses +// vUsed = Proof_CollectUsedRec( vProof, NULL, hRoot ); + vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); + Proof_CleanCollected( vProof, vUsed ); + // perform resolution steps + vTemp = Vec_IntAlloc( 1000 ); + vResolves = Rec_IntAlloc( 20 ); + Rec_IntPush( vResolves, -1 ); + Proof_ForeachNodeVec( vUsed, vProof, pSet, i ) + { + pSet0 = Proof_CheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] ); + for ( k = 1; k < (int)pSet->nEnts; k++ ) + { + pSet1 = Proof_CheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] ); + pSet0 = Proof_ResolveOne( vResolves, pSet0, pSet1, vTemp ); + } + pSet->Id = Rec_IntSizeLast( vResolves ); +//printf( "Clause for proof %d: ", Vec_IntEntry(vUsed, i) ); +//satset_print( pSet0 ); + Counter++; + } + Vec_IntFree( vTemp ); + // clean the proof + Proof_CleanCollected( vProof, vUsed ); + // compare the final clause + printf( "Used %6.2f Mb for resolvents.\n", 4.0 * Rec_IntSize(vResolves) / (1<<20) ); + if ( pSet0->nEnts > 0 ) + printf( "Cound not derive the empty clause. " ); + else + printf( "Proof verification successful. " ); + Abc_PrintTime( 1, "Time", clock() - clk ); + // cleanup + Rec_IntFree( vResolves ); + Vec_IntFree( vUsed ); +} + + /**Function************************************************************* Synopsis [Computes interpolant of the proof.] diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 843a33b6..8fdc2ecb 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -1450,7 +1450,7 @@ void solver2_reducedb(sat_solver2* s) extern void Sat_ProofReduce( veci * pProof, veci * pRoots ); satset * c; cla h,* pArray,* pArray2; - int Counter = 0, CounterStart = s->stats.learnts * 2 / 3; + int Counter = 0, CounterStart = s->stats.learnts * 3 / 4; // 2/3; int i, j, k, hTemp, hHandle, clk = clock(); static int TimeTotal = 0; diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index 01216146..2e745bc2 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -32,7 +32,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA ABC_NAMESPACE_HEADER_START -//#define USE_FLOAT_ACTIVITY +#define USE_FLOAT_ACTIVITY //================================================================================================= // Public interface: -- cgit v1.2.3