src/sat/msat/msatSolverCore.c File Reference

#include "msatInt.h"

Include dependency graph for msatSolverCore.c:

Go to the source code of this file.

Functions
bool	Msat_SolverAddVar (Msat_Solver_t *p, int Level)
bool	Msat_SolverAddClause (Msat_Solver_t *p, Msat_IntVec_t *vLits)
double	Msat_SolverProgressEstimate (Msat_Solver_t *p)
void	Msat_SolverPrintStats (Msat_Solver_t *p)
bool	Msat_SolverSolve (Msat_Solver_t *p, Msat_IntVec_t *vAssumps, int nBackTrackLimit, int nTimeLimit)

---

Function Documentation

bool Msat_SolverAddClause	(	Msat_Solver_t *	p,
		Msat_IntVec_t *	vLits
	)

Function*************************************************************

Synopsis [Adds one clause to the solver's clause database.]

Description []

SideEffects []

SeeAlso []

Definition at line 62 of file msatSolverCore.c.

{
    Msat_Clause_t * pC; 
    bool Value;
    Value = Msat_ClauseCreate( p, vLits, 0, &pC );
    if ( pC != NULL )
        Msat_ClauseVecPush( p->vClauses, pC );
//    else if ( p->fProof )
//        Msat_ClauseCreateFake( p, vLits );
    return Value;
}

bool Msat_SolverAddVar	(	Msat_Solver_t *	p,
		int	Level
	)

CFile****************************************************************

FileName [msatSolverCore.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 SAT solver core procedures.]

Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 1, 2004.]

Revision [

Id

msatSolverCore.c,v 1.2 2004/05/12 03:37:40 satrajit Exp

] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Adds one variable to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file msatSolverCore.c.

{
    if ( p->nVars == p->nVarsAlloc )
        Msat_SolverResize( p, 2 * p->nVarsAlloc );
    p->pLevel[p->nVars] = Level;
    p->nVars++;
    return 1;
}

void Msat_SolverPrintStats

(

Msat_Solver_t *

p

)

Function*************************************************************

Synopsis [Prints statistics about the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 107 of file msatSolverCore.c.

{
    printf("C solver (%d vars; %d clauses; %d learned):\n", 
        p->nVars, Msat_ClauseVecReadSize(p->vClauses), Msat_ClauseVecReadSize(p->vLearned) );
    printf("starts        : %lld\n", p->Stats.nStarts);
    printf("conflicts     : %lld\n", p->Stats.nConflicts);
    printf("decisions     : %lld\n", p->Stats.nDecisions);
    printf("propagations  : %lld\n", p->Stats.nPropagations);
    printf("inspects      : %lld\n", p->Stats.nInspects);
}

double Msat_SolverProgressEstimate

(

Msat_Solver_t *

p

)

Function*************************************************************

Synopsis [Returns search-space coverage. Not extremely reliable.]

Description []

SideEffects []

SeeAlso []

Definition at line 85 of file msatSolverCore.c.

{
    double dProgress = 0.0;
    double dF = 1.0 / p->nVars;
    int i;
    for ( i = 0; i < p->nVars; i++ )
        if ( p->pAssigns[i] != MSAT_VAR_UNASSIGNED )
            dProgress += pow( dF, p->pLevel[i] );
    return dProgress / p->nVars;
}

bool Msat_SolverSolve	(	Msat_Solver_t *	p,
		Msat_IntVec_t *	vAssumps,
		int	nBackTrackLimit,
		int	nTimeLimit
	)

Function*************************************************************

Synopsis [Top-level solve.]

Description [If using assumptions (non-empty 'assumps' vector), you must call 'simplifyDB()' first to see that no top-level conflict is present (which would put the solver in an undefined state. If the last argument is given (vProj), the solver enumerates through the satisfying solutions, which are projected on the variables listed in this array. Note that the variables in the array may be complemented, in which case the derived assignment for the variable is complemented.]

SideEffects []

SeeAlso []

Definition at line 135 of file msatSolverCore.c.

{
    Msat_SearchParams_t Params = { 0.95, 0.999 };
    double nConflictsLimit, nLearnedLimit;
    Msat_Type_t Status;
    int timeStart = clock();
    int64 nConflictsOld = p->Stats.nConflicts;
    int64 nDecisionsOld = p->Stats.nDecisions;

//    p->pFreq = ALLOC( int, p->nVarsAlloc );
//    memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc );
 
    if ( vAssumps )
    {
        int * pAssumps, nAssumps, i;

        assert( Msat_IntVecReadSize(p->vTrailLim) == 0 );

        nAssumps = Msat_IntVecReadSize( vAssumps );
        pAssumps = Msat_IntVecReadArray( vAssumps );
        for ( i = 0; i < nAssumps; i++ )
        {
            if ( !Msat_SolverAssume(p, pAssumps[i]) || Msat_SolverPropagate(p) )
            {
                Msat_QueueClear( p->pQueue );
                Msat_SolverCancelUntil( p, 0 );
                return MSAT_FALSE;
            }
        }
    }
    p->nLevelRoot   = Msat_SolverReadDecisionLevel(p);
    p->nClausesInit = Msat_ClauseVecReadSize( p->vClauses );    
    nConflictsLimit = 100;
    nLearnedLimit   = Msat_ClauseVecReadSize(p->vClauses) / 3;
    Status = MSAT_UNKNOWN;
    p->nBackTracks = (int)p->Stats.nConflicts;
    while ( Status == MSAT_UNKNOWN )
    {
        if ( p->fVerbose )
            printf("Solving -- conflicts=%d   learnts=%d   progress=%.4f %%\n", 
                (int)nConflictsLimit, (int)nLearnedLimit, p->dProgress*100);
        Status = Msat_SolverSearch( p, (int)nConflictsLimit, (int)nLearnedLimit, nBackTrackLimit, &Params );
        nConflictsLimit *= 1.5;
        nLearnedLimit   *= 1.1;
        // if the limit on the number of backtracks is given, quit the restart loop
        if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit )
            break;
        // if the runtime limit is exceeded, quit the restart loop
        if ( nTimeLimit > 0 && clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC )
            break;
    }
    Msat_SolverCancelUntil( p, 0 );
    p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks;
/*
    PRT( "True solver runtime", clock() - timeStart );
    // print the statistics
    {
        int i, Counter = 0;
        for ( i = 0; i < p->nVars; i++ )
            if ( p->pFreq[i] > 0 )
            {
                printf( "%d ", p->pFreq[i] );
                Counter++;
            }
        if ( Counter )
            printf( "\n" );
        printf( "Total = %d. Used = %d.  Decisions = %d. Imps = %d. Conflicts = %d. ", p->nVars, Counter, (int)p->Stats.nDecisions, (int)p->Stats.nPropagations, (int)p->Stats.nConflicts );
        PRT( "Time", clock() - timeStart );
    }
*/
    return Status;
}