msatSolverCore.c 7.1 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
/**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 $]

***********************************************************************/

#include "msatInt.h"

23 24 25
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
26 27 28 29 30
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
Alan Mishchenko committed
31
///                     FUNCTION DEFINITIONS                         ///
Alan Mishchenko committed
32 33 34 35 36 37 38 39 40 41 42 43 44
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    [Adds one variable to the solver.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
45
int  Msat_SolverAddVar( Msat_Solver_t * p, int Level )
Alan Mishchenko committed
46 47 48
{
    if ( p->nVars == p->nVarsAlloc )
        Msat_SolverResize( p, 2 * p->nVarsAlloc );
Alan Mishchenko committed
49
    p->pLevel[p->nVars] = Level;
Alan Mishchenko committed
50 51 52 53 54 55 56 57 58 59 60 61 62 63 64
    p->nVars++;
    return 1;
}

/**Function*************************************************************

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

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
65
int  Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * vLits )
Alan Mishchenko committed
66 67
{
    Msat_Clause_t * pC; 
68
    int  Value;
Alan Mishchenko committed
69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113
    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;
}

/**Function*************************************************************

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

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
double Msat_SolverProgressEstimate( Msat_Solver_t * p )
{
    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;
}

/**Function*************************************************************

  Synopsis    [Prints statistics about the solver.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Msat_SolverPrintStats( Msat_Solver_t * p )
{
    printf("C solver (%d vars; %d clauses; %d learned):\n", 
        p->nVars, Msat_ClauseVecReadSize(p->vClauses), Msat_ClauseVecReadSize(p->vLearned) );
114 115 116 117 118
    printf("starts        : %d\n", (int)p->Stats.nStarts);
    printf("conflicts     : %d\n", (int)p->Stats.nConflicts);
    printf("decisions     : %d\n", (int)p->Stats.nDecisions);
    printf("propagations  : %d\n", (int)p->Stats.nPropagations);
    printf("inspects      : %d\n", (int)p->Stats.nInspects);
Alan Mishchenko committed
119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137
}

/**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     []

***********************************************************************/
138
int  Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTrackLimit, int nTimeLimit )
Alan Mishchenko committed
139 140 141 142
{
    Msat_SearchParams_t Params = { 0.95, 0.999 };
    double nConflictsLimit, nLearnedLimit;
    Msat_Type_t Status;
143
    clock_t timeStart = clock();
Alan Mishchenko committed
144

Alan Mishchenko committed
145
//    p->pFreq = ABC_ALLOC( int, p->nVarsAlloc );
Alan Mishchenko committed
146 147
//    memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc );
 
Alan Mishchenko committed
148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180
    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
Alan Mishchenko committed
181 182 183 184
        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 )
Alan Mishchenko committed
185
            break;
Alan Mishchenko committed
186 187 188
    }
    Msat_SolverCancelUntil( p, 0 );
    p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks;
Alan Mishchenko committed
189
/*
Alan Mishchenko committed
190
    ABC_PRT( "True solver runtime", clock() - timeStart );
Alan Mishchenko committed
191 192 193 194 195 196 197 198 199 200 201 202
    // 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 );
Alan Mishchenko committed
203
        ABC_PRT( "Time", clock() - timeStart );
Alan Mishchenko committed
204 205
    }
*/
Alan Mishchenko committed
206 207 208 209 210 211 212 213
    return Status;
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


214 215
ABC_NAMESPACE_IMPL_END