From bc2f199bd3e4d49e8ce47aaf41ccdb45e70c49ed Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 13 Dec 2011 23:38:41 -0800 Subject: Started SAT-based reparameterization. --- src/sat/bsat/satProof.c | 209 +++++++++++++++------------------------------- src/sat/bsat/satSolver2.c | 8 +- src/sat/bsat/satSolver2.h | 5 ++ 3 files changed, 73 insertions(+), 149 deletions(-) (limited to 'src/sat/bsat') diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index 337fe3ca..ded11f1e 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -133,10 +133,10 @@ static inline satset* Proof_ResolveRead (Rec_Int_t* p, cla h ) { return (sats // iterating through fanins of a proof node #define Proof_NodeForeachFanin( p, pNode, pFanin, i ) \ for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = (pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(p, pNode->pEnts[i] >> 2)), 1); i++ ) -#define Proof_NodeForeachLeaf( pLeaves, pNode, pLeaf, i ) \ - for ( i = 0; (i < (int)pNode->nEnts) && (((pLeaf) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pLeaves, pNode->pEnts[i] >> 2) : NULL), 1); i++ ) -#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++ ) +#define Proof_NodeForeachLeaf( pClauses, pNode, pLeaf, i ) \ + for ( i = 0; (i < (int)pNode->nEnts) && (((pLeaf) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pClauses, pNode->pEnts[i] >> 2) : NULL), 1); i++ ) +#define Proof_NodeForeachFaninLeaf( p, pClauses, pNode, pFanin, i ) \ + for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pClauses, pNode->pEnts[i] >> 2) : Proof_NodeRead(p, pNode->pEnts[i] >> 2)); i++ ) //////////////////////////////////////////////////////////////////////// @@ -420,135 +420,6 @@ void Sat_ProofReduce( sat_solver2 * s ) -#if 0 - -/**Function************************************************************* - - Synopsis [Performs one resultion step.] - - Description [Returns ID of the resolvent if success, and -1 if failure.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -satset * Sat_ProofCheckResolveOne( 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 * Sat_ProofCheckReadOne( 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 Sat_ProofCheck( 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_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 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] ); - for ( k = 1; k < (int)pSet->nEnts; k++ ) - { - pSet1 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] ); - pSet0 = Sat_ProofCheckResolveOne( 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.] @@ -669,7 +540,7 @@ void Sat_ProofCheck( sat_solver2 * s ) // 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. " ); + printf( "Derived clause with %d lits instead of the empty clause. ", pSet0->nEnts ); else printf( "Proof verification successful. " ); Abc_PrintTime( 1, "Time", clock() - clk ); @@ -689,7 +560,7 @@ void Sat_ProofCheck( sat_solver2 * s ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vUsed ) +Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vUsed, int fUseIds ) { Vec_Int_t * vCore; satset * pNode, * pFanin; @@ -709,11 +580,59 @@ Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_ Proof_ForeachNodeVec( vCore, vClauses, pNode, i ) { pNode->mark = 0; - Vec_IntWriteEntry( vCore, i, pNode->Id - 1 ); + if ( fUseIds ) + Vec_IntWriteEntry( vCore, i, pNode->Id - 1 ); } return vCore; } +/**Function************************************************************* + + Synopsis [Verifies that variables are labeled correctly.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sat_ProofInterpolantCheckVars( sat_solver2 * s, Vec_Int_t * vGloVars ) +{ + satset* c; + Vec_Int_t * vVarMap; + int i, k, Entry, * pMask; + int Counts[5] = {0}; + // map variables into their type (A, B, or AB) + vVarMap = Vec_IntStart( s->size ); + sat_solver_foreach_clause( s, c, i ) + for ( k = 0; k < (int)c->nEnts; k++ ) + *Vec_IntEntryP(vVarMap, lit_var(c->pEnts[k])) |= 2 - c->partA; + // analyze variables + Vec_IntForEachEntry( vGloVars, Entry, i ) + { + pMask = Vec_IntEntryP(vVarMap, Entry); + assert( *pMask >= 0 && *pMask <= 3 ); + Counts[(*pMask & 3)]++; + *pMask = 0; + } + // count the number of global variables not listed + Vec_IntForEachEntry( vVarMap, Entry, i ) + if ( Entry == 3 ) + Counts[4]++; + Vec_IntFree( vVarMap ); + // report + if ( Counts[0] ) + printf( "Warning: %6d variables listed as global do not appear in clauses (this is normal)\n", Counts[0] ); + if ( Counts[1] ) + printf( "Warning: %6d variables listed as global appear only in A-clauses (this is a BUG)\n", Counts[1] ); + if ( Counts[2] ) + printf( "Warning: %6d variables listed as global appear only in B-clauses (this is a BUG)\n", Counts[2] ); + if ( Counts[3] ) + printf( "Warning: %6d (out of %d) variables listed as global appear in both A- and B-clauses (this is normal)\n", Counts[3], Vec_IntSize(vGloVars) ); + if ( Counts[4] ) + printf( "Warning: %6d variables not listed as global appear in both A- and B-clauses (this is a BUG)\n", Counts[4] ); +} /**Function************************************************************* @@ -737,15 +656,17 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ) satset * pNode, * pFanin; Aig_Man_t * pAig; Aig_Obj_t * pObj; - int i, k, iVar, Entry; + int i, k, iVar, Lit, Entry; + + Sat_ProofInterpolantCheckVars( s, vGlobVars ); // collect visited nodes vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); // collect core clauses (cleans vUsed and vCore) - vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed ); + vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 0 ); // map variables into their global numbers - vVarMap = Vec_IntStartFull( Vec_IntFindMax(vGlobVars) + 1 ); + vVarMap = Vec_IntStartFull( s->size ); Vec_IntForEachEntry( vGlobVars, Entry, i ) Vec_IntWriteEntry( vVarMap, Entry, i ); @@ -762,9 +683,9 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ) if ( pNode->partA ) { pObj = Aig_ManConst0( pAig ); - satset_foreach_var( pNode, iVar, k, 0 ) - if ( iVar < Vec_IntSize(vVarMap) && Vec_IntEntry(vVarMap, iVar) >= 0 ) - pObj = Aig_Or( pAig, pObj, Aig_IthVar(pAig, iVar) ); + satset_foreach_lit( pNode, Lit, k, 0 ) + if ( (iVar = Vec_IntEntry(vVarMap, lit_var(Lit))) >= 0 ) + pObj = Aig_Or( pAig, pObj, Aig_NotCond(Aig_IthVar(pAig, iVar), lit_sign(Lit)) ); } else pObj = Aig_ManConst1( pAig ); @@ -777,9 +698,11 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ) // copy the numbers out and derive interpol for resolvents Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) { +// satset_print( pNode ); assert( pNode->nEnts > 1 ); Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k ) { + assert( pFanin->Id < 2*Aig_ManObjNumMax(pAig) ); if ( k == 0 ) pObj = Aig_ObjFromLit( pAig, pFanin->Id ); else if ( pNode->pEnts[k] & 2 ) // variable of A @@ -828,7 +751,7 @@ void * Sat_ProofCore( sat_solver2 * s ) // collect visited clauses vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); // collect core clauses - vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed ); + vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 1 ); Vec_IntFree( vUsed ); return vCore; } diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index e2bea751..5eb65132 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -144,11 +144,9 @@ static inline void solver2_clear_marks(sat_solver2* s) { static inline satset* clause_read (sat_solver2* s, cla h) { return (h & 1) ? satset_read(&s->learnts, h>>1) : satset_read(&s->clauses, h>>1); } static inline cla clause_handle (sat_solver2* s, satset* c) { return c->learnt ? (satset_handle(&s->learnts, c)<<1)|1: satset_handle(&s->clauses, c)<<1; } static inline int clause_check (sat_solver2* s, satset* c) { return c->learnt ? satset_check(&s->learnts, c) : satset_check(&s->clauses, c); } -static inline int clause_proofid(sat_solver2* s, satset* c, int partA) { return c->learnt ? (veci_begin(&s->claProofs)[c->Id]<<2) | (partA<<1) : (satset_handle(&s->clauses, c)<<2) | 1; } +static inline int clause_proofid(sat_solver2* s, satset* c, int partA) { return c->learnt ? (veci_begin(&s->claProofs)[c->Id]<<2) | (partA<<1) : (satset_handle(&s->clauses, c)<<2) | (partA<<1) | 1; } static inline int clause_is_used(sat_solver2* s, cla h) { return (h & 1) ? (h >> 1) < s->hLearntPivot : (h >> 1) < s->hClausePivot; } - - //static inline int var_reason (sat_solver2* s, int v) { return (s->reasons[v]&1) ? 0 : s->reasons[v] >> 1; } //static inline int lit_reason (sat_solver2* s, int l) { return (s->reasons[lit_var(l)&1]) ? 0 : s->reasons[lit_var(l)] >> 1; } //static inline satset* var_unit_clause(sat_solver2* s, int v) { return (s->reasons[v]&1) ? clause_read(s, s->reasons[v] >> 1) : NULL; } @@ -163,9 +161,6 @@ int clause_is_partA (sat_solver2* s, int h) { return clause void clause_set_partA(sat_solver2* s, int h, int partA) { clause_read(s, h)->partA = partA; } int clause_id(sat_solver2* s, int h) { return clause_read(s, h)->Id; } -#define sat_solver_foreach_clause( s, c, h ) satset_foreach_entry( &s->clauses, c, h, 1 ) -#define sat_solver_foreach_learnt( s, c, h ) satset_foreach_entry( &s->learnts, c, h, 1 ) - //================================================================================================= // Simple helpers: @@ -1452,6 +1447,7 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end) if ( !solver2_enqueue(s,begin[0],0) ) assert( 0 ); } +//satset_print( clause_read(s, Cid) ); return Cid; } diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index 83dbb6cb..e5b85a43 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -184,6 +184,11 @@ static inline void satset_print (satset * c) { for ( i = 0; (i < veci_size(pVec)) && ((c) = satset_read(p, veci_begin(pVec)[i])); i++ ) #define satset_foreach_var( p, var, i, start ) \ for ( i = start; (i < (int)(p)->nEnts) && ((var) = lit_var((p)->pEnts[i])); i++ ) +#define satset_foreach_lit( p, lit, i, start ) \ + for ( i = start; (i < (int)(p)->nEnts) && ((lit) = (p)->pEnts[i]); i++ ) + +#define sat_solver_foreach_clause( s, c, h ) satset_foreach_entry( &s->clauses, c, h, 1 ) +#define sat_solver_foreach_learnt( s, c, h ) satset_foreach_entry( &s->learnts, c, h, 1 ) //================================================================================================= // Public APIs: -- cgit v1.2.3