diff options
Diffstat (limited to 'src/sat/msat/msatSolverSearch.c')
| -rw-r--r-- | src/sat/msat/msatSolverSearch.c | 623 |
1 files changed, 623 insertions, 0 deletions
diff --git a/src/sat/msat/msatSolverSearch.c b/src/sat/msat/msatSolverSearch.c new file mode 100644 index 00000000..13a0c403 --- /dev/null +++ b/src/sat/msat/msatSolverSearch.c @@ -0,0 +1,623 @@ +/**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 DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**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; + + assert( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot ); + p->Stats.nStarts++; + p->dVarDecay = 1 / pPars->dVarDecay; + p->dClaDecay = 1 / pPars->dClaDecay; + + 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 && nConfs > 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 /// +//////////////////////////////////////////////////////////////////////// + + |