diff options
Diffstat (limited to 'src/sat/msat/msatSolverSearch.c')
| -rw-r--r-- | src/sat/msat/msatSolverSearch.c | 629 |
1 files changed, 0 insertions, 629 deletions
diff --git a/src/sat/msat/msatSolverSearch.c b/src/sat/msat/msatSolverSearch.c deleted file mode 100644 index 11a6540c..00000000 --- a/src/sat/msat/msatSolverSearch.c +++ /dev/null @@ -1,629 +0,0 @@ -/**CFile**************************************************************** - - FileName [msatSolverSearch.c] - - PackageName [A C version of SAT solver MINISAT, originally developed - in C++ by Niklas Een and Niklas Sorensson, Chalmers University of - Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] - - Synopsis [The search part of the solver.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 1, 2004.] - - Revision [$Id: msatSolverSearch.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "msatInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static void Msat_SolverUndoOne( Msat_Solver_t * p ); -static void Msat_SolverCancel( Msat_Solver_t * p ); -static Msat_Clause_t * Msat_SolverRecord( Msat_Solver_t * p, Msat_IntVec_t * vLits ); -static void Msat_SolverAnalyze( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_IntVec_t * vLits_out, int * pLevel_out ); -static void Msat_SolverReduceDB( Msat_Solver_t * p ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Makes the next assumption (Lit).] - - Description [Returns FALSE if immediate conflict.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -bool Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit ) -{ - assert( Msat_QueueReadSize(p->pQueue) == 0 ); - if ( p->fVerbose ) - printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(Lit)); - Msat_IntVecPush( p->vTrailLim, Msat_IntVecReadSize(p->vTrail) ); -// assert( Msat_IntVecReadSize(p->vTrailLim) <= Msat_IntVecReadSize(p->vTrail) + 1 ); -// assert( Msat_IntVecReadSize( p->vTrailLim ) < p->nVars ); - return Msat_SolverEnqueue( p, Lit, NULL ); -} - -/**Function************************************************************* - - Synopsis [Reverts one variable binding on the trail.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverUndoOne( Msat_Solver_t * p ) -{ - Msat_Lit_t Lit; - Msat_Var_t Var; - Lit = Msat_IntVecPop( p->vTrail ); - Var = MSAT_LIT2VAR(Lit); - p->pAssigns[Var] = MSAT_VAR_UNASSIGNED; - p->pReasons[Var] = NULL; - p->pLevel[Var] = -1; -// Msat_OrderUndo( p->pOrder, Var ); - Msat_OrderVarUnassigned( p->pOrder, Var ); - - if ( p->fVerbose ) - printf(L_IND"unbind("L_LIT")\n", L_ind, L_lit(Lit)); -} - -/**Function************************************************************* - - Synopsis [Reverts to the state before last Msat_SolverAssume().] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverCancel( Msat_Solver_t * p ) -{ - int c; - assert( Msat_QueueReadSize(p->pQueue) == 0 ); - if ( p->fVerbose ) - { - if ( Msat_IntVecReadSize(p->vTrail) != Msat_IntVecReadEntryLast(p->vTrailLim) ) - { - Msat_Lit_t Lit; - Lit = Msat_IntVecReadEntry( p->vTrail, Msat_IntVecReadEntryLast(p->vTrailLim) ); - printf(L_IND"cancel("L_LIT")\n", L_ind, L_lit(Lit)); - } - } - for ( c = Msat_IntVecReadSize(p->vTrail) - Msat_IntVecPop( p->vTrailLim ); c != 0; c-- ) - Msat_SolverUndoOne( p ); -} - -/**Function************************************************************* - - Synopsis [Reverts to the state at given level.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverCancelUntil( Msat_Solver_t * p, int Level ) -{ - while ( Msat_IntVecReadSize(p->vTrailLim) > Level ) - Msat_SolverCancel(p); -} - - -/**Function************************************************************* - - Synopsis [Record a clause and drive backtracking.] - - Description [vLits[0] must contain the asserting literal.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_Clause_t * Msat_SolverRecord( Msat_Solver_t * p, Msat_IntVec_t * vLits ) -{ - Msat_Clause_t * pC; - int Value; - assert( Msat_IntVecReadSize(vLits) != 0 ); - Value = Msat_ClauseCreate( p, vLits, 1, &pC ); - assert( Value ); - Value = Msat_SolverEnqueue( p, Msat_IntVecReadEntry(vLits,0), pC ); - assert( Value ); - if ( pC ) - Msat_ClauseVecPush( p->vLearned, pC ); - return pC; -} - -/**Function************************************************************* - - Synopsis [Enqueues one variable assignment.] - - Description [Puts a new fact on the propagation queue and immediately - updates the variable value. Should a conflict arise, FALSE is returned. - Otherwise returns TRUE.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -bool Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC ) -{ - Msat_Var_t Var = MSAT_LIT2VAR(Lit); - - // skip literals that are not in the current cone - if ( !Msat_IntVecReadEntry( p->vVarsUsed, Var ) ) - return 1; - -// assert( Msat_QueueReadSize(p->pQueue) == Msat_IntVecReadSize(p->vTrail) ); - // if the literal is assigned - // return 1 if the assignment is consistent - // return 0 if the assignment is inconsistent (conflict) - if ( p->pAssigns[Var] != MSAT_VAR_UNASSIGNED ) - return p->pAssigns[Var] == Lit; - // new fact - store it - if ( p->fVerbose ) - { -// printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(Lit)); - printf(L_IND"bind("L_LIT") ", L_ind, L_lit(Lit)); - Msat_ClausePrintSymbols( pC ); - } - p->pAssigns[Var] = Lit; - p->pLevel[Var] = Msat_IntVecReadSize(p->vTrailLim); -// p->pReasons[Var] = p->pLevel[Var]? pC: NULL; - p->pReasons[Var] = pC; - Msat_IntVecPush( p->vTrail, Lit ); - Msat_QueueInsert( p->pQueue, Lit ); - - Msat_OrderVarAssigned( p->pOrder, Var ); - return 1; -} - -/**Function************************************************************* - - Synopsis [Propagates the assignments in the queue.] - - Description [Propagates all enqueued facts. If a conflict arises, - the conflicting clause is returned, otherwise NULL.] - - SideEffects [The propagation queue is empty, even if there was a conflict.] - - SeeAlso [] - -***********************************************************************/ -Msat_Clause_t * Msat_SolverPropagate( Msat_Solver_t * p ) -{ - Msat_ClauseVec_t ** pvWatched = p->pvWatched; - Msat_Clause_t ** pClauses; - Msat_Clause_t * pConflict; - Msat_Lit_t Lit, Lit_out; - int i, j, nClauses; - - // propagate all the literals in the queue - while ( (Lit = Msat_QueueExtract( p->pQueue )) >= 0 ) - { - p->Stats.nPropagations++; - // get the clauses watched by this literal - nClauses = Msat_ClauseVecReadSize( pvWatched[Lit] ); - pClauses = Msat_ClauseVecReadArray( pvWatched[Lit] ); - // go through the watched clauses and decide what to do with them - for ( i = j = 0; i < nClauses; i++ ) - { - p->Stats.nInspects++; - // clear the returned literal - Lit_out = -1; - // propagate the clause - if ( !Msat_ClausePropagate( pClauses[i], Lit, p->pAssigns, &Lit_out ) ) - { // the clause is unit - // "Lit_out" contains the new assignment to be enqueued - if ( Msat_SolverEnqueue( p, Lit_out, pClauses[i] ) ) - { // consistent assignment - // no changes to the implication queue; the watch is the same too - pClauses[j++] = pClauses[i]; - continue; - } - // remember the reason of conflict (will be returned) - pConflict = pClauses[i]; - // leave the remaning clauses in the same watched list - for ( ; i < nClauses; i++ ) - pClauses[j++] = pClauses[i]; - Msat_ClauseVecShrink( pvWatched[Lit], j ); - // clear the propagation queue - Msat_QueueClear( p->pQueue ); - return pConflict; - } - // the clause is not unit - // in this case "Lit_out" contains the new watch if it has changed - if ( Lit_out >= 0 ) - Msat_ClauseVecPush( pvWatched[Lit_out], pClauses[i] ); - else // the watch did not change - pClauses[j++] = pClauses[i]; - } - Msat_ClauseVecShrink( pvWatched[Lit], j ); - } - return NULL; -} - -/**Function************************************************************* - - Synopsis [Simplifies the data base.] - - Description [Simplify all constraints according to the current top-level - assigment (redundant constraints may be removed altogether).] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -bool Msat_SolverSimplifyDB( Msat_Solver_t * p ) -{ - Msat_ClauseVec_t * vClauses; - Msat_Clause_t ** pClauses; - int nClauses, Type, i, j; - int * pAssigns; - int Counter; - - assert( Msat_SolverReadDecisionLevel(p) == 0 ); - if ( Msat_SolverPropagate(p) != NULL ) - return 0; -//Msat_SolverPrintClauses( p ); -//Msat_SolverPrintAssignment( p ); -//printf( "Simplification\n" ); - - // simplify and reassign clause numbers - Counter = 0; - pAssigns = Msat_SolverReadAssignsArray( p ); - for ( Type = 0; Type < 2; Type++ ) - { - vClauses = Type? p->vLearned : p->vClauses; - nClauses = Msat_ClauseVecReadSize( vClauses ); - pClauses = Msat_ClauseVecReadArray( vClauses ); - for ( i = j = 0; i < nClauses; i++ ) - if ( Msat_ClauseSimplify( pClauses[i], pAssigns ) ) - Msat_ClauseFree( p, pClauses[i], 1 ); - else - { - pClauses[j++] = pClauses[i]; - Msat_ClauseSetNum( pClauses[i], Counter++ ); - } - Msat_ClauseVecShrink( vClauses, j ); - } - p->nClauses = Counter; - return 1; -} - -/**Function************************************************************* - - Synopsis [Cleans the clause databased from the useless learnt clauses.] - - Description [Removes half of the learnt clauses, minus the clauses locked - by the current assignment. Locked clauses are clauses that are reason - to a some assignment.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverReduceDB( Msat_Solver_t * p ) -{ - Msat_Clause_t ** pLearned; - int nLearned, i, j; - double dExtraLim = p->dClaInc / Msat_ClauseVecReadSize(p->vLearned); - // Remove any clause below this activity - - // sort the learned clauses in the increasing order of activity - Msat_SolverSortDB( p ); - - // discard the first half the clauses (the less active ones) - nLearned = Msat_ClauseVecReadSize( p->vLearned ); - pLearned = Msat_ClauseVecReadArray( p->vLearned ); - for ( i = j = 0; i < nLearned / 2; i++ ) - if ( !Msat_ClauseIsLocked( p, pLearned[i]) ) - Msat_ClauseFree( p, pLearned[i], 1 ); - else - pLearned[j++] = pLearned[i]; - // filter the more active clauses and leave those above the limit - for ( ; i < nLearned; i++ ) - if ( !Msat_ClauseIsLocked( p, pLearned[i] ) && - Msat_ClauseReadActivity(pLearned[i]) < dExtraLim ) - Msat_ClauseFree( p, pLearned[i], 1 ); - else - pLearned[j++] = pLearned[i]; - Msat_ClauseVecShrink( p->vLearned, j ); -} - -/**Function************************************************************* - - Synopsis [Removes the learned clauses.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverRemoveLearned( Msat_Solver_t * p ) -{ - Msat_Clause_t ** pLearned; - int nLearned, i; - - // discard the learned clauses - nLearned = Msat_ClauseVecReadSize( p->vLearned ); - pLearned = Msat_ClauseVecReadArray( p->vLearned ); - for ( i = 0; i < nLearned; i++ ) - { - assert( !Msat_ClauseIsLocked( p, pLearned[i]) ); - - Msat_ClauseFree( p, pLearned[i], 1 ); - } - Msat_ClauseVecShrink( p->vLearned, 0 ); - p->nClauses = Msat_ClauseVecReadSize(p->vClauses); - - for ( i = 0; i < p->nVarsAlloc; i++ ) - p->pReasons[i] = NULL; -} - -/**Function************************************************************* - - Synopsis [Removes the recently added clauses.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverRemoveMarked( Msat_Solver_t * p ) -{ - Msat_Clause_t ** pLearned, ** pClauses; - int nLearned, nClauses, i; - - // discard the learned clauses - nClauses = Msat_ClauseVecReadSize( p->vClauses ); - pClauses = Msat_ClauseVecReadArray( p->vClauses ); - for ( i = p->nClausesStart; i < nClauses; i++ ) - { -// assert( !Msat_ClauseIsLocked( p, pClauses[i]) ); - Msat_ClauseFree( p, pClauses[i], 1 ); - } - Msat_ClauseVecShrink( p->vClauses, p->nClausesStart ); - - // discard the learned clauses - nLearned = Msat_ClauseVecReadSize( p->vLearned ); - pLearned = Msat_ClauseVecReadArray( p->vLearned ); - for ( i = 0; i < nLearned; i++ ) - { -// assert( !Msat_ClauseIsLocked( p, pLearned[i]) ); - Msat_ClauseFree( p, pLearned[i], 1 ); - } - Msat_ClauseVecShrink( p->vLearned, 0 ); - p->nClauses = Msat_ClauseVecReadSize(p->vClauses); -/* - // undo the previous data - for ( i = 0; i < p->nVarsAlloc; i++ ) - { - p->pAssigns[i] = MSAT_VAR_UNASSIGNED; - p->pReasons[i] = NULL; - p->pLevel[i] = -1; - p->pdActivity[i] = 0.0; - } - Msat_OrderClean( p->pOrder, p->nVars, NULL ); - Msat_QueueClear( p->pQueue ); -*/ -} - - - -/**Function************************************************************* - - Synopsis [Analyze conflict and produce a reason clause.] - - Description [Current decision level must be greater than root level.] - - SideEffects [vLits_out[0] is the asserting literal at level pLevel_out.] - - SeeAlso [] - -***********************************************************************/ -void Msat_SolverAnalyze( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_IntVec_t * vLits_out, int * pLevel_out ) -{ - Msat_Lit_t LitQ, Lit = MSAT_LIT_UNASSIGNED; - Msat_Var_t VarQ, Var; - int * pReasonArray, nReasonSize; - int j, pathC = 0, nLevelCur = Msat_IntVecReadSize(p->vTrailLim); - int iStep = Msat_IntVecReadSize(p->vTrail) - 1; - - // increment the seen counter - p->nSeenId++; - // empty the vector array - Msat_IntVecClear( vLits_out ); - Msat_IntVecPush( vLits_out, -1 ); // (leave room for the asserting literal) - *pLevel_out = 0; - do { - assert( pC != NULL ); // (otherwise should be UIP) - // get the reason of conflict - Msat_ClauseCalcReason( p, pC, Lit, p->vReason ); - nReasonSize = Msat_IntVecReadSize( p->vReason ); - pReasonArray = Msat_IntVecReadArray( p->vReason ); - for ( j = 0; j < nReasonSize; j++ ) { - LitQ = pReasonArray[j]; - VarQ = MSAT_LIT2VAR(LitQ); - if ( p->pSeen[VarQ] != p->nSeenId ) { - p->pSeen[VarQ] = p->nSeenId; - - // added to better fine-tune the search - Msat_SolverVarBumpActivity( p, LitQ ); - - // skip all the literals on this decision level - if ( p->pLevel[VarQ] == nLevelCur ) - pathC++; - else if ( p->pLevel[VarQ] > 0 ) { - // add the literals on other decision levels but - // exclude variables from decision level 0 - Msat_IntVecPush( vLits_out, MSAT_LITNOT(LitQ) ); - if ( *pLevel_out < p->pLevel[VarQ] ) - *pLevel_out = p->pLevel[VarQ]; - } - } - } - // Select next clause to look at: - do { -// Lit = Msat_IntVecReadEntryLast(p->vTrail); - Lit = Msat_IntVecReadEntry( p->vTrail, iStep-- ); - Var = MSAT_LIT2VAR(Lit); - pC = p->pReasons[Var]; -// Msat_SolverUndoOne( p ); - } while ( p->pSeen[Var] != p->nSeenId ); - pathC--; - } while ( pathC > 0 ); - // we do not unbind the variables above - // this will be done after conflict analysis - - Msat_IntVecWriteEntry( vLits_out, 0, MSAT_LITNOT(Lit) ); - if ( p->fVerbose ) - { - printf( L_IND"Learnt {", L_ind ); - nReasonSize = Msat_IntVecReadSize( vLits_out ); - pReasonArray = Msat_IntVecReadArray( vLits_out ); - for ( j = 0; j < nReasonSize; j++ ) - printf(" "L_LIT, L_lit(pReasonArray[j])); - printf(" } at level %d\n", *pLevel_out); - } -} - -/**Function************************************************************* - - Synopsis [The search procedure called between the restarts.] - - Description [Search for a satisfying solution as long as the number of - conflicts does not exceed the limit (nConfLimit) while keeping the number - of learnt clauses below the provided limit (nLearnedLimit). NOTE! Use - negative value for nConfLimit or nLearnedLimit to indicate infinity.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLimit, int nBackTrackLimit, Msat_SearchParams_t * pPars ) -{ - Msat_Clause_t * pConf; - Msat_Var_t Var; - int nLevelBack, nConfs, nAssigns, Value; - int i; - - assert( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot ); - p->Stats.nStarts++; - p->dVarDecay = 1 / pPars->dVarDecay; - p->dClaDecay = 1 / pPars->dClaDecay; - - // reset the activities - for ( i = 0; i < p->nVars; i++ ) - p->pdActivity[i] = (double)p->pFactors[i]; -// p->pdActivity[i] = 0.0; - - nConfs = 0; - while ( 1 ) - { - pConf = Msat_SolverPropagate( p ); - if ( pConf != NULL ){ - // CONFLICT - if ( p->fVerbose ) - { -// printf(L_IND"**CONFLICT**\n", L_ind); - printf(L_IND"**CONFLICT** ", L_ind); - Msat_ClausePrintSymbols( pConf ); - } - // count conflicts - p->Stats.nConflicts++; - nConfs++; - - // if top level, return UNSAT - if ( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot ) - return MSAT_FALSE; - - // perform conflict analysis - Msat_SolverAnalyze( p, pConf, p->vTemp, &nLevelBack ); - Msat_SolverCancelUntil( p, (p->nLevelRoot > nLevelBack)? p->nLevelRoot : nLevelBack ); - Msat_SolverRecord( p, p->vTemp ); - - // it is important that recording is done after cancelling - // because canceling cleans the queue while recording adds to it - Msat_SolverVarDecayActivity( p ); - Msat_SolverClaDecayActivity( p ); - - } - else{ - // NO CONFLICT - if ( Msat_IntVecReadSize(p->vTrailLim) == 0 ) { - // Simplify the set of problem clauses: -// Value = Msat_SolverSimplifyDB(p); -// assert( Value ); - } - nAssigns = Msat_IntVecReadSize( p->vTrail ); - if ( nLearnedLimit >= 0 && Msat_ClauseVecReadSize(p->vLearned) >= nLearnedLimit + nAssigns ) { - // Reduce the set of learnt clauses: - Msat_SolverReduceDB(p); - } - - Var = Msat_OrderVarSelect( p->pOrder ); - if ( Var == MSAT_ORDER_UNKNOWN ) { - // Model found and stored in p->pAssigns - memcpy( p->pModel, p->pAssigns, sizeof(int) * p->nVars ); - Msat_QueueClear( p->pQueue ); - Msat_SolverCancelUntil( p, p->nLevelRoot ); - return MSAT_TRUE; - } - if ( nConfLimit > 0 && nConfs > nConfLimit ) { - // Reached bound on number of conflicts: - p->dProgress = Msat_SolverProgressEstimate( p ); - Msat_QueueClear( p->pQueue ); - Msat_SolverCancelUntil( p, p->nLevelRoot ); - return MSAT_UNKNOWN; - } - else if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit ) { - // Reached bound on number of conflicts: - Msat_QueueClear( p->pQueue ); - Msat_SolverCancelUntil( p, p->nLevelRoot ); - return MSAT_UNKNOWN; - } - else{ - // New variable decision: - p->Stats.nDecisions++; - assert( Var != MSAT_ORDER_UNKNOWN && Var >= 0 && Var < p->nVars ); - Value = Msat_SolverAssume(p, MSAT_VAR2LIT(Var,0) ); - assert( Value ); - } - } - } -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - |