From 72404d1fdf699c75a4f98101cd695dd3622afe69 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 5 Dec 2011 18:00:49 -0800 Subject: Proof-logging in the updated solver. --- src/sat/bsat/satProof.c | 517 +++++++++++++++++++++++++++------------------- src/sat/bsat/satSolver2.c | 206 +++++++++--------- src/sat/bsat/satSolver2.h | 186 ++++++++++------- src/sat/bsat/satVec.h | 6 +- 4 files changed, 524 insertions(+), 391 deletions(-) diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index 5b3901a1..e2f907bb 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "satSolver.h" +#include "satSolver2.h" #include "vec.h" #include "aig.h" @@ -33,30 +33,41 @@ ABC_NAMESPACE_IMPL_START Label is initialized to 0. Root clauses are 1-based. They are marked by prepending bit 1; */ +/* + +typedef struct satset_t satset; +struct satset_t +{ + unsigned learnt : 1; + unsigned mark : 1; + unsigned partA : 1; + unsigned nEnts : 29; + int Id; + lit pEnts[0]; +}; + +#define satset_foreach_entry( p, c, h, s ) \ + for ( h = s; (h < veci_size(p)) && (((c) = satset_read(p, h)), 1); h += satset_size(c->nEnts) ) +*/ //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -typedef struct Sat_Set_t_ Sat_Set_t; -struct Sat_Set_t_ -{ - int nEnts; - int Label; - int pEnts[0]; -}; +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 int Sat_SetCheck( Vec_Int_t * p, Sat_Set_t * pNode ) { return (int *)pNode > Vec_IntArray(p) && (int *)pNode < Vec_IntLimit(p); } -static inline int Sat_SetId( Vec_Int_t * p, Sat_Set_t * pNode ) { return (int *)pNode - Vec_IntArray(p); } -static inline Sat_Set_t * Sat_SetFromId( Vec_Int_t * p, int i ) { return (Sat_Set_t *)(Vec_IntArray(p) + i); } -static inline int Sat_SetSize( Sat_Set_t * pNode ) { return pNode->nEnts + 2; } +#define Proof_ForeachNode( p, pNode, hNode ) \ + satset_foreach_entry( ((veci*)p), pNode, hNode, 1 ) +#define Proof_ForeachNodeVec( pVec, p, pNode, i ) \ + for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_NodeRead(p, Vec_IntEntry(pVec,i))); i++ ) +#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] >> 1))), 1); i++ ) +#define Proof_NodeForeachFanin2( p, pNode, pFanin, iFanin, i ) \ + for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = ((pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(p, pNode->pEnts[i] >> 1))), ((iFanin) = ((pNode->pEnts[i] & 1) ? pNode->pEnts[i] >> 1 : 0)), 1); i++ ) -#define Sat_PoolForEachSet( p, pNode, i ) \ - for ( i = 1; (i < Vec_IntSize(p)) && ((pNode) = Sat_SetFromId(p, Vec_IntEntry(p,i))); i += Sat_SetSize(pNode) ) -#define Sat_SetForEachSet( p, pSet, pNode, i ) \ - for ( i = 0; (i < pSet->nEnts) && (((pNode) = ((pSet->pEnts[i] & 1) ? NULL : Sat_SetFromId(p, pSet->pEnts[i]))), 1); i++ ) -#define Sat_VecForEachSet( pVec, p, pNode, i ) \ - for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Sat_SetFromId(p, Vec_IntEntry(pVec,i))); i++ ) //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -64,7 +75,7 @@ static inline int Sat_SetSize( Sat_Set_t * pNode ) { re /**Function************************************************************* - Synopsis [Recursively visits useful proof nodes.] + Synopsis [Collects all resolution nodes belonging to the proof.] Description [] @@ -73,48 +84,20 @@ static inline int Sat_SetSize( Sat_Set_t * pNode ) { re SeeAlso [] ***********************************************************************/ -int Sat_ProofReduceOne( Vec_Int_t * p, Sat_Set_t * pNode, int * pnSize, Vec_Int_t * vStack ) +Vec_Int_t * Proof_CollectAll( Vec_Int_t * p ) { - Sat_Set_t * pNext; - int i, NodeId; - if ( pNode->Label ) - return pNode->Label; - // start with node - pNode->Label = 1; - Vec_IntPush( vStack, Sat_SetId(p, pNode) ); - // perform DFS search - while ( Vec_IntSize(vStack) ) - { - NodeId = Vec_IntPop( vStack ); - if ( NodeId & 1 ) // extrated second time - { - pNode = Sat_SetFromId( p, NodeId ^ 1 ); - pNode->Label = *pnSize; - *pnSize += Sat_SetSize(pNode); - // update fanins - Sat_SetForEachSet( p, pNode, pNext, i ) - if ( pNext ) - pNode->pEnts[i] = pNext->Label; - continue; - } - // extracted first time - // add second time - Vec_IntPush( vStack, NodeId ^ 1 ); - // add its anticedents - pNode = Sat_SetFromId( p, NodeId ); - Sat_SetForEachSet( p, pNode, pNext, i ) - if ( pNext && !pNext->Label ) - { - pNext->Label = 1; - Vec_IntPush( vStack, Sat_SetId(p, pNode) ); // add first time - } - } - return pNode->Label; + Vec_Int_t * vUsed; + satset * pNode; + int hNode; + vUsed = Vec_IntAlloc( 1000 ); + Proof_ForeachNode( p, pNode, hNode ) + Vec_IntPush( vUsed, hNode ); + return vUsed; } /**Function************************************************************* - Synopsis [Recursively visits useful proof nodes.] + Synopsis [Cleans collected resultion nodes belonging to the proof.] Description [] @@ -123,63 +106,55 @@ int Sat_ProofReduceOne( Vec_Int_t * p, Sat_Set_t * pNode, int * pnSize, Vec_Int_ SeeAlso [] ***********************************************************************/ -/* -int Sat_ProofReduce_rec( Vec_Int_t * p, Sat_Set_t * pNode, int * pnSize ) +void Proof_CleanCollected( Vec_Int_t * vProof, Vec_Int_t * vUsed ) { - int * pBeg; - assert( Sat_SetCheck(p, pNode) ); - if ( pNode->Label ) - return pNode->Label; - for ( pBeg = pNode->pEnts; pBeg < pNode->pEnts + pNode->nEnts; pBeg++ ) - if ( !(*pBeg & 1) ) - *pBeg = Sat_ProofReduce_rec( p, Sat_SetFromId(p, *pBeg), pnSize ); - pNode->Label = *pnSize; - *pnSize += Sat_SetSize(pNode); - return pNode->Label; + satset * pNode; + int hNode; + Proof_ForeachNodeVec( vUsed, vProof, pNode, hNode ) + pNode->Id = 0; } -*/ /**Function************************************************************* - Synopsis [Reduces the proof to contain only roots and their children.] + Synopsis [Recursively visits useful proof nodes.] - Description [The result is updated proof and updated roots.] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -void Sat_ProofReduce( Vec_Int_t * p, Vec_Int_t * vRoots ) +void Proof_CollectUsedInt( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed, Vec_Int_t * vStack ) { - int i, nSize = 1; - int * pBeg, * pEnd, * pNew; - Vec_Int_t * vStack; - Sat_Set_t * pNode; - // mark used nodes - vStack = Vec_IntAlloc( 1000 ); - Sat_VecForEachSet( vRoots, p, pNode, i ) - vRoots->pArray[i] = Sat_ProofReduceOne( p, pNode, &nSize, vStack ); - Vec_IntFree( vStack ); - // compact proof - pNew = Vec_IntArray(p) + 1; - Sat_PoolForEachSet( p, pNode, i ) + satset * pNext; + int i, hNode; + if ( pNode->Id ) + return; + // start with node + pNode->Id = 1; + Vec_IntPush( vStack, Proof_NodeHandle(p, pNode) << 1 ); + // perform DFS search + while ( Vec_IntSize(vStack) ) { - if ( !pNode->Label ) + hNode = Vec_IntPop( vStack ); + if ( hNode & 1 ) // extrated second time + { + Vec_IntPush( vUsed, hNode >> 1 ); continue; - assert( pNew - Vec_IntArray(p) == pNode->Label ); - pNode->Label = 0; - pBeg = (int *)pNode; - pEnd = pBeg + Sat_SetSize(pNode); - while ( pBeg < pEnd ) - *pNew++ = *pBeg++; + } + // extracted first time + Vec_IntPush( vStack, hNode ^ 1 ); // add second time + // add its anticedents ; + pNode = Proof_NodeRead( p, hNode >> 1 ); + Proof_NodeForeachFanin( p, pNode, pNext, i ) + if ( pNext && !pNext->Id ) + { + pNext->Id = 1; + Vec_IntPush( vStack, Proof_NodeHandle(p, pNext) << 1 ); // add first time + } } - // report the result - printf( "The proof was reduced from %d to %d (by %6.2f %%)\n", - Vec_IntSize(p), nSize, 100.0 * (Vec_IntSize(p) - nSize) / Vec_IntSize(p) ); - assert( pNew - Vec_IntArray(p) == nSize ); - Vec_IntShrink( p, nSize ); -} +} /**Function************************************************************* @@ -192,80 +167,51 @@ void Sat_ProofReduce( Vec_Int_t * p, Vec_Int_t * vRoots ) SeeAlso [] ***********************************************************************/ -void Sat_ProofLabel( Vec_Int_t * p, Sat_Set_t * pNode, Vec_Int_t * vUsed, Vec_Int_t * vStack ) +void Proof_CollectUsedRec( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed ) { - Sat_Set_t * pNext; - int i, NodeId; - if ( pNode->Label ) + satset * pNext; + int i; + if ( pNode->Id ) return; - // start with node - pNode->Label = 1; - Vec_IntPush( vStack, Sat_SetId(p, pNode) ); - // perform DFS search - while ( Vec_IntSize(vStack) ) - { - NodeId = Vec_IntPop( vStack ); - if ( NodeId & 1 ) // extrated second time - { - Vec_IntPush( vUsed, NodeId ^ 1 ); - continue; - } - // extracted first time - // add second time - Vec_IntPush( vStack, NodeId ^ 1 ); - // add its anticedents - pNode = Sat_SetFromId( p, NodeId ); - Sat_SetForEachSet( p, pNode, pNext, i ) - if ( pNext && !pNext->Label ) - { - pNext->Label = 1; - Vec_IntPush( vStack, Sat_SetId(p, pNode) ); // add first time - } - } + pNode->Id = 1; + Proof_NodeForeachFanin( p, pNode, pNext, i ) + if ( pNext && !pNext->Id ) + Proof_CollectUsedRec( p, pNext, vUsed ); + Vec_IntPush( vUsed, Proof_NodeHandle(p, pNode) ); } /**Function************************************************************* - Synopsis [Computes UNSAT core.] + Synopsis [Recursively visits useful proof nodes.] - Description [The result is the array of root clause indexes.] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -Vec_Int_t * Sat_ProofCore( Vec_Int_t * p, int nRoots, int * pBeg, int * pEnd ) +Vec_Int_t * Proof_CollectUsed( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hRoot ) { - unsigned * pSeen; - Vec_Int_t * vCore, * vUsed, * vStack; - Sat_Set_t * pNode; - int i; - // collect visited clauses + Vec_Int_t * vUsed, * vStack; + assert( (hRoot > 0) ^ (vRoots != NULL) ); vUsed = Vec_IntAlloc( 1000 ); vStack = Vec_IntAlloc( 1000 ); - while ( pBeg < pEnd ) - Sat_ProofLabel( p, Sat_SetFromId(p, *pBeg++), vUsed, vStack ); - Vec_IntFree( vStack ); - // find the core - vCore = Vec_IntAlloc( 1000 ); - pSeen = ABC_CALLOC( unsigned, Aig_BitWordNum(nRoots) ); - Sat_VecForEachSet( vUsed, p, pNode, i ) + if ( hRoot ) +// Proof_CollectUsedInt( vProof, Proof_NodeRead(vProof, hRoot), vUsed, vStack ); + Proof_CollectUsedRec( vProof, Proof_NodeRead(vProof, hRoot), vUsed ); + else { - pNode->Label = 0; - for ( pBeg = pNode->pEnts; pBeg < pNode->pEnts + pNode->nEnts; pBeg++ ) - if ( (*pBeg & 1) && !Aig_InfoHasBit(pBeg, *pBeg>>1) ) - { - Aig_InfoSetBit( pBeg, *pBeg>>1 ); - Vec_IntPush( vCore, (*pBeg>>1)-1 ); - } + satset * pNode; + int i; + Proof_ForeachNodeVec( vRoots, vProof, pNode, i ) +// Proof_CollectUsedInt( vProof, pNode, vUsed, vStack ); + Proof_CollectUsedRec( vProof, pNode, vUsed ); } - Vec_IntFree( vUsed ); - ABC_FREE( pSeen ); - return vCore; + Vec_IntFree( vStack ); + return vUsed; } - - + /**Function************************************************************* Synopsis [Performs one resultion step.] @@ -277,12 +223,14 @@ Vec_Int_t * Sat_ProofCore( Vec_Int_t * p, int nRoots, int * pBeg, int * pEnd ) SeeAlso [] ***********************************************************************/ -Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 ) +satset * Proof_ResolveOne( Vec_Int_t * p, satset * c1, satset * c2 ) { + satset * c; int i, k, Id, Var = -1, Count = 0; + // find resolution variable - for ( i = 0; i < c1->nEnts; i++ ) - for ( k = 0; k < c2->nEnts; k++ ) + 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); @@ -302,7 +250,7 @@ Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 ) Id = Vec_IntSize( p ); Vec_IntPush( p, 0 ); // placeholder Vec_IntPush( p, 0 ); - for ( i = 0; i < c1->nEnts; i++ ) + for ( i = 0; i < (int)c1->nEnts; i++ ) { if ( (c1->pEnts[i] >> 1) == Var ) continue; @@ -312,7 +260,7 @@ Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 ) if ( k == Vec_IntSize(p) ) Vec_IntPush( p, c1->pEnts[i] ); } - for ( i = 0; i < c2->nEnts; i++ ) + for ( i = 0; i < (int)c2->nEnts; i++ ) { if ( (c2->pEnts[i] >> 1) == Var ) continue; @@ -322,8 +270,9 @@ Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 ) if ( k == Vec_IntSize(p) ) Vec_IntPush( p, c2->pEnts[i] ); } - Vec_IntWriteEntry( p, Id, Vec_IntSize(p) - Id - 2 ); - return Sat_SetFromId( p, Id ); + c = Proof_NodeRead( p, Id ); + c->nEnts = Vec_IntSize(p) - Id - 2; + return c; } /**Function************************************************************* @@ -337,13 +286,15 @@ Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 ) SeeAlso [] ***********************************************************************/ -Sat_Set_t * Sat_ProofCheckGetOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vResolves, int iAnt ) +satset * Proof_CheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vResolves, int iAnt ) { - Sat_Set_t * pAnt; + satset * pAnt; if ( iAnt & 1 ) - return Sat_SetFromId( vClauses, iAnt >> 1 ); - pAnt = Sat_SetFromId( vProof, iAnt ); - return Sat_SetFromId( vResolves, pAnt->Label ); + return Proof_NodeRead( vClauses, iAnt >> 1 ); + assert( iAnt > 0 ); + pAnt = Proof_NodeRead( vProof, iAnt >> 1 ); + assert( pAnt->Id > 0 ); + return Proof_NodeRead( vResolves, pAnt->Id ); } /**Function************************************************************* @@ -357,117 +308,247 @@ Sat_Set_t * Sat_ProofCheckGetOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_ SeeAlso [] ***********************************************************************/ -void Sat_ProofCheck( Vec_Int_t * vClauses, Vec_Int_t * vProof, int iRoot ) +void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot ) { - Vec_Int_t * vOrigs, * vStack, * vUsed, * vResolves; - Sat_Set_t * pSet, * pSet0, * pSet1; - int i, k; - // collect original clauses - vOrigs = Vec_IntAlloc( 1000 ); - Vec_IntPush( vOrigs, -1 ); - Sat_PoolForEachSet( vClauses, pSet, i ) - Vec_IntPush( vOrigs, Sat_SetId(vClauses, pSet) ); + Vec_Int_t * vUsed, * vResolves; + satset * pSet, * pSet0, * pSet1; + int i, k, Counter = 0; // collect visited clauses - vUsed = Vec_IntAlloc( 1000 ); - vStack = Vec_IntAlloc( 1000 ); - Sat_ProofLabel( vProof, Sat_SetFromId(vProof, iRoot), vUsed, vStack ); - Vec_IntFree( vStack ); + vUsed = Proof_CollectUsed( vProof, NULL, hRoot ); + Proof_CleanCollected( vProof, vUsed ); // perform resolution steps vResolves = Vec_IntAlloc( 1000 ); Vec_IntPush( vResolves, -1 ); - Sat_VecForEachSet( vUsed, vProof, pSet, i ) + Proof_ForeachNodeVec( vUsed, vProof, pSet, i ) { - pSet0 = Sat_ProofCheckGetOne( vOrigs, vProof, vResolves, pSet->pEnts[0] ); - for ( k = 1; k < pSet->nEnts; k++ ) + pSet0 = Proof_CheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] ); + for ( k = 1; k < (int)pSet->nEnts; k++ ) { - pSet1 = Sat_ProofCheckGetOne( vOrigs, vProof, vResolves, pSet->pEnts[k] ); - pSet0 = Sat_ProofResolve( vResolves, pSet0, pSet1 ); + pSet1 = Proof_CheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] ); + pSet0 = Proof_ResolveOne( vResolves, pSet0, pSet1 ); } - pSet->Label = Sat_SetId( vResolves, pSet0 ); + pSet->Id = Proof_NodeHandle( vResolves, pSet0 ); + Counter++; } // clean the proof - Sat_VecForEachSet( vUsed, vProof, pSet, i ) - pSet->Label = 0; + Proof_ForeachNodeVec( vUsed, vProof, pSet, i ) + pSet->Id = 0; // compare the final clause if ( pSet0->nEnts > 0 ) printf( "Cound not derive the empty clause\n" ); Vec_IntFree( vResolves ); Vec_IntFree( vUsed ); - Vec_IntFree( vOrigs ); } + + + /**Function************************************************************* - Synopsis [Creates variable map.] + Synopsis [Recursively visits useful proof nodes.] - Description [1=A, 2=B, neg=global] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -void Sat_ProofVarMapCheck( Vec_Int_t * vClauses, Vec_Int_t * vVarMap ) +int Sat_ProofReduceOne( Vec_Int_t * p, satset * pNode, int * pnSize, Vec_Int_t * vStack ) { - Sat_Set_t * pSet; - int i, k, fSeeA, fSeeB; - // make sure all clauses are either A or B - Sat_PoolForEachSet( vClauses, pSet, i ) + satset * pNext; + int i, NodeId; + if ( pNode->Id ) + return pNode->Id; + // start with node + pNode->Id = 1; + Vec_IntPush( vStack, Proof_NodeHandle(p, pNode) ); + // perform DFS search + while ( Vec_IntSize(vStack) ) { - fSeeA = fSeeB = 0; - for ( k = 0; k < pSet->nEnts; k++ ) + NodeId = Vec_IntPop( vStack ); + if ( NodeId & 1 ) // extrated second time { - fSeeA += (Vec_IntEntry(vVarMap, pSet->pEnts[k]) == 1); - fSeeB += (Vec_IntEntry(vVarMap, pSet->pEnts[k]) == 2); + pNode = Proof_NodeRead( p, NodeId ^ 1 ); + pNode->Id = *pnSize; + *pnSize += Proof_NodeSize(pNode->nEnts); + // update fanins + Proof_NodeForeachFanin( p, pNode, pNext, i ) + if ( pNext ) + pNode->pEnts[i] = pNext->Id; + continue; } - if ( fSeeA && fSeeB ) - printf( "VarMap error!\n" ); + // extracted first time + // add second time + Vec_IntPush( vStack, NodeId ^ 1 ); + // add its anticedents + pNode = Proof_NodeRead( p, NodeId ); + Proof_NodeForeachFanin( p, pNode, pNext, i ) + if ( pNext && !pNext->Id ) + { + pNext->Id = 1; + Vec_IntPush( vStack, Proof_NodeHandle(p, pNode) ); // add first time + } + } + return pNode->Id; +} + +/**Function************************************************************* + + Synopsis [Reduces the proof to contain only roots and their children.] + + Description [The result is updated proof and updated roots.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sat_ProofReduce( Vec_Int_t * p, Vec_Int_t * vRoots ) +{ + int i, nSize = 1; + int * pBeg, * pEnd, * pNew; + Vec_Int_t * vStack; + satset * pNode; + // mark used nodes + vStack = Vec_IntAlloc( 1000 ); + Proof_ForeachNodeVec( vRoots, p, pNode, i ) + vRoots->pArray[i] = Sat_ProofReduceOne( p, pNode, &nSize, vStack ); + Vec_IntFree( vStack ); + // compact proof + pNew = Vec_IntArray(p) + 1; + Proof_ForeachNode( p, pNode, i ) + { + if ( !pNode->Id ) + continue; + assert( pNew - Vec_IntArray(p) == pNode->Id ); + pNode->Id = 0; + pBeg = (int *)pNode; + pEnd = pBeg + Proof_NodeSize(pNode->nEnts); + while ( pBeg < pEnd ) + *pNew++ = *pBeg++; + } + // report the result + printf( "The proof was reduced from %d to %d (by %6.2f %%)\n", + Vec_IntSize(p), nSize, 100.0 * (Vec_IntSize(p) - nSize) / Vec_IntSize(p) ); + assert( pNew - Vec_IntArray(p) == nSize ); + Vec_IntShrink( p, nSize ); +} + +/**Function************************************************************* + + Synopsis [Computes UNSAT core.] + + Description [The result is the array of root clause indexes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Sat_ProofCore( Vec_Int_t * vProof, int nRoots, Vec_Int_t * vRoots ) +{ + unsigned * pSeen; + Vec_Int_t * vCore, * vUsed; + satset * pNode; + int i, * pBeg; + // collect visited clauses + vUsed = Proof_CollectUsed( vProof, vRoots, 0 ); + // find the core + vCore = Vec_IntAlloc( 1000 ); + pSeen = ABC_CALLOC( unsigned, Aig_BitWordNum(nRoots) ); + Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) + { + pNode->Id = 0; + for ( pBeg = pNode->pEnts; pBeg < pNode->pEnts + pNode->nEnts; pBeg++ ) + if ( (*pBeg & 1) && !Aig_InfoHasBit(pBeg, *pBeg>>1) ) + { + Aig_InfoSetBit( pBeg, *pBeg>>1 ); + Vec_IntPush( vCore, (*pBeg>>1)-1 ); + } } + Vec_IntFree( vUsed ); + ABC_FREE( pSeen ); + return vCore; } /**Function************************************************************* Synopsis [Computes interpolant of the proof.] - Description [Assuming that res vars are recorded, too...] + Description [Aassuming that global vars and A-clauses are marked.] SideEffects [] SeeAlso [] ***********************************************************************/ -Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vProof, int iRoot, Vec_Int_t * vClauses, Vec_Int_t * vVarMap ) +Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot, Vec_Int_t * vGlobVars ) { - Vec_Int_t * vOrigs, * vUsed, * vStack; + Vec_Int_t * vUsed; Aig_Man_t * pAig; - Sat_Set_t * pSet; int i; - Sat_ProofVarMapCheck( vClauses, vVarMap ); - - // collect original clauses - vOrigs = Vec_IntAlloc( 1000 ); - Vec_IntPush( vOrigs, -1 ); - Sat_PoolForEachSet( vClauses, pSet, i ) - Vec_IntPush( vOrigs, Sat_SetId(vClauses, pSet) ); - // collect visited clauses - vUsed = Vec_IntAlloc( 1000 ); - vStack = Vec_IntAlloc( 1000 ); - Sat_ProofLabel( vProof, Sat_SetFromId(vProof, iRoot), vUsed, vStack ); - Vec_IntFree( vStack ); + vUsed = Proof_CollectUsed( vProof, NULL, hRoot ); // start the AIG pAig = Aig_ManStart( 10000 ); pAig->pName = Aig_UtilStrsav( "interpol" ); - for ( i = 0; i < Vec_IntSize(vVarMap); i++ ) - if ( Vec_IntEntry(vVarMap, i) < 0 ) - Aig_ObjCreatePi( pAig ); + for ( i = 0; i < Vec_IntSize(vGlobVars); i++ ) + Aig_ObjCreatePi( pAig ); return pAig; } +/* + Sat_ProofTest( + &s->clauses, // clauses + &s->proof_clas, // proof clauses + &s->proof_vars, // proof variables + NULL, // proof roots + veci_begin(&s->claProofs)[clause_read(s, s->iLearntLast)->Id)], // one root + &s->glob_vars ); // global variables (for interpolation) +*/ + +/**Function************************************************************* + + Synopsis [Computes interpolant of the proof.] + + Description [Aassuming that global vars and A-clauses are marked.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pVars, veci * pRoots, int hRoot, veci * pGlobVars ) +{ + Vec_Int_t * vClauses = (Vec_Int_t *)pClauses; + Vec_Int_t * vProof = (Vec_Int_t *)pProof; + Vec_Int_t * vVars = (Vec_Int_t *)pVars; + Vec_Int_t * vRoots = (Vec_Int_t *)pRoots; + Vec_Int_t * vGlobVars = (Vec_Int_t *)pGlobVars; + Vec_Int_t * vUsed; +// int i, Entry; + + // collect visited clauses + vUsed = Proof_CollectUsed( vProof, NULL, hRoot ); + Proof_CleanCollected( vProof, vUsed ); +// Vec_IntForEachEntry( vUsed, Entry, i ) +// printf( "%d ", Entry ); +// printf( "\n" ); + + printf( "Found %d useful resolution nodes.\n", Vec_IntSize(vUsed) ); + Vec_IntFree( vUsed ); + vUsed = Proof_CollectAll( vProof ); + printf( "Found %d total resolution nodes.\n", Vec_IntSize(vUsed) ); + Vec_IntFree( vUsed ); + + Proof_Check( vClauses, vProof, hRoot ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 72e36894..a7628239 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -86,12 +86,12 @@ struct varinfo_t unsigned val : 2; // variable value unsigned pol : 1; // last polarity unsigned glo : 1; // global variable - unsigned tag : 3; // conflict analysis tags - unsigned lev : 25; // variable level + unsigned tag : 4; // conflict analysis tags + unsigned lev : 24; // variable level }; int var_is_global (sat_solver2* s, int v) { return s->vi[v].glo; } -void var_set_global(sat_solver2* s, int v, int glo) { s->vi[v].glo = glo; } +void var_set_global(sat_solver2* s, int v, int glo) { s->vi[v].glo = glo; if (glo) veci_push(&s->glob_vars, v); } static inline int var_value (sat_solver2* s, int v) { return s->vi[v].val; } static inline int var_polar (sat_solver2* s, int v) { return s->vi[v].pol; } @@ -104,13 +104,13 @@ static inline void var_set_level (sat_solver2* s, int v, int lev) { s->vi[v // variable tags static inline int var_tag (sat_solver2* s, int v) { return s->vi[v].tag; } static inline void var_set_tag (sat_solver2* s, int v, int tag) { - assert( tag > 0 && tag < 8 ); + assert( tag > 0 && tag < 16 ); if ( s->vi[v].tag == 0 ) veci_push( &s->tagged, v ); s->vi[v].tag = tag; } static inline void var_add_tag (sat_solver2* s, int v, int tag) { - assert( tag > 0 && tag < 8 ); + assert( tag > 0 && tag < 16 ); if ( s->vi[v].tag == 0 ) veci_push( &s->tagged, v ); s->vi[v].tag |= tag; @@ -139,44 +139,30 @@ static inline void solver2_clear_marks(sat_solver2* s) { veci_resize(&s->mark_levels,0); } -// other inlines -//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 int var_reason (sat_solver2* s, int v) { return s->reasons[v]; } -static inline int lit_reason (sat_solver2* s, int l) { return s->reasons[lit_var(l)]; } - //================================================================================================= // Clause datatype + minor functions: -typedef struct satset_t satset; -struct satset_t -{ - unsigned learnt : 1; - unsigned mark : 1; - unsigned partA : 1; - unsigned nLits : 29; - int Id; - lit pLits[0]; -}; - -static inline satset* get_clause (sat_solver2* s, int c) { return c ? (satset*)(veci_begin(&s->clauses) + c) : NULL; } -static inline cla clause_id (sat_solver2* s, satset* c) { return (cla)((int *)c - veci_begin(&s->clauses)); } -static inline int clause_size (int nLits) { return sizeof(satset)/4 + nLits; } -static inline int clause_proofid(sat_solver2* s, satset* c) { return c->learnt ? veci_begin(&s->claProofs)[c->Id]<<1 : (clause_id(s,c)<<1) | 1; } +static inline satset* clause_read (sat_solver2* s, cla h) { return satset_read( &s->clauses, h ); } +static inline cla clause_handle (sat_solver2* s, satset* c) { return satset_handle( &s->clauses, c ); } +static inline int clause_check (sat_solver2* s, satset* c) { return satset_check( &s->clauses, c ); } +static inline int clause_proofid(sat_solver2* s, satset* c) { return c->learnt ? veci_begin(&s->claProofs)[c->Id]<<1 : (clause_handle(s,c)<<1) | 1; } + +//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; } +//static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(i && !s->reasons[v]); s->reasons[v] = (i << 1) | 1; } +static inline int var_reason (sat_solver2* s, int v) { return s->reasons[v]; } +static inline int lit_reason (sat_solver2* s, int l) { return s->reasons[lit_var(l)]; } +static inline satset* var_unit_clause(sat_solver2* s, int v) { return clause_read(s, s->units[v]); } +static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size && !s->units[v]); s->units[v] = i; s->nUnits++; } // these two only work after creating a clause before the solver is called -int clause_is_partA (sat_solver2* s, int cid) { return get_clause(s, cid)->partA; } -void clause_set_partA(sat_solver2* s, int cid, int partA) { get_clause(s, cid)->partA = partA; } - -//static inline satset* var_unit_clause(sat_solver2* s, int v) { return (s->reasons[v]&1) ? get_clause(s, s->reasons[v] >> 1) : NULL; } -//static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(i && !s->reasons[v]); s->reasons[v] = (i << 1) | 1; } -static inline satset* var_unit_clause(sat_solver2* s, int v) { return get_clause(s, s->units[v]); } -static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size && !s->units[v]); s->units[v] = i; s->nUnits++; } +int clause_is_partA (sat_solver2* s, int h) { return clause_read(s, h)->partA; } +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, i ) \ - for ( i = 1; (i < s->nMemSize) && (((c) = get_clause(s, i)), 1); i += clause_size(c->nLits) ) -#define sat_solver_foreach_learnt( s, c, i ) \ - for ( i = s->iFirstLearnt; (i < s->nMemSize) && (((c) = get_clause(s, i)), 1); i += clause_size(c->nLits) ) +#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->clauses, c, h, s->iLearntFirst ) //================================================================================================= // Simple helpers: @@ -219,7 +205,7 @@ static inline int proof_chain_stop( sat_solver2* s ) int RetValue = s->iStartChain; satset* c = (satset*)(veci_begin(&s->proof_clas) + s->iStartChain); assert( s->iStartChain > 0 && s->iStartChain < veci_size(&s->proof_clas) ); - c->nLits = veci_size(&s->proof_clas) - s->iStartChain - 2; + c->nEnts = veci_size(&s->proof_clas) - s->iStartChain - 2; s->iStartChain = 0; return RetValue; } @@ -396,11 +382,11 @@ static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proo assert(nLits < 1 || lit_var(begin[0]) < s->size); assert(nLits < 2 || lit_var(begin[1]) < s->size); // add memory if needed - if ( veci_size(&s->clauses) + clause_size(nLits) > s->clauses.cap ) + if ( veci_size(&s->clauses) + satset_size(nLits) > s->clauses.cap ) { int nMemAlloc = s->clauses.cap ? 2 * s->clauses.cap : (1 << 20); s->clauses.ptr = ABC_REALLOC( int, veci_begin(&s->clauses), nMemAlloc ); - memset( veci_begin(&s->clauses) + s->clauses.cap, 0, sizeof(int) * (nMemAlloc - s->clauses.cap) ); +// memset( veci_begin(&s->clauses) + s->clauses.cap, 0, sizeof(int) * (nMemAlloc - s->clauses.cap) ); // printf( "Reallocing from %d to %d...\n", s->clauses.cap, nMemAlloc ); s->clauses.cap = nMemAlloc; if ( veci_size(&s->clauses) == 0 ) @@ -408,10 +394,11 @@ static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proo } // create clause c = (satset*)(veci_begin(&s->clauses) + veci_size(&s->clauses)); + ((int*)c)[0] = 0; c->learnt = learnt; - c->nLits = nLits; + c->nEnts = nLits; for (i = 0; i < nLits; i++) - c->pLits[i] = begin[i]; + c->pEnts[i] = begin[i]; // assign clause ID if ( learnt ) { @@ -434,14 +421,14 @@ static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proo // extend storage Cid = veci_size(&s->clauses); - s->clauses.size += clause_size(nLits); + s->clauses.size += satset_size(nLits); assert( veci_size(&s->clauses) <= s->clauses.cap ); assert(((ABC_PTRUINT_T)c & 3) == 0); // remember the last one and first learnt - s->fLastConfId = Cid; - if ( learnt && s->iFirstLearnt == -1 ) - s->iFirstLearnt = Cid; + s->iLearntLast = Cid; + if ( learnt && s->iLearntFirst == -1 ) + s->iLearntFirst = Cid; // watch the clause if ( nLits > 1 ){ @@ -614,9 +601,9 @@ static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first) return -1; proof_chain_start( s, conf ); assert( veci_size(&s->tagged) == 0 ); - for ( i = skip_first; i < (int)conf->nLits; i++ ) + for ( i = skip_first; i < (int)conf->nEnts; i++ ) { - x = lit_var(conf->pLits[i]); + x = lit_var(conf->pEnts[i]); if ( var_level(s,x) ) var_set_tag(s, x, 1); else @@ -627,11 +614,11 @@ static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first) for (i = s->qtail-1; i >= (veci_begin(&s->trail_lim))[0]; i--){ x = lit_var(s->trail[i]); if (var_tag(s,x)){ - satset* c = get_clause(s, var_reason(s,x)); + satset* c = clause_read(s, var_reason(s,x)); if (c){ proof_chain_resolve( s, c, x ); - for (j = 1; j < (int)c->nLits; j++) { - x = lit_var(c->pLits[j]); + for (j = 1; j < (int)c->nEnts; j++) { + x = lit_var(c->pEnts[j]); if ( var_level(s,x) ) var_set_tag(s, x, 1); else @@ -664,14 +651,14 @@ static int solver2_lit_removable_rec(sat_solver2* s, int v) return (var_tag(s,v) & 4) > 0; // skip decisions on a wrong level - c = get_clause(s, var_reason(s,v)); + c = clause_read(s, var_reason(s,v)); if ( c == NULL ){ var_add_tag(s,v,2); return 0; } - for ( i = 1; i < (int)c->nLits; i++ ){ - x = lit_var(c->pLits[i]); + for ( i = 1; i < (int)c->nEnts; i++ ){ + x = lit_var(c->pEnts[i]); if (var_tag(s,x) & 1) solver2_lit_removable_rec(s, x); else{ @@ -715,9 +702,9 @@ static int solver2_lit_removable(sat_solver2* s, int x) veci_push(&s->stack, x ^ 1 ); } x >>= 1; - c = get_clause(s, var_reason(s,x)); - for (i = 1; i < (int)c->nLits; i++){ - x = lit_var(c->pLits[i]); + c = clause_read(s, var_reason(s,x)); + for (i = 1; i < (int)c->nEnts; i++){ + x = lit_var(c->pEnts[i]); if (var_tag(s,x) || !var_level(s,x)) continue; if (!var_reason(s,x) || !var_lev_mark(s,x)){ @@ -749,11 +736,11 @@ static void solver2_logging_order(sat_solver2* s, int x) } veci_push(&s->stack, x ^ 1 ); x >>= 1; - c = get_clause(s, var_reason(s,x)); + c = clause_read(s, var_reason(s,x)); // if ( !c ) // printf( "solver2_logging_order(): Error in conflict analysis!!!\n" ); - for (i = 1; i < (int)c->nLits; i++){ - x = lit_var(c->pLits[i]); + for (i = 1; i < (int)c->nEnts; i++){ + x = lit_var(c->pEnts[i]); if ( !var_level(s,x) || (var_tag(s,x) & 1) ) continue; veci_push(&s->stack, x << 1); @@ -762,6 +749,22 @@ static void solver2_logging_order(sat_solver2* s, int x) } } +static void solver2_logging_order_rec(sat_solver2* s, int x) +{ + satset* c; + int i, y; + if ( (var_tag(s,x) & 8) ) + return; + c = clause_read(s, var_reason(s,x)); + for (i = 1; i < (int)c->nEnts; i++){ + y = lit_var(c->pEnts[i]); + if ( var_level(s,y) && (var_tag(s,y) & 1) == 0 ) + solver2_logging_order_rec(s, y); + } + var_add_tag(s, x, 8); + veci_push(&s->min_step_order, x); +} + static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt) { int cnt = 0; @@ -780,8 +783,8 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt) assert(c != 0); if (c->learnt) act_clause_bump(s,c); - for ( j = (int)(p != lit_Undef); j < (int)c->nLits; j++){ - x = lit_var(c->pLits[j]); + for ( j = (int)(p != lit_Undef); j < (int)c->nEnts; j++){ + x = lit_var(c->pEnts[j]); assert(x >= 0 && x < s->size); if ( var_tag(s, x) ) continue; @@ -795,13 +798,13 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt) if (var_level(s,x) == solver2_dlevel(s)) cnt++; else - veci_push(learnt,c->pLits[j]); + veci_push(learnt,c->pEnts[j]); } while (!var_tag(s, lit_var(s->trail[ind--]))); p = s->trail[ind+1]; - c = get_clause(s, lit_reason(s,p)); + c = clause_read(s, lit_reason(s,p)); cnt--; if ( cnt == 0 ) break; @@ -818,8 +821,8 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt) // simplify (full) veci_resize(&s->min_lit_order, 0); for (i = j = 1; i < veci_size(learnt); i++){ -// if (!solver2_lit_removable_rec(s,lit_var(lits[i]))) // changed to vars!!! - if (!solver2_lit_removable( s,lit_var(lits[i])) ) +// if (!solver2_lit_removable( s,lit_var(lits[i])) ) + if (!solver2_lit_removable_rec(s,lit_var(lits[i]))) // changed to vars!!! lits[j++] = lits[i]; } @@ -830,16 +833,17 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt) veci_resize(&s->min_step_order, 0); vars = veci_begin(&s->min_lit_order); for (i = 0; i < veci_size(&s->min_lit_order); i++) - solver2_logging_order( s, vars[i] ); +// solver2_logging_order( s, vars[i] ); + solver2_logging_order_rec( s, vars[i] ); // add them in the reverse order vars = veci_begin(&s->min_step_order); for (i = veci_size(&s->min_step_order); i > 0; ) { i--; - c = get_clause(s, var_reason(s,vars[i])); + c = clause_read(s, var_reason(s,vars[i])); proof_chain_resolve( s, c, vars[i] ); - for ( k = 1; k < (int)c->nLits; k++ ) + for ( k = 1; k < (int)c->nEnts; k++ ) { - x = lit_var(c->pLits[k]); + x = lit_var(c->pEnts[k]); if ( var_level(s,x) == 0 ) proof_chain_resolve( s, NULL, x ); } @@ -908,8 +912,8 @@ satset* solver2_propagate(sat_solver2* s) s->simpdb_props--; for (i = j = begin; i < end; ){ - c = get_clause(s,*i); - lits = c->pLits; + c = clause_read(s,*i); + lits = c->pEnts; // Make sure the false literal is data[1]: false_lit = lit_neg(p); @@ -924,7 +928,7 @@ satset* solver2_propagate(sat_solver2* s) *j++ = *i; else{ // Look for new watch: - stop = lits + c->nLits; + stop = lits + c->nEnts; for (k = lits + 2; k < stop; k++){ if (var_value(s, lit_var(*k)) != !lit_sign(*k)){ lits[1] = *k; @@ -939,9 +943,9 @@ satset* solver2_propagate(sat_solver2* s) int fLitIsFalse = (var_value(s, Var) == !lit_sign(lits[0])); // Log production of top-level unit clause: proof_chain_start( s, c ); - for ( k = 1; k < (int)c->nLits; k++ ) + for ( k = 1; k < (int)c->nEnts; k++ ) { - int x = lit_var(c->pLits[k]); + int x = lit_var(c->pEnts[k]); assert( var_level(s, x) == 0 ); proof_chain_resolve( s, NULL, x ); } @@ -955,7 +959,7 @@ satset* solver2_propagate(sat_solver2* s) var_set_unit_clause(s, Var, Cid); else{ // Empty clause derived: - proof_chain_start( s, get_clause(s,Cid) ); + proof_chain_start( s, clause_read(s,Cid) ); proof_chain_resolve( s, NULL, Var ); proof_id = proof_chain_stop( s ); clause_new( s, lits, lits, 1, proof_id ); @@ -965,7 +969,7 @@ satset* solver2_propagate(sat_solver2* s) *j++ = *i; // Clause is unit under assignment: if (!solver2_enqueue(s,lits[0], *i)){ - confl = get_clause(s,*i++); + confl = clause_read(s,*i++); // Copy the remaining watches: while (i < end) *j++ = *i++; @@ -984,18 +988,18 @@ WatchFound: i++; static void clause_remove(sat_solver2* s, satset* c) { - assert(lit_neg(c->pLits[0]) < s->size*2); - assert(lit_neg(c->pLits[1]) < s->size*2); + assert(lit_neg(c->pEnts[0]) < s->size*2); + assert(lit_neg(c->pEnts[1]) < s->size*2); - veci_remove(solver2_wlist(s,lit_neg(c->pLits[0])),clause_id(s,c)); - veci_remove(solver2_wlist(s,lit_neg(c->pLits[1])),clause_id(s,c)); + veci_remove(solver2_wlist(s,lit_neg(c->pEnts[0])),clause_handle(s,c)); + veci_remove(solver2_wlist(s,lit_neg(c->pEnts[1])),clause_handle(s,c)); if (c->learnt){ s->stats.learnts--; - s->stats.learnts_literals -= c->nLits; + s->stats.learnts_literals -= c->nEnts; }else{ s->stats.clauses--; - s->stats.clauses_literals -= c->nLits; + s->stats.clauses_literals -= c->nEnts; } } @@ -1004,8 +1008,8 @@ static lbool clause_simplify(sat_solver2* s, satset* c) { int i; assert(solver2_dlevel(s) == 0); - for (i = 0; i < (int)c->nLits; i++){ - if (var_value(s, lit_var(c->pLits[i])) == lit_sign(c->pLits[i])) + for (i = 0; i < (int)c->nEnts; i++){ + if (var_value(s, lit_var(c->pEnts[i])) == lit_sign(c->pEnts[i])) return l_True; } return l_False; @@ -1026,8 +1030,8 @@ int sat_solver2_simplify(sat_solver2* s) int* cls = (int*)veci_begin(cs); int i, j; for (j = i = 0; i < veci_size(cs); i++){ - satset* c = get_clause(s,cls[i]); - if (lit_reason(s,c->pLits[0]) != cls[i] && + satset* c = clause_read(s,cls[i]); + if (lit_reason(s,c->pEnts[0]) != cls[i] && clause_simplify(s,c) == l_True) clause_remove(s,c), Counter++; else @@ -1067,7 +1071,7 @@ void solver2_reducedb(sat_solver2* s) { assert( c->Id == k ); c->mark = 0; - if ( c->nLits > 2 && lit_reason(s,c->pLits[0]) != Cid && (k < nLearnts/2 || pActs[k] < extra_lim) ) + if ( c->nEnts > 2 && lit_reason(s,c->pEnts[0]) != Cid && (k < nLearnts/2 || pActs[k] < extra_lim) ) { c->mark = 1; Counter++; @@ -1216,14 +1220,15 @@ sat_solver2* sat_solver2_new(void) veci_new(&s->mark_levels); veci_new(&s->min_lit_order); veci_new(&s->min_step_order); + veci_new(&s->glob_vars); veci_new(&s->proof_clas); veci_push(&s->proof_clas, -1); veci_new(&s->proof_vars); veci_push(&s->proof_vars, -1); veci_new(&s->claActs); veci_push(&s->claActs, -1); veci_new(&s->claProofs); veci_push(&s->claProofs, -1); // initialize other - s->iFirstLearnt = -1; // the first learnt clause - s->fLastConfId = -1; // the last learnt clause + s->iLearntFirst = -1; // the first learnt clause + s->iLearntLast = -1; // the last learnt clause #ifdef USE_FLOAT_ACTIVITY s->var_inc = 1; s->cla_inc = 1; @@ -1245,9 +1250,9 @@ sat_solver2* sat_solver2_new(void) if ( s->fProofLogging ) { s->proof_clas.cap = (1 << 20); - s->proof_clas.ptr = ABC_ALLOC( int, s->proof_clas.cap ); + s->proof_clas.ptr = ABC_REALLOC( int, s->proof_clas.ptr, s->proof_clas.cap ); s->proof_vars.cap = (1 << 20); - s->proof_vars.ptr = ABC_ALLOC( int, s->proof_clas.cap ); + s->proof_vars.ptr = ABC_REALLOC( int, s->proof_vars.ptr, s->proof_clas.cap ); } return s; } @@ -1294,10 +1299,19 @@ void sat_solver2_setnvars(sat_solver2* s,int n) void sat_solver2_delete(sat_solver2* s) { + satset * c = clause_read(s, s->iLearntLast); // report statistics assert( veci_size(&s->proof_clas) == veci_size(&s->proof_vars) ); printf( "Used %6.2f Mb for proof-logging. Unit clauses = %d.\n", 8.0 * veci_size(&s->proof_clas) / (1<<20), s->nUnits ); + Sat_ProofTest( + &s->clauses, // clauses + &s->proof_clas, // proof clauses + &s->proof_vars, // proof variables + NULL, // proof roots + veci_begin(&s->claProofs)[c->Id], // one root + &s->glob_vars ); // global variables (for interpolation) + // delete vectors veci_delete(&s->order); veci_delete(&s->trail_lim); @@ -1309,6 +1323,7 @@ void sat_solver2_delete(sat_solver2* s) veci_delete(&s->mark_levels); veci_delete(&s->min_lit_order); veci_delete(&s->min_step_order); + veci_delete(&s->glob_vars); veci_delete(&s->proof_clas); veci_delete(&s->proof_vars); veci_delete(&s->claActs); @@ -1320,7 +1335,10 @@ void sat_solver2_delete(sat_solver2* s) int i; if ( s->wlists ) for (i = 0; i < s->size*2; i++) + { +// printf( "%d ", s->wlists[i].size ); veci_delete(&s->wlists[i]); + } ABC_FREE(s->wlists ); ABC_FREE(s->vi ); ABC_FREE(s->trail ); @@ -1461,7 +1479,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim // lbool* values = s->assigns; lit* i; - s->fLastConfId = -1; + s->iLearntLast = -1; // set the external limits // s->nCalls++; @@ -1542,7 +1560,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim veci_push(&s->trail_lim,s->qtail); if (!solver2_enqueue(s,p,0)) { - satset* r = get_clause(s, lit_reason(s,p)); + satset* r = clause_read(s, lit_reason(s,p)); if (r != NULL) { satset* confl = r; diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index c64a4213..1cdc8bd9 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -41,39 +41,41 @@ struct sat_solver2_t; typedef struct sat_solver2_t sat_solver2; extern sat_solver2* sat_solver2_new(void); -extern void sat_solver2_delete(sat_solver2* s); +extern void sat_solver2_delete(sat_solver2* s); -extern int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end); -extern int sat_solver2_simplify(sat_solver2* s); -extern int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); +extern int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end); +extern int sat_solver2_simplify(sat_solver2* s); +extern int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); -extern void sat_solver2_setnvars(sat_solver2* s,int n); +extern void sat_solver2_setnvars(sat_solver2* s,int n); -extern void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars ); -extern void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * p ); -extern int * Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars ); -extern void Sat_Solver2DoubleClauses( sat_solver2 * p, int iVar ); +extern void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars ); +extern void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * p ); +extern int * Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars ); +extern void Sat_Solver2DoubleClauses( sat_solver2 * p, int iVar ); // trace recording -extern void sat_solver2TraceStart( sat_solver2 * pSat, char * pName ); -extern void sat_solver2TraceStop( sat_solver2 * pSat ); -extern void sat_solver2TraceWrite( sat_solver2 * pSat, int * pBeg, int * pEnd, int fRoot ); +extern void sat_solver2TraceStart( sat_solver2 * pSat, char * pName ); +extern void sat_solver2TraceStop( sat_solver2 * pSat ); +extern void sat_solver2TraceWrite( sat_solver2 * pSat, int * pBeg, int * pEnd, int fRoot ); // clause storage -extern void sat_solver2_store_alloc( sat_solver2 * s ); -extern void sat_solver2_store_write( sat_solver2 * s, char * pFileName ); -extern void sat_solver2_store_free( sat_solver2 * s ); -extern void sat_solver2_store_mark_roots( sat_solver2 * s ); -extern void sat_solver2_store_mark_clauses_a( sat_solver2 * s ); -extern void * sat_solver2_store_release( sat_solver2 * s ); +extern void sat_solver2_store_alloc( sat_solver2 * s ); +extern void sat_solver2_store_write( sat_solver2 * s, char * pFileName ); +extern void sat_solver2_store_free( sat_solver2 * s ); +extern void sat_solver2_store_mark_roots( sat_solver2 * s ); +extern void sat_solver2_store_mark_clauses_a( sat_solver2 * s ); +extern void * sat_solver2_store_release( sat_solver2 * s ); // global variables -extern int var_is_global (sat_solver2* s, int v); -extern void var_set_global(sat_solver2* s, int v, int glo); +extern int var_is_global (sat_solver2* s, int v); +extern void var_set_global(sat_solver2* s, int v, int glo); // clause grouping (these two only work after creating a clause before the solver is called) -extern int clause_is_partA (sat_solver2* s, int cid); -extern void clause_set_partA(sat_solver2* s, int cid, int partA); - +extern int clause_is_partA (sat_solver2* s, int handle); +extern void clause_set_partA(sat_solver2* s, int handle, int partA); +// other clause functions +extern int clause_id(sat_solver2* s, int h); + //================================================================================================= // Solver representation: @@ -83,75 +85,105 @@ typedef struct varinfo_t varinfo; struct sat_solver2_t { - int size; // nof variables - int cap; // size of varmaps - int qhead; // Head index of queue. - int qtail; // Tail index of queue. - - int root_level; // Level of first proper decision. - int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'. - int simpdb_props; // Number of propagations before next 'simplifyDB()'. - double random_seed; - double progress_estimate; - int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything - int fNotUseRandom; // do not allow random decisions with a fixed probability -// int fSkipSimplify; // set to one to skip simplification of the clause database - int fProofLogging; // enable proof-logging + int size; // nof variables + int cap; // size of varmaps + int qhead; // Head index of queue. + int qtail; // Tail index of queue. + + int root_level; // Level of first proper decision. + int simpdb_assigns; // Number of top-level assignments at last 'simplifyDB()'. + int simpdb_props; // Number of propagations before next 'simplifyDB()'. + double random_seed; + double progress_estimate; + int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything + int fNotUseRandom; // do not allow random decisions with a fixed probability +// int fSkipSimplify; // set to one to skip simplification of the clause database + int fProofLogging; // enable proof-logging // clauses - veci clauses; // clause memory - veci* wlists; // watcher lists (for each literal) - int iFirstLearnt; // the first learnt clause + veci clauses; // clause memory + veci* wlists; // watcher lists (for each literal) + int iLearntFirst; // the first learnt clause + int iLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) // activities #ifdef USE_FLOAT_ACTIVITY - double var_inc; // Amount to bump next variable with. - double var_decay; // INVERSE decay factor for variable activity: stores 1/decay. - float cla_inc; // Amount to bump next clause with. - float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay. - double* activity; // A heuristic measurement of the activity of a variable. + double var_inc; // Amount to bump next variable with. + double var_decay; // INVERSE decay factor for variable activity: stores 1/decay. + float cla_inc; // Amount to bump next clause with. + float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay. + double* activity; // A heuristic measurement of the activity of a variable. #else - int var_inc; // Amount to bump next variable with. - int cla_inc; // Amount to bump next clause with. - unsigned* activity; // A heuristic measurement of the activity of a variable. + int var_inc; // Amount to bump next variable with. + int cla_inc; // Amount to bump next clause with. + unsigned* activity; // A heuristic measurement of the activity of a variable. #endif - veci claActs; // clause activities - veci claProofs; // clause proofs + veci claActs; // clause activities + veci claProofs; // clause proofs // internal state - varinfo * vi; // variable information - lit* trail; // sequence of assignment and implications - int* orderpos; // Index in variable order. - cla* reasons; // reason clauses - cla* units; // unit clauses - - veci tagged; // (contains: var) - veci stack; // (contains: var) - veci order; // Variable order. (heap) (contains: var) - veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int) - veci temp_clause; // temporary storage for a CNF clause - veci model; // If problem is solved, this vector contains the model (contains: lbool). - veci conf_final; // If problem is unsatisfiable (possibly under assumptions), - // this vector represent the final conflict clause expressed in the assumptions. - veci mark_levels; // temporary storage for labeled levels - veci min_lit_order; // ordering of removable literals - veci min_step_order;// ordering of resolution steps + varinfo * vi; // variable information + lit* trail; // sequence of assignment and implications + int* orderpos; // Index in variable order. + cla* reasons; // reason clauses + cla* units; // unit clauses + + veci tagged; // (contains: var) + veci stack; // (contains: var) + veci order; // Variable order. (heap) (contains: var) + veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int) + veci temp_clause; // temporary storage for a CNF clause + veci model; // If problem is solved, this vector contains the model (contains: lbool). + veci conf_final; // If problem is unsatisfiable (possibly under assumptions), + // this vector represent the final conflict clause expressed in the assumptions. + veci mark_levels; // temporary storage for labeled levels + veci min_lit_order; // ordering of removable literals + veci min_step_order; // ordering of resolution steps + veci glob_vars; // global variables // proof logging - veci proof_clas; // sequence of proof clauses - veci proof_vars; // sequence of proof variables - int iStartChain; // temporary variable to remember beginning of the current chain in proof logging - int fLastConfId; // in proof-logging mode, the ID of the final conflict clause (conf_final) - int nUnits; // the total number of unit clauses + veci proof_clas; // sequence of proof clauses + veci proof_vars; // sequence of proof variables + int iStartChain; // temporary variable to remember beginning of the current chain in proof logging + int nUnits; // the total number of unit clauses // statistics - stats_t stats; - ABC_INT64_T nConfLimit; // external limit on the number of conflicts - ABC_INT64_T nInsLimit; // external limit on the number of implications - int nRuntimeLimit; // external limit on runtime + stats_t stats; + ABC_INT64_T nConfLimit; // external limit on the number of conflicts + ABC_INT64_T nInsLimit; // external limit on the number of implications + int nRuntimeLimit; // external limit on runtime +}; +typedef struct satset_t satset; +struct satset_t +{ + unsigned learnt : 1; + unsigned mark : 1; + unsigned partA : 1; + unsigned nEnts : 29; + int Id; + lit pEnts[0]; }; +static inline satset* satset_read (veci* p, cla h ) { return h ? (satset*)(veci_begin(p) + h) : NULL; } +static inline cla satset_handle (veci* p, satset* c) { return (cla)((int *)c - veci_begin(p)); } +static inline int satset_check (veci* p, satset* c) { return (int*)c > veci_begin(p) && (int*)c < veci_begin(p) + veci_size(p); } +static inline int satset_size (int nLits) { return sizeof(satset)/4 + nLits; } +static inline void satset_print (satset * c) { + int i; + printf( "{ " ); + for ( i = 0; i < (int)c->nEnts; i++ ) + printf( "%d ", (c->pEnts[i] & 1)? -(c->pEnts[i] >> 1) : c->pEnts[i] >> 1 ); + printf( "}\n" ); +} + + +#define satset_foreach_entry( p, c, h, s ) \ + for ( h = s; (h < veci_size(p)) && (((c) = satset_read(p, h)), 1); h += satset_size(c->nEnts) ) + +//================================================================================================= +// Public APIs: + static inline int sat_solver2_nvars(sat_solver2* s) { return s->size; @@ -213,6 +245,8 @@ static inline int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom) return fNotUseRandomOld; } +extern void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pVars, veci * pRoots, int hRoot, veci * pGlobVars ); + ABC_NAMESPACE_HEADER_END #endif diff --git a/src/sat/bsat/satVec.h b/src/sat/bsat/satVec.h index 1f63ba1e..441ec974 100644 --- a/src/sat/bsat/satVec.h +++ b/src/sat/bsat/satVec.h @@ -29,15 +29,15 @@ ABC_NAMESPACE_HEADER_START // vector of 32-bit intergers (added for 64-bit portability) struct veci_t { - int size; int cap; + int size; int* ptr; }; typedef struct veci_t veci; static inline void veci_new (veci* v) { - v->size = 0; v->cap = 4; + v->size = 0; v->ptr = (int*)ABC_ALLOC( char, sizeof(int)*v->cap); } @@ -68,8 +68,8 @@ static inline void veci_remove(veci* v, int e) // vector of 32- or 64-bit pointers struct vecp_t { - int size; int cap; + int size; void** ptr; }; typedef struct vecp_t vecp; -- cgit v1.2.3