diff options
Diffstat (limited to 'src/sat/bsat')
-rw-r--r-- | src/sat/bsat/satClause.h | 115 | ||||
-rw-r--r-- | src/sat/bsat/satProof.c | 125 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.c | 14 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.h | 9 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.c | 609 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.h | 76 | ||||
-rw-r--r-- | src/sat/bsat/satUtil.c | 2 | ||||
-rw-r--r-- | src/sat/bsat/satVec.h | 3 |
8 files changed, 498 insertions, 455 deletions
diff --git a/src/sat/bsat/satClause.h b/src/sat/bsat/satClause.h index 8b1a1294..7769dc36 100644 --- a/src/sat/bsat/satClause.h +++ b/src/sat/bsat/satClause.h @@ -33,6 +33,11 @@ ABC_NAMESPACE_HEADER_START /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// +//#define LEARNT_MAX_START_DEFAULT 0 +#define LEARNT_MAX_START_DEFAULT 10000 +#define LEARNT_MAX_INCRE_DEFAULT 1000 +#define LEARNT_MAX_RATIO_DEFAULT 50 + //////////////////////////////////////////////////////////////////////// /// STRUCTURE DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -40,9 +45,6 @@ ABC_NAMESPACE_HEADER_START //================================================================================================= // Clause datatype + minor functions: -typedef int lit; -typedef int cla; - typedef struct clause_t clause; struct clause_t { @@ -90,14 +92,16 @@ static inline int Sat_MemIntSize( int size, int lrn ) { return (s static inline int Sat_MemClauseSize( clause * p ) { return Sat_MemIntSize(p->size, p->lrn); } //static inline clause * Sat_MemClause( Sat_Mem_t * p, int i, int k ) { assert(i <= p->iPage[i&1] && k <= Sat_MemLimit(p->pPages[i])); return (clause *)(p->pPages[i] + k ); } -static inline clause * Sat_MemClause( Sat_Mem_t * p, int i, int k ) { return (clause *)(p->pPages[i] + k); } +static inline clause * Sat_MemClause( Sat_Mem_t * p, int i, int k ) { assert( k ); return (clause *)(p->pPages[i] + k); } //static inline clause * Sat_MemClauseHand( Sat_Mem_t * p, cla h ) { assert(Sat_MemHandPage(p, h) <= p->iPage[(h & p->uLearnedMask) > 0]); assert(Sat_MemHandShift(p, h) >= 2 && Sat_MemHandShift(p, h) < (int)p->uLearnedMask); return Sat_MemClause( p, Sat_MemHandPage(p, h), Sat_MemHandShift(p, h) ); } -static inline clause * Sat_MemClauseHand( Sat_Mem_t * p, cla h ) { return Sat_MemClause( p, Sat_MemHandPage(p, h), Sat_MemHandShift(p, h) ); } +static inline clause * Sat_MemClauseHand( Sat_Mem_t * p, cla h ) { return h ? Sat_MemClause( p, Sat_MemHandPage(p, h), Sat_MemHandShift(p, h) ) : NULL; } static inline int Sat_MemEntryNum( Sat_Mem_t * p, int lrn ) { return p->nEntries[lrn]; } static inline cla Sat_MemHand( Sat_Mem_t * p, int i, int k ) { return (i << p->nPageSize) | k; } static inline cla Sat_MemHandCurrent( Sat_Mem_t * p, int lrn ) { return (p->iPage[lrn] << p->nPageSize) | Sat_MemLimit( p->pPages[p->iPage[lrn]] ); } +static inline int Sat_MemClauseUsed( Sat_Mem_t * p, cla h ) { return h < p->BookMarkH[(h & p->uLearnedMask) > 0]; } + static inline double Sat_MemMemoryHand( Sat_Mem_t * p, cla h ) { return 1.0 * ((Sat_MemHandPage(p, h) + 2)/2 * (1 << (p->nPageSize+2)) + Sat_MemHandShift(p, h) * 4); } static inline double Sat_MemMemoryUsed( Sat_Mem_t * p, int lrn ) { return Sat_MemMemoryHand( p, Sat_MemHandCurrent(p, lrn) ); } static inline double Sat_MemMemoryAllUsed( Sat_Mem_t * p ) { return Sat_MemMemoryUsed( p, 0 ) + Sat_MemMemoryUsed( p, 1 ); } @@ -108,9 +112,10 @@ static inline double Sat_MemMemoryAll( Sat_Mem_t * p ) { return 1. // i is page number // k is page offset -#define Sat_MemForEachClause( p, c, i, k ) \ - for ( i = 0; i <= p->iPage[0]; i += 2 ) \ - for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) ) +// this macro has to be fixed (Sat_MemClauseSize does not work for problem clauses in proof mode) +//#define Sat_MemForEachClause( p, c, i, k ) \ +// for ( i = 0; i <= p->iPage[0]; i += 2 ) \ +// for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) ) #define Sat_MemForEachLearned( p, c, i, k ) \ for ( i = 1; i <= p->iPage[1]; i += 2 ) \ @@ -130,7 +135,8 @@ static inline lit clause_read_lit( cla h ) { return (li static inline int clause_learnt_h( Sat_Mem_t * p, cla h ) { return (h & p->uLearnedMask) > 0; } static inline int clause_learnt( clause * c ) { return c->lrn; } -static inline int clause_id( clause * c ) { assert(c->lrn); return c->lits[c->size]; } +static inline int clause_id( clause * c ) { return c->lits[c->size]; } +static inline int clause_set_id( clause * c, int id ) { c->lits[c->size] = id; } static inline int clause_size( clause * c ) { return c->size; } static inline lit * clause_begin( clause * c ) { return c->lits; } static inline lit * clause_end( clause * c ) { return c->lits + c->size; } @@ -158,6 +164,26 @@ static inline void clause_print( clause * c ) SeeAlso [] ***********************************************************************/ +static inline int Sat_MemCountL( Sat_Mem_t * p ) +{ + clause * c; + int i, k, Count = 0; + Sat_MemForEachLearned( p, c, i, k ) + Count++; + return Count; +} + +/**Function************************************************************* + + Synopsis [Allocating vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ static inline void Sat_MemAlloc_( Sat_Mem_t * p, int nPageSize ) { assert( nPageSize > 8 && nPageSize < 32 ); @@ -216,10 +242,10 @@ static inline void Sat_MemRestart( Sat_Mem_t * p ) ***********************************************************************/ static inline void Sat_MemBookMark( Sat_Mem_t * p ) { - p->BookMarkH[0] = Sat_MemHandCurrent( p, 0 ); - p->BookMarkH[1] = Sat_MemHandCurrent( p, 1 ); p->BookMarkE[0] = p->nEntries[0]; p->BookMarkE[1] = p->nEntries[1]; + p->BookMarkH[0] = Sat_MemHandCurrent( p, 0 ); + p->BookMarkH[1] = Sat_MemHandCurrent( p, 1 ); } static inline void Sat_MemRollBack( Sat_Mem_t * p ) { @@ -227,8 +253,8 @@ static inline void Sat_MemRollBack( Sat_Mem_t * p ) p->nEntries[1] = p->BookMarkE[1]; p->iPage[0] = Sat_MemHandPage( p, p->BookMarkH[0] ); p->iPage[1] = Sat_MemHandPage( p, p->BookMarkH[1] ); - Sat_MemWriteLimit( p->pPages[0], Sat_MemHandShift( p, p->BookMarkH[0] ) ); - Sat_MemWriteLimit( p->pPages[1], Sat_MemHandShift( p, p->BookMarkH[1] ) ); + Sat_MemWriteLimit( p->pPages[p->iPage[0]], Sat_MemHandShift( p, p->BookMarkH[0] ) ); + Sat_MemWriteLimit( p->pPages[p->iPage[1]], Sat_MemHandShift( p, p->BookMarkH[1] ) ); } /**Function************************************************************* @@ -266,15 +292,15 @@ static inline void Sat_MemFree( Sat_Mem_t * p ) SeeAlso [] ***********************************************************************/ -static inline int Sat_MemAppend( Sat_Mem_t * p, int * pArray, int nSize, int lrn ) +static inline int Sat_MemAppend( Sat_Mem_t * p, int * pArray, int nSize, int lrn, int fPlus1 ) { clause * c; int * pPage = p->pPages[p->iPage[lrn]]; - int nInts = Sat_MemIntSize( nSize, lrn ); + int nInts = Sat_MemIntSize( nSize, lrn | fPlus1 ); assert( nInts + 3 < (1 << p->nPageSize) ); // need two extra at the begining of the page and one extra in the end - if ( Sat_MemLimit(pPage) + nInts >= (1 << p->nPageSize) ) - { + if ( Sat_MemLimit(pPage) + nInts + 2 >= (1 << p->nPageSize) ) + { p->iPage[lrn] += 2; if ( p->iPage[lrn] >= p->nPagesAlloc ) { @@ -293,8 +319,8 @@ static inline int Sat_MemAppend( Sat_Mem_t * p, int * pArray, int nSize, int lrn c->lrn = lrn; if ( pArray ) memcpy( c->lits, pArray, sizeof(int) * nSize ); - if ( lrn ) - c->lits[c->size] = p->nEntries[1]; + if ( lrn | fPlus1 ) + c->lits[c->size] = p->nEntries[lrn]; p->nEntries[lrn]++; Sat_MemIncLimit( pPage, nInts ); return Sat_MemHandCurrent(p, lrn) - nInts; @@ -333,15 +359,46 @@ static inline void Sat_MemShrink( Sat_Mem_t * p, int h, int lrn ) ***********************************************************************/ static inline int Sat_MemCompactLearned( Sat_Mem_t * p, int fDoMove ) { - clause * c; - int i, k, iNew = 1, kNew = 2, nInts, Counter = 0; + clause * c, * cPivot = NULL; + int i, k, iNew = 1, kNew = 2, nInts, fStartLooking, Counter = 0; + int hLimit = Sat_MemHandCurrent(p, 1); + if ( hLimit == Sat_MemHand(p, 1, 2) ) + return 0; + if ( fDoMove && p->BookMarkH[1] ) + { + // move the pivot + assert( p->BookMarkH[1] >= Sat_MemHand(p, 1, 2) && p->BookMarkH[1] <= hLimit ); + // get the pivot and remember it may be pointed offlimit + cPivot = Sat_MemClauseHand( p, p->BookMarkH[1] ); + if ( p->BookMarkH[1] < hLimit && !cPivot->mark ) + { + p->BookMarkH[1] = cPivot->lits[cPivot->size]; + cPivot = NULL; + } + // else find the next used clause after cPivot + } // iterate through the learned clauses + fStartLooking = 0; Sat_MemForEachLearned( p, c, i, k ) { assert( c->lrn ); // skip marked entry if ( c->mark ) + { + // if pivot is a marked clause, start looking for the next non-marked one + if ( cPivot && cPivot == c ) + { + fStartLooking = 1; + cPivot = NULL; + } continue; + } + // if we started looking before, we found it! + if ( fStartLooking ) + { + fStartLooking = 0; + p->BookMarkH[1] = c->lits[c->size]; + } // compute entry size nInts = Sat_MemClauseSize(c); assert( !(nInts & 1) ); @@ -380,12 +437,24 @@ static inline int Sat_MemCompactLearned( Sat_Mem_t * p, int fDoMove ) } if ( fDoMove ) { + // update the counter + p->nEntries[1] = Counter; // update the page count p->iPage[1] = iNew; // set the limit of the last page Sat_MemWriteLimit( p->pPages[iNew], kNew ); - // update the counter - p->nEntries[1] = Counter; + // check if the pivot need to be updated + if ( p->BookMarkH[1] ) + { + if ( cPivot ) + { + p->BookMarkH[1] = Sat_MemHandCurrent(p, 1); + p->BookMarkE[1] = p->nEntries[1]; + } + else + p->BookMarkE[1] = clause_id(Sat_MemClauseHand( p, p->BookMarkH[1] )); + } + } return Counter; } diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index eaadf71d..a669d2be 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -18,7 +18,11 @@ ***********************************************************************/ -#include "satSolver2.h" +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <assert.h> + #include "misc/vec/vec.h" #include "misc/vec/vecSet.h" #include "aig/aig/aig.h" @@ -26,7 +30,6 @@ ABC_NAMESPACE_IMPL_START - /* Proof is represented as a vector of records. A resolution record is represented by a handle (an offset in this vector). @@ -35,8 +38,6 @@ ABC_NAMESPACE_IMPL_START They are marked by bitshifting by 2 bits up and setting the LSB to 1 */ - -/* typedef struct satset_t satset; struct satset_t { @@ -45,21 +46,20 @@ struct satset_t unsigned partA : 1; unsigned nEnts : 29; int Id; - lit pEnts[0]; + int 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 /// //////////////////////////////////////////////////////////////////////// -static inline satset* Proof_ClauseRead ( Vec_Int_t* p, cla h ) { assert( h > 0 ); return satset_read( (veci *)p, h ); } -static inline satset* Proof_NodeRead ( Vec_Set_t* p, cla h ) { assert( h > 0 ); return (satset*)Vec_SetEntry( p, h ); } +//static inline satset* Proof_ClauseRead ( Vec_Int_t* p, int h ) { assert( h > 0 ); return satset_read( (veci *)p, h ); } +//static inline satset* Proof_ClauseRead ( Vec_Int_t* p, int h ) { assert( h > 0 ); return (satset *)Vec_IntEntryP( p, h );} +static inline satset* Proof_NodeRead ( Vec_Set_t* p, int h ) { assert( h > 0 ); return (satset*)Vec_SetEntry( p, h ); } static inline int Proof_NodeWordNum ( int nEnts ) { assert( nEnts > 0 ); return 1 + ((nEnts + 1) >> 1); } +void Proof_ClauseSetEnts( Vec_Set_t* p, int h, int nEnts ) { Proof_NodeRead(p, h)->nEnts = nEnts; } + // iterating through nodes in the proof #define Proof_ForeachClauseVec( pVec, p, pNode, i ) \ for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_ClauseRead(p, Vec_IntEntry(pVec,i))); i++ ) @@ -71,10 +71,10 @@ static inline int Proof_NodeWordNum ( int nEnts ) { assert( nE // iterating through fanins of a proof node #define Proof_NodeForeachFanin( pProof, pNode, pFanin, i ) \ for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = (pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(pProof, pNode->pEnts[i] >> 2)), 1); i++ ) -#define Proof_NodeForeachLeaf( pClauses, pNode, pLeaf, i ) \ - for ( i = 0; (i < (int)pNode->nEnts) && (((pLeaf) = (pNode->pEnts[i] & 1) ? Proof_ClauseRead(pClauses, pNode->pEnts[i] >> 2) : NULL), 1); i++ ) -#define Proof_NodeForeachFaninLeaf( pProof, pClauses, pNode, pFanin, i ) \ - for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_ClauseRead(pClauses, pNode->pEnts[i] >> 2) : Proof_NodeRead(pProof, 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_ClauseRead(pClauses, pNode->pEnts[i] >> 2) : NULL), 1); i++ ) +//#define Proof_NodeForeachFaninLeaf( pProof, pClauses, pNode, pFanin, i ) \ +// for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_ClauseRead(pClauses, pNode->pEnts[i] >> 2) : Proof_NodeRead(pProof, pNode->pEnts[i] >> 2)); i++ ) //////////////////////////////////////////////////////////////////////// @@ -252,6 +252,7 @@ int Proof_MarkUsedRec( Vec_Set_t * vProof, Vec_Int_t * vRoots ) SeeAlso [] ***********************************************************************/ +/* void Sat_ProofReduceCheck_rec( Vec_Set_t * vProof, Vec_Int_t * vClauses, satset * pNode, int hClausePivot, Vec_Ptr_t * vVisited ) { satset * pFanin; @@ -288,6 +289,7 @@ void Sat_ProofReduceCheck( sat_solver2 * s ) c->Id = 0; Vec_PtrFree( vVisited ); } +*/ /**Function************************************************************* @@ -300,6 +302,7 @@ void Sat_ProofReduceCheck( sat_solver2 * s ) SeeAlso [] ***********************************************************************/ +/* void Sat_ProofReduce2( sat_solver2 * s ) { Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs; @@ -361,20 +364,24 @@ void Sat_ProofReduce2( sat_solver2 * s ) Abc_PrintTime( 1, "Time", TimeTotal ); } Vec_SetShrink( vProof, Vec_SetHandCurrentS(vProof) ); - Sat_ProofReduceCheck( s ); +// Sat_ProofReduceCheck( s ); } +*/ + -void Sat_ProofReduce( sat_solver2 * s ) +int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot ) { - Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs; - Vec_Int_t * vRoots = (Vec_Int_t *)&s->claProofs; - Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses; +// Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs; +// Vec_Int_t * vRoots = (Vec_Int_t *)&s->claProofs; + Vec_Int_t * vRoots = (Vec_Int_t *)pRoots; +// Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses; int fVerbose = 0; Vec_Ptr_t * vUsed; satset * pNode, * pFanin, * pPivot; int i, j, k, hTemp, nSize; clock_t clk = clock(); static clock_t TimeTotal = 0; + int RetValue; // collect visited nodes nSize = Proof_MarkUsedRec( vProof, vRoots ); @@ -390,20 +397,20 @@ void Sat_ProofReduce( sat_solver2 * s ) pNode->Id = Vec_SetAppendS( vProof, 2 + pNode->nEnts ); Vec_PtrPush( vUsed, pNode ); // update fanins - Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k ) + Proof_NodeForeachFanin( vProof, pNode, pFanin, k ) if ( (pNode->pEnts[k] & 1) == 0 ) // proof node pNode->pEnts[k] = (pFanin->Id << 2) | (pNode->pEnts[k] & 2); - else // problem clause - assert( (int*)pFanin >= Vec_IntArray(vClauses) && (int*)pFanin < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) ); +// else // problem clause +// assert( (int*)pFanin >= Vec_IntArray(vClauses) && (int*)pFanin < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) ); } // update roots Proof_ForeachNodeVec1( vRoots, vProof, pNode, i ) Vec_IntWriteEntry( vRoots, i, pNode->Id ); // determine new pivot - assert( s->hProofPivot >= 1 && s->hProofPivot <= Vec_SetHandCurrent(vProof) ); - pPivot = Proof_NodeRead( vProof, s->hProofPivot ); - s->hProofPivot = Vec_SetHandCurrentS(vProof); - s->iProofPivot = Vec_PtrSize(vUsed); + assert( hProofPivot >= 1 && hProofPivot <= Vec_SetHandCurrent(vProof) ); + pPivot = Proof_NodeRead( vProof, hProofPivot ); + RetValue = Vec_SetHandCurrentS(vProof); +// s->iProofPivot = Vec_PtrSize(vUsed); // compact the nodes Vec_PtrForEachEntry( satset *, vUsed, pNode, i ) { @@ -411,8 +418,8 @@ void Sat_ProofReduce( sat_solver2 * s ) memmove( Vec_SetEntry(vProof, hTemp), pNode, sizeof(word)*Proof_NodeWordNum(pNode->nEnts) ); if ( pPivot && pPivot <= pNode ) { - s->hProofPivot = hTemp; - s->iProofPivot = i; + RetValue = hTemp; +// s->iProofPivot = i; pPivot = NULL; } } @@ -432,8 +439,10 @@ void Sat_ProofReduce( sat_solver2 * s ) Vec_SetShrink( vProof, Vec_SetHandCurrentS(vProof) ); Vec_SetShrinkLimits( vProof ); // Sat_ProofReduceCheck( s ); + return RetValue; } +#if 0 /**Function************************************************************* @@ -565,7 +574,7 @@ void Sat_ProofCheck( sat_solver2 * s ) Vec_SetFree( vResolves ); Vec_IntFree( vUsed ); } - +#endif /**Function************************************************************* @@ -578,33 +587,38 @@ void Sat_ProofCheck( sat_solver2 * s ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Set_t * vProof, Vec_Int_t * vUsed, int fUseIds ) +Vec_Int_t * Sat_ProofCollectCore( Vec_Set_t * vProof, Vec_Int_t * vUsed ) { Vec_Int_t * vCore; satset * pNode, * pFanin; - int i, k;//, clk = clock(); + unsigned * pBitMap; + int i, k, MaxCla = 0; + // find the largest number + Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) + Proof_NodeForeachFanin( vProof, pNode, pFanin, k ) + if ( pFanin == NULL ) + MaxCla = Abc_MaxInt( MaxCla, pNode->pEnts[k] >> 2 ); + // allocate bitmap + pBitMap = ABC_CALLOC( unsigned, Abc_BitWordNum(MaxCla) + 1 ); + // collect leaves vCore = Vec_IntAlloc( 1000 ); Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) - { - pNode->Id = 0; - Proof_NodeForeachLeaf( vClauses, pNode, pFanin, k ) - if ( pFanin && !pFanin->mark ) + Proof_NodeForeachFanin( vProof, pNode, pFanin, k ) + if ( pFanin == NULL ) { - pFanin->mark = 1; - Vec_IntPush( vCore, pNode->pEnts[k] >> 2 ); + int Entry = (pNode->pEnts[k] >> 2); + if ( Abc_InfoHasBit(pBitMap, Entry) ) + continue; + Abc_InfoSetBit(pBitMap, Entry); + Vec_IntPush( vCore, Entry ); } - } - // clean core clauses and reexpress core in terms of clause IDs - Proof_ForeachClauseVec( vCore, vClauses, pNode, i ) - { - assert( (int*)pNode < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) ); - pNode->mark = 0; - if ( fUseIds ) - Vec_IntWriteEntry( vCore, i, pNode->Id ); - } + ABC_FREE( pBitMap ); +// Vec_IntUniqify( vCore ); return vCore; } +#if 0 + /**Function************************************************************* Synopsis [Verifies that variables are labeled correctly.] @@ -687,7 +701,8 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ) // collect visited nodes vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 ); // collect core clauses (cleans vUsed and vCore) - vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 0 ); + vCore = Sat_ProofCollectCore( vProof, vUsed ); + // vCore arrived in terms of clause handles // map variables into their global numbers vVarMap = Vec_IntStartFull( s->size ); @@ -789,7 +804,8 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars ) // collect visited nodes vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 ); // collect core clauses (cleans vUsed and vCore) - vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 0 ); + vCore = Sat_ProofCollectCore( vProof, vUsed, 0 ); + // vCore arrived in terms of clause handles // map variables into their global numbers vVarMap = Vec_IntStartFull( s->size ); @@ -864,6 +880,8 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars ) return pRes; } +#endif + /**Function************************************************************* Synopsis [Computes UNSAT core.] @@ -875,19 +893,16 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars ) SeeAlso [] ***********************************************************************/ -void * Sat_ProofCore( sat_solver2 * s ) +void * Proof_DeriveCore( Vec_Set_t * vProof, int hRoot ) { - Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses; - Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs; - Vec_Int_t Roots = { 1, 1, &s->hProofLast }, * vRoots = &Roots; + Vec_Int_t Roots = { 1, 1, &hRoot }, * vRoots = &Roots; Vec_Int_t * vCore, * vUsed; - int hRoot = s->hProofLast; if ( hRoot == -1 ) return NULL; // collect visited clauses vUsed = Proof_CollectUsedIter( vProof, vRoots, 0 ); // collect core clauses - vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 1 ); + vCore = Sat_ProofCollectCore( vProof, vUsed ); Vec_IntFree( vUsed ); return vCore; } diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 2e3af2dd..5472e25d 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -29,11 +29,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA ABC_NAMESPACE_IMPL_START -//#define LEARNT_MAX_START_DEFAULT 0 -#define LEARNT_MAX_START_DEFAULT 20000 -#define LEARNT_MAX_INCRE_DEFAULT 1000 -#define LEARNT_MAX_RATIO_DEFAULT 50 - #define SAT_USE_ANALYZE_FINAL //================================================================================================= @@ -426,7 +421,7 @@ static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt) // create new clause // h = Vec_SetAppend( &s->Mem, NULL, size + learnt + 1 + 1 ) << 1; - h = Sat_MemAppend( &s->Mem, begin, size, learnt ); + h = Sat_MemAppend( &s->Mem, begin, size, learnt, 0 ); assert( !(h & 1) ); if ( s->hLearnts == -1 && learnt ) s->hLearnts = h; @@ -919,13 +914,12 @@ sat_solver* sat_solver_new(void) // Vec_SetAlloc_(&s->Mem, 15); Sat_MemAlloc_(&s->Mem, 14); s->hLearnts = -1; - s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0 ); + s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 ); s->binary = clause_read( s, s->hBinary ); s->nLearntStart = LEARNT_MAX_START_DEFAULT; // starting learned clause limit s->nLearntDelta = LEARNT_MAX_INCRE_DEFAULT; // delta of learned clause limit s->nLearntRatio = LEARNT_MAX_RATIO_DEFAULT; // ratio of learned clause limit - s->nLearntMax = s->nLearntStart; // initialize vectors @@ -1089,7 +1083,7 @@ void sat_solver_rollback( sat_solver* s ) int i; Sat_MemRestart( &s->Mem ); s->hLearnts = -1; - s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0 ); + s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 ); s->binary = clause_read( s, s->hBinary ); veci_resize(&s->act_clas, 0); @@ -1098,7 +1092,7 @@ void sat_solver_rollback( sat_solver* s ) for ( i = 0; i < s->size*2; i++ ) s->wlists[i].size = 0; - s->nLearntMax = s->nLearntStart; + s->nDBreduces = 0; // initialize other vars s->size = 0; diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 8998b78c..520e8284 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -28,8 +28,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <string.h> #include <assert.h> -#include "satClause.h" #include "satVec.h" +#include "satClause.h" #include "misc/vec/vecSet.h" ABC_NAMESPACE_HEADER_START @@ -98,6 +98,8 @@ struct sat_solver_t int hLearnts; // the first learnt clause int hBinary; // the special binary clause clause * binary; + veci* wlists; // watcher lists + veci act_clas; // contain clause activities // activities #ifdef USE_FLOAT_ACTIVITY @@ -112,7 +114,6 @@ struct sat_solver_t unsigned* activity; // A heuristic measurement of the activity of a variable. #endif - veci* wlists; // // varinfo * vi; // variable information int* levels; // char* assigns; // Current values of variables. @@ -141,13 +142,11 @@ struct sat_solver_t int fVerbose; stats_t stats; + int nLearntMax; // max number of learned clauses int nLearntStart; // starting learned clause limit int nLearntDelta; // delta of learned clause limit int nLearntRatio; // ratio percentage of learned clauses - int nLearntMax; // max number of learned clauses int nDBreduces; // number of DB reductions -// veci learned; // contain learnt clause handles - veci act_clas; // contain clause activities ABC_INT64_T nConfLimit; // external limit on the number of conflicts ABC_INT64_T nInsLimit; // external limit on the number of implications diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 58ea531c..0bca05ed 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -30,9 +30,11 @@ ABC_NAMESPACE_IMPL_START #define SAT_USE_PROOF_LOGGING +static int Time = 0; + //================================================================================================= // Debug: - + //#define VERBOSEDEBUG // For derivation output (verbosity level 2) @@ -136,28 +138,19 @@ static inline void solver2_clear_marks(sat_solver2* s) { //================================================================================================= // Clause datatype + minor functions: -static inline satset* clause2_read (sat_solver2* s, cla h) { return (h & 1) ? satset_read(&s->learnts, h>>1) : satset_read(&s->clauses, h>>1); } -static inline cla clause2_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 clause2_check (sat_solver2* s, satset* c) { return c->learnt ? satset_check(&s->learnts, c) : satset_check(&s->clauses, c); } -static inline int clause2_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 clause2_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) ? clause2_read(s, s->reasons[v] >> 1) : NULL; } +//static inline clause* var_unit_clause(sat_solver2* s, int v) { return (s->reasons[v]&1) ? clause2_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 clause2_read(s, s->units[v]); } +static inline clause* var_unit_clause(sat_solver2* s, int v) { return clause2_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++; } -//static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size); s->units[v] = i; s->nUnits++; } -// these two only work after creating a clause before the solver is called -int clause2_is_partA (sat_solver2* s, int h) { return clause2_read(s, h)->partA; } -void clause2_set_partA(sat_solver2* s, int h, int partA) { clause2_read(s, h)->partA = partA; } -int clause2_id(sat_solver2* s, int h) { return clause2_read(s, h)->Id; } +#define clause_foreach_var( p, var, i, start ) \ + for ( i = start; (i < (int)(p)->size) && ((var) = lit_var((p)->lits[i])); i++ ) //================================================================================================= // Simple helpers: @@ -168,7 +161,7 @@ static inline veci* solver2_wlist(sat_solver2* s, lit l) { return &s->wlists[l //================================================================================================= // Proof logging: -static inline void proof_chain_start( sat_solver2* s, satset* c ) +static inline void proof_chain_start( sat_solver2* s, clause* c ) { if ( s->fProofLogging ) { @@ -181,11 +174,11 @@ static inline void proof_chain_start( sat_solver2* s, satset* c ) } } -static inline void proof_chain_resolve( sat_solver2* s, satset* cls, int Var ) +static inline void proof_chain_resolve( sat_solver2* s, clause* cls, int Var ) { if ( s->fProofLogging ) { - satset* c = cls ? cls : var_unit_clause( s, Var ); + clause* c = cls ? cls : var_unit_clause( s, Var ); int ProofId = clause2_proofid(s, c, var_is_partA(s,Var)); assert( ProofId > 0 ); veci_push( &s->temp_proof, ProofId ); @@ -196,9 +189,9 @@ static inline int proof_chain_stop( sat_solver2* s ) { if ( s->fProofLogging ) { + extern void Proof_ClauseSetEnts( Vec_Set_t* p, int h, int nEnts ); int h = Vec_SetAppend( &s->Proofs, veci_begin(&s->temp_proof), veci_size(&s->temp_proof) ); - satset * c = (satset *)Vec_SetEntry( &s->Proofs, h ); - c->nEnts = veci_size(&s->temp_proof) - 2; + Proof_ClauseSetEnts( &s->Proofs, h, veci_size(&s->temp_proof) - 2 ); return h; } return 0; @@ -292,12 +285,12 @@ static inline void act_var_rescale(sat_solver2* s) { s->var_inc *= 1e-100; } static inline void act_clause2_rescale(sat_solver2* s) { - static int Total = 0; - float * claActs = (float *)veci_begin(&s->claActs); + static clock_t Total = 0; + float * act_clas = (float *)veci_begin(&s->act_clas); int i; clock_t clk = clock(); - for (i = 0; i < veci_size(&s->claActs); i++) - claActs[i] *= (float)1e-20; + for (i = 0; i < veci_size(&s->act_clas); i++) + act_clas[i] *= (float)1e-20; s->cla_inc *= (float)1e-20; Total += clock() - clk; @@ -311,11 +304,11 @@ static inline void act_var_bump(sat_solver2* s, int v) { if (s->orderpos[v] != -1) order_update(s,v); } -static inline void act_clause2_bump(sat_solver2* s, satset*c) { - float * claActs = (float *)veci_begin(&s->claActs); - assert( c->Id < veci_size(&s->claActs) ); - claActs[c->Id] += s->cla_inc; - if (claActs[c->Id] > (float)1e20) +static inline void act_clause2_bump(sat_solver2* s, clause*c) { + float * act_clas = (float *)veci_begin(&s->act_clas); + assert( c->Id < veci_size(&s->act_clas) ); + act_clas[c->Id] += s->cla_inc; + if (act_clas[c->Id] > (float)1e20) act_clause2_rescale(s); } static inline void act_var_decay(sat_solver2* s) { s->var_inc *= s->var_decay; } @@ -332,14 +325,14 @@ static inline void act_var_rescale(sat_solver2* s) { s->var_inc = Abc_MaxInt( s->var_inc, (1<<4) ); } static inline void act_clause2_rescale(sat_solver2* s) { -// static int Total = 0; - int i;//, clk = clock(); - unsigned * claActs = (unsigned *)veci_begin(&s->claActs); - for (i = 1; i < veci_size(&s->claActs); i++) - claActs[i] >>= 14; +// static clock_t Total = 0; +// clock_t clk = clock(); + int i; + unsigned * act_clas = (unsigned *)veci_begin(&s->act_clas); + for (i = 0; i < veci_size(&s->act_clas); i++) + act_clas[i] >>= 14; s->cla_inc >>= 14; s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) ); - // Total += clock() - clk; // Abc_Print(1, "Rescaling... Cla inc = %5d Conf = %10d ", s->cla_inc, s->stats.conflicts ); // Abc_PrintTime( 1, "Time", Total ); @@ -351,11 +344,12 @@ static inline void act_var_bump(sat_solver2* s, int v) { if (s->orderpos[v] != -1) order_update(s,v); } -static inline void act_clause2_bump(sat_solver2* s, satset*c) { - unsigned * claActs = (unsigned *)veci_begin(&s->claActs); - assert( c->Id > 0 && c->Id < veci_size(&s->claActs) ); - claActs[c->Id] += s->cla_inc; - if (claActs[c->Id] & 0x80000000) +static inline void act_clause2_bump(sat_solver2* s, clause*c) { + unsigned * act_clas = (unsigned *)veci_begin(&s->act_clas); + int Id = clause_id(c); + assert( Id >= 0 && Id < veci_size(&s->act_clas) ); + act_clas[Id] += s->cla_inc; + if (act_clas[Id] & 0x80000000) act_clause2_rescale(s); } static inline void act_var_decay(sat_solver2* s) { s->var_inc += (s->var_inc >> 4); } @@ -366,89 +360,61 @@ static inline void act_clause2_decay(sat_solver2* s) { s->cla_inc += (s->cla_inc //================================================================================================= // Clause functions: +static inline int sat_clause_compute_lbd( sat_solver2* s, clause* c ) +{ + int i, lev, minl = 0, lbd = 0; + for (i = 0; i < (int)c->size; i++) { + lev = var_level(s, lit_var(c->lits[i])); + if ( !(minl & (1 << (lev & 31))) ) { + minl |= 1 << (lev & 31); + lbd++; + } + } + return lbd; +} + static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proof_id) { - satset* c; - int i, Cid, nLits = end - begin; - assert(nLits < 1 || begin[0] >= 0); - assert(nLits < 2 || begin[1] >= 0); - assert(nLits < 1 || lit_var(begin[0]) < s->size); - assert(nLits < 2 || lit_var(begin[1]) < s->size); - // add memory if needed - - // assign clause ID - if ( learnt ) + clause* c; + int h, size = end - begin; + assert(size < 1 || begin[0] >= 0); + assert(size < 2 || begin[1] >= 0); + assert(size < 1 || lit_var(begin[0]) < s->size); + assert(size < 2 || lit_var(begin[1]) < s->size); + // create new clause + h = Sat_MemAppend( &s->Mem, begin, size, learnt, 1 ); + assert( !(h & 1) ); + c = clause2_read( s, h ); + if (learnt) { - if ( veci_size(&s->learnts) + satset_size(nLits) > s->learnts.cap ) - { - int nMemAlloc = s->learnts.cap ? 2 * s->learnts.cap : (1 << 20); - s->learnts.ptr = ABC_REALLOC( int, veci_begin(&s->learnts), nMemAlloc ); - // Abc_Print(1, "Reallocing from %d to %d...\n", s->learnts.cap, nMemAlloc ); - s->learnts.cap = nMemAlloc; - if ( veci_size(&s->learnts) == 0 ) - veci_push( &s->learnts, -1 ); - } - // create clause - c = (satset*)(veci_begin(&s->learnts) + veci_size(&s->learnts)); - ((int*)c)[0] = 0; - c->learnt = learnt; - c->nEnts = nLits; - for (i = 0; i < nLits; i++) - c->pEnts[i] = begin[i]; - // count the clause - s->stats.learnts++; - s->stats.learnts_literals += nLits; - c->Id = s->stats.learnts; - assert( c->Id == veci_size(&s->claActs) ); - veci_push(&s->claActs, 0); + if ( s->fProofLogging ) + assert( proof_id ); + c->lbd = sat_clause_compute_lbd( s, c ); + assert( clause_id(c) == veci_size(&s->act_clas) ); if ( proof_id ) veci_push(&s->claProofs, proof_id); - if ( nLits > 2 ) +// veci_push(&s->act_clas, (1<<10)); + veci_push(&s->act_clas, 0); + if ( size > 2 ) act_clause2_bump( s,c ); - // extend storage - Cid = (veci_size(&s->learnts) << 1) | 1; - s->learnts.size += satset_size(nLits); - assert( veci_size(&s->learnts) <= s->learnts.cap ); - assert(((ABC_PTRUINT_T)c & 3) == 0); -// Abc_Print(1, "Clause for proof %d: ", proof_id ); -// satset_print( c ); + s->stats.learnts++; + s->stats.learnts_literals += size; // remember the last one - s->hLearntLast = Cid; + s->hLearntLast = h; } else { - 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 ); - // Abc_Print(1, "Reallocing from %d to %d...\n", s->clauses.cap, nMemAlloc ); - s->clauses.cap = nMemAlloc; - if ( veci_size(&s->clauses) == 0 ) - veci_push( &s->clauses, -1 ); - } - // create clause - c = (satset*)(veci_begin(&s->clauses) + veci_size(&s->clauses)); - ((int*)c)[0] = 0; - c->learnt = learnt; - c->nEnts = nLits; - for (i = 0; i < nLits; i++) - c->pEnts[i] = begin[i]; - // count the clause + assert( clause_id(c) == (int)s->stats.clauses ); s->stats.clauses++; - s->stats.clauses_literals += nLits; - c->Id = s->stats.clauses; - // extend storage - Cid = (veci_size(&s->clauses) << 1); - s->clauses.size += satset_size(nLits); - assert( veci_size(&s->clauses) <= s->clauses.cap ); - assert(((ABC_PTRUINT_T)c & 3) == 0); + s->stats.clauses_literals += size; } // watch the clause - if ( nLits > 1 ){ - veci_push(solver2_wlist(s,lit_neg(begin[0])),Cid); - veci_push(solver2_wlist(s,lit_neg(begin[1])),Cid); + if ( size > 1 ) + { + veci_push(solver2_wlist(s,lit_neg(begin[0])),h); + veci_push(solver2_wlist(s,lit_neg(begin[1])),h); } - return Cid; + return h; } //================================================================================================= @@ -472,17 +438,6 @@ static inline int solver2_enqueue(sat_solver2* s, lit l, cla from) s->reasons[v] = from; // = from << 1; s->trail[s->qtail++] = l; order_assigned(s, v); -/* - if ( solver2_dlevel(s) == 0 ) - { - satset * c = from ? clause2_read( s, from ) : NULL; - Abc_Print(1, "Enqueing var %d on level %d with reason clause ", v, solver2_dlevel(s) ); - if ( c ) - satset_print( c ); - else - Abc_Print(1, "<none>\n" ); - } -*/ return true; } } @@ -589,7 +544,7 @@ static double solver2_progress(sat_solver2* s) | stores the result in 'out_conflict'. |________________________________________________________________________________________________@*/ /* -void Solver::analyzeFinal(satset* confl, bool skip_first) +void Solver::analyzeFinal(clause* confl, bool skip_first) { // -- NOTE! This code is relatively untested. Please report bugs! conflict.clear(); @@ -628,7 +583,7 @@ void Solver::analyzeFinal(satset* confl, bool skip_first) } */ -static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first) +static int solver2_analyze_final(sat_solver2* s, clause* conf, int skip_first) { int i, j, x;//, start; veci_resize(&s->conf_final,0); @@ -636,7 +591,7 @@ static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first) return s->hProofLast; proof_chain_start( s, conf ); assert( veci_size(&s->tagged) == 0 ); - satset_foreach_var( conf, x, i, skip_first ){ + clause_foreach_var( conf, x, i, skip_first ){ if ( var_level(s,x) ) var_set_tag(s, x, 1); else @@ -647,10 +602,10 @@ 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 = clause2_read(s, var_reason(s,x)); + clause* c = clause2_read(s, var_reason(s,x)); if (c){ proof_chain_resolve( s, c, x ); - satset_foreach_var( c, x, j, 1 ){ + clause_foreach_var( c, x, j, 1 ){ if ( var_level(s,x) ) var_set_tag(s, x, 1); else @@ -672,7 +627,7 @@ static int solver2_lit_removable_rec(sat_solver2* s, int v) // tag[1]: Processed by this procedure // tag[2]: 0=non-removable, 1=removable - satset* c; + clause* c; int i, x; // skip visited @@ -686,7 +641,7 @@ static int solver2_lit_removable_rec(sat_solver2* s, int v) return 0; } - satset_foreach_var( c, x, i, 1 ){ + clause_foreach_var( c, x, i, 1 ){ if (var_tag(s,x) & 1) solver2_lit_removable_rec(s, x); else{ @@ -706,7 +661,7 @@ static int solver2_lit_removable_rec(sat_solver2* s, int v) static int solver2_lit_removable(sat_solver2* s, int x) { - satset* c; + clause* c; int i, top; if ( !var_reason(s,x) ) return 0; @@ -731,7 +686,7 @@ static int solver2_lit_removable(sat_solver2* s, int x) } x >>= 1; c = clause2_read(s, var_reason(s,x)); - satset_foreach_var( c, x, i, 1 ){ + clause_foreach_var( c, x, i, 1 ){ if (var_tag(s,x) || !var_level(s,x)) continue; if (!var_reason(s,x) || !var_lev_mark(s,x)){ @@ -747,7 +702,7 @@ static int solver2_lit_removable(sat_solver2* s, int x) static void solver2_logging_order(sat_solver2* s, int x) { - satset* c; + clause* c; int i; if ( (var_tag(s,x) & 4) ) return; @@ -766,7 +721,7 @@ static void solver2_logging_order(sat_solver2* s, int x) c = clause2_read(s, var_reason(s,x)); // if ( !c ) // Abc_Print(1, "solver2_logging_order(): Error in conflict analysis!!!\n" ); - satset_foreach_var( c, x, i, 1 ){ + clause_foreach_var( c, x, i, 1 ){ if ( !var_level(s,x) || (var_tag(s,x) & 1) ) continue; veci_push(&s->stack, x << 1); @@ -777,19 +732,19 @@ static void solver2_logging_order(sat_solver2* s, int x) static void solver2_logging_order_rec(sat_solver2* s, int x) { - satset* c; + clause* c; int i, y; if ( (var_tag(s,x) & 8) ) return; c = clause2_read(s, var_reason(s,x)); - satset_foreach_var( c, y, i, 1 ) + clause_foreach_var( c, y, i, 1 ) 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) +static int solver2_analyze(sat_solver2* s, clause* c, veci* learnt) { int cnt = 0; lit p = 0; @@ -805,9 +760,9 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt) veci_push(learnt,lit_Undef); while ( 1 ){ assert(c != 0); - if (c->learnt) + if (c->lrn) act_clause2_bump(s,c); - satset_foreach_var( c, x, j, (int)(p > 0) ){ + clause_foreach_var( c, x, j, (int)(p > 0) ){ assert(x >= 0 && x < s->size); if ( var_tag(s, x) ) continue; @@ -821,7 +776,7 @@ 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->pEnts[j]); + veci_push(learnt,c->lits[j]); } while (!var_tag(s, lit_var(s->trail[ind--]))); @@ -864,7 +819,7 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt) for (i = veci_size(&s->min_step_order); i > 0; ) { i--; c = clause2_read(s, var_reason(s,vars[i])); proof_chain_resolve( s, c, vars[i] ); - satset_foreach_var(c, x, k, 1) + clause_foreach_var(c, x, k, 1) if ( var_level(s,x) == 0 ) proof_chain_resolve( s, NULL, x ); } @@ -913,9 +868,9 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt) return proof_id; } -satset* solver2_propagate(sat_solver2* s) +clause* solver2_propagate(sat_solver2* s) { - satset* c, * confl = NULL; + clause* c, * confl = NULL; veci* ws; lit* lits, false_lit, p, * stop, * k; cla* begin,* end, *i, *j; @@ -931,7 +886,7 @@ satset* solver2_propagate(sat_solver2* s) s->stats.propagations++; for (i = j = begin; i < end; ){ c = clause2_read(s,*i); - lits = c->pEnts; + lits = c->lits; // Make sure the false literal is data[1]: false_lit = lit_neg(p); @@ -946,7 +901,7 @@ satset* solver2_propagate(sat_solver2* s) *j++ = *i; else{ // Look for new watch: - stop = lits + c->nEnts; + stop = lits + c->size; for (k = lits + 2; k < stop; k++){ if (var_value(s, lit_var(*k)) != !lit_sign(*k)){ lits[1] = *k; @@ -962,7 +917,7 @@ satset* solver2_propagate(sat_solver2* s) int fLitIsFalse = (var_value(s, Var) == !lit_sign(Lit)); // Log production of top-level unit clause: proof_chain_start( s, c ); - satset_foreach_var( c, x, k, 1 ){ + clause_foreach_var( c, x, k, 1 ){ assert( var_level(s, x) == 0 ); proof_chain_resolve( s, NULL, x ); } @@ -986,6 +941,8 @@ satset* solver2_propagate(sat_solver2* s) *j++ = *i; // Clause is unit under assignment: + if ( c->lrn ) + c->lbd = sat_clause_compute_lbd(s, c); if (!solver2_enqueue(s,Lit, *i)){ confl = clause2_read(s,*i++); // Copy the remaining watches: @@ -1024,7 +981,7 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts) veci_new(&learnt_clause); for (;;){ - satset* confl = solver2_propagate(s); + clause* confl = solver2_propagate(s); if (confl != 0){ // CONFLICT int blevel; @@ -1138,9 +1095,13 @@ sat_solver2* sat_solver2_new(void) #endif s->fSkipSimplify = 1; s->fNotUseRandom = 0; - s->nLearntMax = 0; s->fVerbose = 0; + s->nLearntStart = LEARNT_MAX_START_DEFAULT; // starting learned clause limit + s->nLearntDelta = LEARNT_MAX_INCRE_DEFAULT; // delta of learned clause limit + s->nLearntRatio = LEARNT_MAX_RATIO_DEFAULT; // ratio of learned clause limit + s->nLearntMax = s->nLearntStart; + // initialize vectors veci_new(&s->order); veci_new(&s->trail_lim); @@ -1152,32 +1113,20 @@ 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->learnt_live); - veci_new(&s->claActs); veci_push(&s->claActs, -1); - veci_new(&s->claProofs); veci_push(&s->claProofs, -1); +// veci_new(&s->learnt_live); + + Sat_MemAlloc_( &s->Mem, 14 ); + veci_new(&s->act_clas); + veci_new(&s->claProofs); if ( s->fProofLogging ) Vec_SetAlloc_( &s->Proofs, 20 ); - // prealloc clause - assert( !s->clauses.ptr ); - s->clauses.cap = (1 << 20); - s->clauses.ptr = ABC_ALLOC( int, s->clauses.cap ); - veci_push(&s->clauses, -1); - // prealloc learnt - assert( !s->learnts.ptr ); - s->learnts.cap = (1 << 20); - s->learnts.ptr = ABC_ALLOC( int, s->learnts.cap ); - veci_push(&s->learnts, -1); - // initialize clause pointers s->hLearntLast = -1; // the last learnt clause s->hProofLast = -1; // the last proof ID // initialize rollback s->iVarPivot = 0; // the pivot for variables s->iTrailPivot = 0; // the pivot for trail - s->iProofPivot = 0; // the pivot for proof records - s->hClausePivot = 1; // the pivot for problem clause - s->hLearntPivot = 1; // the pivot for learned clause s->hProofPivot = 1; // the pivot for proof records return s; } @@ -1243,11 +1192,11 @@ void sat_solver2_delete(sat_solver2* s) if ( fVerify ) { veci * pCore = (veci *)Sat_ProofCore( s ); - Abc_Print(1, "UNSAT core contains %d clauses (%6.2f %%).\n", veci_size(pCore), 100.0*veci_size(pCore)/veci_size(&s->clauses) ); +// Abc_Print(1, "UNSAT core contains %d clauses (%6.2f %%).\n", veci_size(pCore), 100.0*veci_size(pCore)/veci_size(&s->clauses) ); veci_delete( pCore ); ABC_FREE( pCore ); - if ( s->fProofLogging ) - Sat_ProofCheck( s ); +// if ( s->fProofLogging ) +// Sat_ProofCheck( s ); } // report statistics @@ -1264,11 +1213,12 @@ 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->learnt_live); - veci_delete(&s->claActs); +// veci_delete(&s->learnt_live); + veci_delete(&s->act_clas); veci_delete(&s->claProofs); - veci_delete(&s->clauses); - veci_delete(&s->learnts); +// veci_delete(&s->clauses); +// veci_delete(&s->lrns); + Sat_MemFree_( &s->Mem ); // veci_delete(&s->proofs); Vec_SetFree_( &s->Proofs ); @@ -1290,6 +1240,8 @@ void sat_solver2_delete(sat_solver2* s) ABC_FREE(s->model ); } ABC_FREE(s); + +// Abc_PrintTime( 1, "Time", Time ); } @@ -1358,9 +1310,9 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end) { // Log production of top-level unit clause: int x, k, proof_id, CidNew; - satset* c = clause2_read(s, Cid); + clause* c = clause2_read(s, Cid); proof_chain_start( s, c ); - satset_foreach_var( c, x, k, 1 ) + clause_foreach_var( c, x, k, 1 ) proof_chain_resolve( s, NULL, x ); proof_id = proof_chain_stop( s ); // generate a new clause @@ -1400,127 +1352,178 @@ void luby2_test() void sat_solver2_reducedb(sat_solver2* s) { static clock_t TimeTotal = 0; - satset * c, * pivot; - cla h,* pArray,* pArray2; - int * pPerm, * pClaAct, nClaAct, ActCutOff; - int i, j, k, hTemp, hHandle, LastSize = 0; + Sat_Mem_t * pMem = &s->Mem; + clause * c; + int nLearnedOld = veci_size(&s->act_clas); + int * act_clas = veci_begin(&s->act_clas); + int * pPerm, * pSortValues, nCutoffValue, * pClaProofs; + int i, j, k, Id, nSelected, LastSize = 0; int Counter, CounterStart; clock_t clk = clock(); + static int Count = 0; + Count++; + assert( s->nLearntMax ); + s->nDBreduces++; +// printf( "Calling reduceDB with %d clause limit and parameters (%d %d %d).\n", s->nLearntMax, s->nLearntStart, s->nLearntDelta, s->nLearntRatio ); - // check if it is time to reduce - if ( s->nLearntMax == 0 || s->stats.learnts < (unsigned)s->nLearntMax ) - return; +/* + // find the new limit s->nLearntMax = s->nLearntMax * 11 / 10; - // preserve 1/10 of last clauses CounterStart = s->stats.learnts - (s->nLearntMax / 10); - // preserve 1/10 of most active clauses - pClaAct = veci_begin(&s->claActs) + 1; - nClaAct = veci_size(&s->claActs) - 1; - pPerm = Abc_MergeSortCost( pClaAct, nClaAct ); - assert( pClaAct[pPerm[0]] <= pClaAct[pPerm[nClaAct-1]] ); - ActCutOff = pClaAct[pPerm[nClaAct*9/10]]; + pSortValues = veci_begin(&s->act_clas); + pPerm = Abc_MergeSortCost( pSortValues, nLearnedOld ); + assert( pSortValues[pPerm[0]] <= pSortValues[pPerm[nLearnedOld-1]] ); + nCutoffValue = pSortValues[pPerm[nLearnedOld*9/10]]; + ABC_FREE( pPerm ); +// nCutoffValue = ABC_INFINITY; +*/ + + + // find the new limit + s->nLearntMax = s->nLearntStart + s->nLearntDelta * s->nDBreduces; + // preserve 1/20 of last clauses + CounterStart = nLearnedOld - (s->nLearntMax / 20); + // preserve 3/4 of most active clauses + nSelected = nLearnedOld*s->nLearntRatio/100; + // create sorting values + pSortValues = ABC_ALLOC( int, nLearnedOld ); + Sat_MemForEachLearned( pMem, c, i, k ) + { + Id = clause_id(c); + pSortValues[Id] = (((7 - Abc_MinInt(c->lbd, 7)) << 28) | (act_clas[Id] >> 4)); +// pSortValues[Id] = act_clas[Id]; + assert( pSortValues[Id] >= 0 ); + } + // find non-decreasing permutation + pPerm = Abc_MergeSortCost( pSortValues, nLearnedOld ); + assert( pSortValues[pPerm[0]] <= pSortValues[pPerm[nLearnedOld-1]] ); + nCutoffValue = pSortValues[pPerm[nLearnedOld-nSelected]]; ABC_FREE( pPerm ); -// ActCutOff = ABC_INFINITY; +// nCutoffValue = ABC_INFINITY; - // mark learned clauses to remove - Counter = 0; - veci_resize( &s->learnt_live, 0 ); - sat_solver_foreach_learnt( s, c, h ) + // count how many clauses satisfy the condition + Counter = j = 0; + Sat_MemForEachLearned( pMem, c, i, k ) { - if ( Counter++ > CounterStart || c->nEnts < 3 || pClaAct[c->Id-1] >= ActCutOff || s->reasons[lit_var(c->pEnts[0])] == (h<<1)+1 ) - veci_push( &s->learnt_live, h ); + assert( c->mark == 0 ); + if ( Counter++ > CounterStart || clause_size(c) < 2 || pSortValues[clause_id(c)] >= nCutoffValue || s->reasons[lit_var(c->lits[0])] == Sat_MemHand(pMem, i, k) ) + { + } else - c->mark = 1; + j++; + if ( j >= nLearnedOld / 6 ) + break; } - // report the results - if ( s->fVerbose ) - Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%) ", - veci_size(&s->learnt_live), s->stats.learnts, 100.0 * veci_size(&s->learnt_live) / s->stats.learnts ); - - // remap clause proofs and clauses - hHandle = 1; - pArray = s->fProofLogging ? veci_begin(&s->claProofs) : NULL; - pArray2 = veci_begin(&s->claActs); - satset_foreach_entry_vec( &s->learnt_live, &s->learnts, c, i ) + if ( j < nLearnedOld / 6 ) + return; + + // mark learned clauses to remove + Counter = j = 0; + pClaProofs = s->fProofLogging ? veci_begin(&s->claProofs) : NULL; + Sat_MemForEachLearned( pMem, c, i, k ) { - if ( pArray ) - pArray[i+1] = pArray[c->Id]; - pArray2[i+1] = pArray2[c->Id]; - c->Id = hHandle; hHandle += satset_size(c->nEnts); + assert( c->mark == 0 ); + if ( Counter++ > CounterStart || clause_size(c) < 2 || pSortValues[clause_id(c)] >= nCutoffValue || s->reasons[lit_var(c->lits[0])] == Sat_MemHand(pMem, i, k) ) + { + pSortValues[j] = pSortValues[clause_id(c)]; + if ( pClaProofs ) + pClaProofs[j] = pClaProofs[clause_id(c)]; + j++; + } + else // delete + { + c->mark = 1; + s->stats.learnts_literals -= clause_size(c); + s->stats.learnts--; + } } +// if ( j == nLearnedOld ) +// return; + + assert( s->stats.learnts == (unsigned)j ); + assert( Counter == nLearnedOld ); + veci_resize(&s->act_clas,j); if ( s->fProofLogging ) - veci_resize(&s->claProofs,veci_size(&s->learnt_live)+1); - veci_resize(&s->claActs,veci_size(&s->learnt_live)+1); + veci_resize(&s->claProofs,j); + + // update ID of each clause to be its new handle + Counter = Sat_MemCompactLearned( pMem, 0 ); + assert( Counter == (int)s->stats.learnts ); - // update reason clauses + // update reasons for ( i = 0; i < s->size; i++ ) - if ( s->reasons[i] && (s->reasons[i] & 1) ) - { - c = clause2_read( s, s->reasons[i] ); - assert( c->mark == 0 ); - s->reasons[i] = (c->Id << 1) | 1; - } + { + if ( !s->reasons[i] ) // no reason + continue; + if ( clause_is_lit(s->reasons[i]) ) // 2-lit clause + continue; + if ( !clause_learnt_h(pMem, s->reasons[i]) ) // problem clause + continue; + c = clause2_read( s, s->reasons[i] ); + assert( c->mark == 0 ); + s->reasons[i] = clause_id(c); // updating handle here!!! + } - // compact watches + // update watches for ( i = 0; i < s->size*2; i++ ) { - pArray = veci_begin(&s->wlists[i]); + int * pArray = veci_begin(&s->wlists[i]); for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ ) - if ( !(pArray[k] & 1) ) // problem clause + { + if ( clause_is_lit(pArray[k]) ) // 2-lit clause pArray[j++] = pArray[k]; - else if ( !(c = clause2_read(s, pArray[k]))->mark ) // useful learned clause - pArray[j++] = (c->Id << 1) | 1; + else if ( !clause_learnt_h(pMem, pArray[k]) ) // problem clause + pArray[j++] = pArray[k]; + else + { + c = clause2_read(s, pArray[k]); + if ( !c->mark ) // useful learned clause + pArray[j++] = clause_id(c); // updating handle here!!! + } + } veci_resize(&s->wlists[i],j); } + // compact units if ( s->fProofLogging ) - for ( i = 0; i < s->size; i++ ) - if ( s->units[i] && (s->units[i] & 1) ) - { - c = clause2_read( s, s->units[i] ); - assert( c->mark == 0 ); - s->units[i] = (c->Id << 1) | 1; - } - // compact clauses - pivot = satset_read( &s->learnts, s->hLearntPivot ); - s->hLearntPivot = hTemp = hHandle; - satset_foreach_entry_vec( &s->learnt_live, &s->learnts, c, i ) - { - hTemp = c->Id; c->Id = i + 1; - LastSize = satset_size(c->nEnts); - memmove( veci_begin(&s->learnts) + hTemp, c, sizeof(int)*LastSize ); - if ( pivot && pivot <= c ) - { - s->hLearntPivot = hTemp; - pivot = NULL; - } - } - assert( hHandle == hTemp + LastSize ); - veci_resize(&s->learnts,hHandle); - s->stats.learnts = veci_size(&s->learnt_live); - assert( s->hLearntPivot <= veci_size(&s->learnts) ); - assert( s->hClausePivot <= veci_size(&s->clauses) ); + for ( i = 0; i < s->size; i++ ) + if ( s->units[i] && clause_learnt_h(pMem, s->units[i]) ) + { + c = clause2_read( s, s->units[i] ); + assert( c->mark == 0 ); + s->units[i] = clause_id(c); + } + + // perform final move of the clauses + Counter = Sat_MemCompactLearned( pMem, 1 ); + assert( Counter == (int)s->stats.learnts ); // compact proof (compacts 'proofs' and update 'claProofs') if ( s->fProofLogging ) - Sat_ProofReduce( s ); + s->hProofPivot = Sat_ProofReduce( &s->Proofs, &s->claProofs, s->hProofPivot ); + + // report the results TimeTotal += clock() - clk; if ( s->fVerbose ) - Abc_PrintTime( 1, "Time", TimeTotal ); + { + Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%) ", + s->stats.learnts, nLearnedOld, 100.0 * s->stats.learnts / nLearnedOld ); + Abc_PrintTime( 1, "Time", TimeTotal ); + } } // reverses to the previously bookmarked point void sat_solver2_rollback( sat_solver2* s ) { + Sat_Mem_t * pMem = &s->Mem; int i, k, j; + static int Count = 0; + Count++; assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size ); assert( s->iTrailPivot >= 0 && s->iTrailPivot <= s->qtail ); - assert( s->iProofPivot >= 0 && s->iProofPivot <= Vec_SetEntryNum(&s->Proofs) ); - assert( s->hClausePivot >= 1 && s->hClausePivot <= veci_size(&s->clauses) ); - assert( s->hLearntPivot >= 1 && s->hLearntPivot <= veci_size(&s->learnts) ); assert( s->hProofPivot >= 1 && s->hProofPivot <= Vec_SetHandCurrent(&s->Proofs) ); // reset implication queue solver2_canceluntil_rollback( s, s->iTrailPivot ); @@ -1538,42 +1541,32 @@ void sat_solver2_rollback( sat_solver2* s ) } } // compact watches - if ( s->hClausePivot > 1 || s->hLearntPivot > 1 ) - { - for ( i = 0; i < s->size*2; i++ ) - { - cla* pArray = veci_begin(&s->wlists[i]); - for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ ) - if ( clause2_is_used(s, pArray[k]) ) - pArray[j++] = pArray[k]; - veci_resize(&s->wlists[i],j); - } - } - // reset problem clauses - if ( s->hClausePivot < veci_size(&s->clauses) ) + for ( i = 0; i < s->iVarPivot*2; i++ ) { - satset* first = satset_read(&s->clauses, s->hClausePivot); - s->stats.clauses = first->Id-1; - veci_resize(&s->clauses, s->hClausePivot); - } - // resetn learned clauses - if ( s->hLearntPivot < veci_size(&s->learnts) ) - { - satset* first = satset_read(&s->learnts, s->hLearntPivot); - veci_resize(&s->claActs, first->Id); - if ( s->fProofLogging ) { - veci_resize(&s->claProofs, first->Id); -// Vec_SetWriteEntryNum(&s->Proofs, s->iProofPivot); // <- some bug here -// Vec_SetShrink(&s->Proofs, s->hProofPivot); - Sat_ProofReduce( s ); - } - s->stats.learnts = first->Id-1; - veci_resize(&s->learnts, s->hLearntPivot); + cla* pArray = veci_begin(&s->wlists[i]); + for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ ) + if ( Sat_MemClauseUsed(pMem, pArray[k]) ) + pArray[j++] = pArray[k]; + veci_resize(&s->wlists[i],j); } // reset watcher lists for ( i = 2*s->iVarPivot; i < 2*s->size; i++ ) s->wlists[i].size = 0; + // reset clause counts + s->stats.clauses = pMem->BookMarkE[0]; + s->stats.learnts = pMem->BookMarkE[1]; + // rollback clauses + Sat_MemRollBack( pMem ); + + // resize learned arrays + veci_resize(&s->act_clas, s->stats.learnts); + if ( s->fProofLogging ) + { + veci_resize(&s->claProofs, s->stats.learnts); + Vec_SetShrink(&s->Proofs, s->hProofPivot); // past bug here +// Sat_ProofReduce( &s->Proofs, &s->claProofs, s->hProofPivot ); + } // initialize other vars s->size = s->iVarPivot; @@ -1614,9 +1607,6 @@ void sat_solver2_rollback( sat_solver2* s ) // initialize rollback s->iVarPivot = 0; // the pivot for variables s->iTrailPivot = 0; // the pivot for trail - s->iProofPivot = 0; // the pivot for proof records - s->hClausePivot = 1; // the pivot for problem clause - s->hLearntPivot = 1; // the pivot for learned clause s->hProofPivot = 1; // the pivot for proof records } } @@ -1630,9 +1620,7 @@ double sat_solver2_memory( sat_solver2* s, int fAll ) for (i = 0; i < s->cap*2; i++) Mem += s->wlists[i].cap * sizeof(int); Mem += s->cap * sizeof(veci); // ABC_FREE(s->wlists ); - Mem += s->clauses.cap * sizeof(int); - Mem += s->learnts.cap * sizeof(int); - Mem += s->claActs.cap * sizeof(int); + Mem += s->act_clas.cap * sizeof(int); Mem += s->claProofs.cap * sizeof(int); // Mem += s->cap * sizeof(char); // ABC_FREE(s->polarity ); // Mem += s->cap * sizeof(char); // ABC_FREE(s->tags ); @@ -1651,7 +1639,6 @@ double sat_solver2_memory( sat_solver2* s, int fAll ) Mem += s->cap * sizeof(int); // ABC_FREE(s->reasons ); Mem += s->cap * sizeof(int); // ABC_FREE(s->units ); Mem += s->cap * sizeof(int); // ABC_FREE(s->model ); - Mem += s->tagged.cap * sizeof(int); Mem += s->stack.cap * sizeof(int); Mem += s->order.cap * sizeof(int); @@ -1661,9 +1648,9 @@ double sat_solver2_memory( sat_solver2* s, int fAll ) Mem += s->mark_levels.cap * sizeof(int); Mem += s->min_lit_order.cap * sizeof(int); Mem += s->min_step_order.cap * sizeof(int); - Mem += s->learnt_live.cap * sizeof(int); Mem += s->temp_proof.cap * sizeof(int); -// Mem += Vec_ReportMemory( &s->Mem ); + Mem += Sat_MemMemoryAll( &s->Mem ); +// Mem += Vec_ReportMemory( &s->Proofs ); return Mem; } double sat_solver2_memory_proof( sat_solver2* s ) @@ -1673,6 +1660,7 @@ double sat_solver2_memory_proof( sat_solver2* s ) // find the clause in the watcher lists +/* int sat_solver2_find_clause( sat_solver2* s, int Hand, int fVerbose ) { int i, k, Found = 0; @@ -1697,25 +1685,26 @@ int sat_solver2_find_clause( sat_solver2* s, int Hand, int fVerbose ) } return Found; } - +*/ +/* // verify that all problem clauses are satisfied void sat_solver2_verify( sat_solver2* s ) { - satset * c; + clause * c; int i, k, v, Counter = 0; - satset_foreach_entry( &s->clauses, c, i, 1 ) + clause_foreach_entry( &s->clauses, c, i, 1 ) { - for ( k = 0; k < (int)c->nEnts; k++ ) + for ( k = 0; k < (int)c->size; k++ ) { - v = lit_var(c->pEnts[k]); - if ( sat_solver2_var_value(s, v) ^ lit_sign(c->pEnts[k]) ) + v = lit_var(c->lits[k]); + if ( sat_solver2_var_value(s, v) ^ lit_sign(c->lits[k]) ) break; } - if ( k == (int)c->nEnts ) + if ( k == (int)c->size ) { Abc_Print(1, "Clause %d is not satisfied. ", c->Id ); - satset_print( c ); - sat_solver2_find_clause( s, satset_handle(&s->clauses, c), 1 ); + clause_print( c ); + sat_solver2_find_clause( s, clause_handle(&s->clauses, c), 1 ); Counter++; } } @@ -1724,7 +1713,7 @@ void sat_solver2_verify( sat_solver2* s ) // else // Abc_Print(1, "Verification passed.\n" ); } - +*/ 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) { @@ -1761,7 +1750,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim if (!solver2_assume(p)){ GClause r = reason[var(p)]; if (r != Gclause2_NULL){ - satset* confl; + clause* confl; if (r.isLit()){ confl = propagate_tmpbin; (*confl)[1] = ~p; @@ -1775,7 +1764,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim conflict.push(~p); cancelUntil(0); return false; } - satset* confl = propagate(); + clause* confl = propagate(); if (confl != NULL){ analyzeFinal(confl), assert(conflict.size() > 0); cancelUntil(0); @@ -1793,10 +1782,10 @@ 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 = clause2_read(s, lit_reason(s,p)); + clause* r = clause2_read(s, lit_reason(s,p)); if (r != NULL) { - satset* confl = r; + clause* confl = r; proof_id = solver2_analyze_final(s, confl, 1); veci_push(&s->conf_final, lit_neg(p)); } @@ -1816,7 +1805,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim } else { - satset* confl = solver2_propagate(s); + clause* confl = solver2_propagate(s); if (confl != NULL){ proof_id = solver2_analyze_final(s, confl, 0); assert(s->conf_final.size > 0); @@ -1851,8 +1840,9 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim } if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit ) break; - // reduce the set of learnt clauses: - sat_solver2_reducedb(s); + // reduce the set of learnt clauses + if ( s->nLearntMax && veci_size(&s->act_clas) >= s->nLearntMax ) + sat_solver2_reducedb(s); // perform next run nof_conflicts = (ABC_INT64_T)( 100 * luby2(2, restart_iter++) ); status = solver2_search(s, nof_conflicts); @@ -1872,5 +1862,10 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim return status; } +void * Sat_ProofCore( sat_solver2 * s ) +{ + extern void * Proof_DeriveCore( Vec_Set_t * vProof, int hRoot ); + return Proof_DeriveCore( &s->Proofs, s->hProofLast ); +} ABC_NAMESPACE_IMPL_END diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index cba57638..36d2a1ad 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -21,15 +21,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef ABC__sat__bsat__satSolver2_h #define ABC__sat__bsat__satSolver2_h - + #include <stdio.h> #include <stdlib.h> #include <string.h> #include <assert.h> -#include "satClause.h" #include "satVec.h" +#include "satClause.h" #include "misc/vec/vecSet.h" ABC_NAMESPACE_HEADER_START @@ -63,17 +63,12 @@ extern void Sat_Solver2DoubleClauses( sat_solver2 * p, int iVar ); // global variables extern int var_is_partA (sat_solver2* s, int v); extern void var_set_partA(sat_solver2* s, int v, int partA); -// clause grouping (these two only work after creating a clause before the solver is called) -extern int clause2_is_partA (sat_solver2* s, int handle); -extern void clause2_set_partA(sat_solver2* s, int handle, int partA); -// other clause functions -extern int clause2_id(sat_solver2* s, int h); - + // proof-based APIs extern void * Sat_ProofCore( sat_solver2 * s ); extern void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ); extern word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars ); -extern void Sat_ProofReduce( sat_solver2 * s ); +extern int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot ); extern void Sat_ProofCheck( sat_solver2 * s ); //================================================================================================= @@ -106,28 +101,27 @@ struct sat_solver2_t unsigned* activity; // A heuristic measurement of the activity of a variable. #endif + int nUnits; // the total number of unit clauses + int nof_learnts; // the number of clauses to trigger reduceDB int nLearntMax; // enables using reduce DB method + int nLearntStart; // starting learned clause limit + int nLearntDelta; // delta of learned clause limit + int nLearntRatio; // ratio percentage of learned clauses + int nDBreduces; // number of DB reductions 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 fVerbose; // clauses - veci clauses; // clause memory - veci learnts; // learnt memory + Sat_Mem_t Mem; veci* wlists; // watcher lists (for each literal) - veci claActs; // clause activities + veci act_clas; // clause activities veci claProofs; // clause proofs - int hLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) - int hProofLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) - int nof_learnts; // the number of clauses to trigger reduceDB // rollback int iVarPivot; // the pivot for variables int iTrailPivot; // the pivot for trail - int iProofPivot; // the pivot for proof records - int hClausePivot; // the pivot for problem clause - int hLearntPivot; // the pivot for learned clause int hProofPivot; // the pivot for proof records // internal state @@ -155,7 +149,8 @@ struct sat_solver2_t // proof logging Vec_Set_t Proofs; // sequence of proof records veci temp_proof; // temporary place to store proofs - int nUnits; // the total number of unit clauses + int hLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) + int hProofLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) // statistics stats_t stats; @@ -164,40 +159,13 @@ struct sat_solver2_t clock_t 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) ) -#define satset_foreach_entry_vec( pVec, p, c, i ) \ - 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++ ) +static inline clause * clause2_read( sat_solver2 * s, cla h ) { return Sat_MemClauseHand( &s->Mem, h ); } +static inline int clause2_proofid(sat_solver2* s, clause* c, int partA) { return c->lrn ? (veci_begin(&s->claProofs)[clause_id(c)]<<2) | (partA<<1) : ((clause_id(c)+1)<<2) | (partA<<1) | 1; } -#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 ) +// these two only work after creating a clause before the solver is called +static inline int clause2_is_partA (sat_solver2* s, int h) { return clause2_read(s, h)->partA; } +static inline void clause2_set_partA(sat_solver2* s, int h, int partA) { clause2_read(s, h)->partA = partA; } +static inline int clause2_id(sat_solver2* s, int h) { return clause_id(clause2_read(s, h)); } //================================================================================================= // Public APIs: @@ -265,10 +233,8 @@ static inline void sat_solver2_bookmark(sat_solver2* s) assert( s->qhead == s->qtail ); s->iVarPivot = s->size; s->iTrailPivot = s->qhead; - s->iProofPivot = Vec_SetEntryNum(&s->Proofs); - s->hClausePivot = veci_size(&s->clauses); - s->hLearntPivot = veci_size(&s->learnts); s->hProofPivot = Vec_SetHandCurrent(&s->Proofs); + Sat_MemBookMark( &s->Mem ); } static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fCompl, int fMark ) diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c index 1694ae01..05b9403d 100644 --- a/src/sat/bsat/satUtil.c +++ b/src/sat/bsat/satUtil.c @@ -211,6 +211,7 @@ void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * s ) printf( "propagations : %10d\n", (int)s->stats.propagations ); // printf( "inspects : %10d\n", (int)s->stats.inspects ); // printf( "inspects2 : %10d\n", (int)s->stats.inspects2 ); +/* printf( "memory for variables %.1f MB (free %6.2f %%) and clauses %.1f MB (free %6.2f %%)\n", 1.0 * Sat_Solver2GetVarMem(s) * s->size / (1<<20), 100.0 * (s->cap - s->size) / s->cap, @@ -218,6 +219,7 @@ void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * s ) 100.0 * (s->clauses.cap - s->clauses.size + s->learnts.cap - s->learnts.size) / (s->clauses.cap + s->learnts.cap) ); +*/ } /**Function************************************************************* diff --git a/src/sat/bsat/satVec.h b/src/sat/bsat/satVec.h index 8a711007..8cc8ba4e 100644 --- a/src/sat/bsat/satVec.h +++ b/src/sat/bsat/satVec.h @@ -127,6 +127,9 @@ static inline void vecp_remove(vecp* v, void* e) #endif #endif +typedef int lit; +typedef int cla; + typedef char lbool; static const int var_Undef = -1; |