#include "satInt.h"
Include dependency graph for satDecision.c:
Go to the source code of this file.
Functions | |
| static int | ScoreCompare (const void *node1, const void *node2) |
| satLevel_t * | sat_MakeDecision (satManager_t *cm) |
| long | sat_DecisionBasedOnLatestConflict (satManager_t *cm, satLevel_t *d) |
| void | sat_CheckDecisonVariableArray (satManager_t *cm) |
| long | sat_DecisionBasedOnScore (satManager_t *cm, satLevel_t *d) |
| long | sat_DecisionBasedOnBDD (satManager_t *cm, satLevel_t *d) |
| long | sat_DecisionBasedOnShrink (satManager_t *cm) |
| void | sat_UpdateScore (satManager_t *cm) |
| void | sat_UpdateDVH (satManager_t *cm, satLevel_t *d, satArray_t *clauseArray, int bLevel, long unitLit) |
| void | sat_CheckOrderedVariableArray (satManager_t *cm) |
| void | sat_InitScore (satManager_t *cm) |
| void | sat_InitScoreForMixed (satManager_t *cm) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: satDecision.c,v 1.28 2009/04/11 18:26:37 fabio Exp $" |
| static satManager_t * | SatCm |
Function Documentation
| void sat_CheckDecisonVariableArray | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [ Check decision variable to check correctness of currentVarPos, since currentVarPos has to point lowest variable that are not implied.]
Description [ Check decision variable to check correctness of currentVarPos, since currentVarPos has to point lowest variable that are not implied.]
SideEffects []
SeeAlso []
Definition at line 266 of file satDecision.c.
{
satArray_t *orderedVariableArray;
int size, i;
long v;
orderedVariableArray = cm->orderedVariableArray;
size = orderedVariableArray->num;
for(i=0; i<cm->currentVarPos; i++) {
v = orderedVariableArray->space[i];
if(SATvalue(v) > 1) {
fprintf(stdout, " ERROR : wrong current variable pos %d at %d\n",
cm->currentVarPos, i);
}
}
}
| void sat_CheckOrderedVariableArray | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [ Check correctness of variable order ]
Description [ Check correctness of variable order ]
SideEffects []
SeeAlso []
Definition at line 597 of file satDecision.c.
{
satArray_t *ordered;
satVariable_t *var;
int i;
long v;
ordered = cm->orderedVariableArray;
for(i=0; i<ordered->num; i++) {
v = ordered->space[i];
var = SATgetVariable(v);
if(i != var->pos) {
fprintf(cm->stdOut, "Error : wrong variable position %d %d in ordered array\n", i, var->pos);
}
}
}
| long sat_DecisionBasedOnBDD | ( | satManager_t * | cm, |
| satLevel_t * | d | ||
| ) |
Function********************************************************************
Synopsis [ Take care of decision by BDD based mathod ]
Description [ Take care of decision by BDD based mathod ]
SideEffects []
SeeAlso []
for(i=0; i<arr->num; i++) { v = arr->space[i]; nv = SATnormalNode(v); if(SATvalue(nv) > 1) return(v); }
Definition at line 352 of file satDecision.c.
{
satArray_t *arr;
long nv, v;
if(cm->assignByBDD == 0)
return(0);
arr = cm->assignByBDD;
if(arr->num == 0)
return(0);
while(arr->num) {
v = arr->space[arr->num-1];
nv = SATnormalNode(v);
arr->num--;
if(SATvalue(nv) > 1)
return(v);
}
return(0);
}
Here is the caller graph for this function:
| long sat_DecisionBasedOnLatestConflict | ( | satManager_t * | cm, |
| satLevel_t * | d | ||
| ) |
Function********************************************************************
Synopsis [ Decision making based on current top clause ]
Description [ Decision making based on current top clause ]
SideEffects []
SeeAlso []
CONSIDER if(stats->nConflictCl < option->minConflictForDecision) return(0);
for(plit =literals->last-1, i=literals->last - literals->begin; i>=0; i--, plit--) {
Definition at line 123 of file satDecision.c.
{
satOption_t *option;
satStatistics_t *stats;
satLiteralDB_t *literals;
satVariable_t *var;
int size, limit;
long *plit, *tplit;
long v, lit, tv, maxV;
int tsize, count;
int inverted, value;
int i, j, satisfied;
int tmpScore, maxScore;
option = cm->option;
stats = cm->each;
if(!(option->decisionHeuristic & LATEST_CONFLICT_DECISION))
return(0);
if(cm->currentTopConflict == 0)
return(0);
literals = cm->literals;
size = literals->last - literals->begin;
limit = MAXINT;
if(option->maxConflictForDecision > 0)
limit = option->maxConflictForDecision;
count = cm->currentTopConflictCount;
tv = -(*(cm->currentTopConflict));
tsize = SATnumLits(tv);
tplit = (long*)SATfirstLit(tv);
plit = tplit + tsize;
for(i=plit-literals->begin; i>=0; i--, plit--) {
if(count > limit) break;
lit = *plit;
if(lit < 0) {
tv = -lit;
if(!(SATflags(tv) & IsConflictMask))
return(0);
if(plit < (long*)SATfirstLit(tv))
continue;
count++;
if(option->skipSatisfiedClauseForDecision) {
tsize = SATnumLits(tv);
tplit = (long *)SATfirstLit(tv);
satisfied = 0;
maxScore = -1;
maxV = 0;
for(j=0; j<tsize; j++, tplit++) {
v = SATgetNode(*tplit);
inverted = SATisInverted(v);
v = SATnormalNode(v);
value = SATvalue(v) ^ inverted;
if(value == 1) {
satisfied = 1;
break;
}
else if(value == 0) {
continue;
}
var = SATgetVariable(v);
tmpScore = (var->scores[0] >= var->scores[1]) ? var->scores[0] : var->scores[1];
if(tmpScore > maxScore) {
maxScore = tmpScore;
maxV = v;
}
}
if(satisfied) {
i = i - tsize - 1;
plit = plit - tsize -1;
}
else {
var = SATgetVariable(maxV);
value = (var->scores[0] >= var->scores[1]) ? 0 : 1;
cm->currentTopConflict = (long*)SATfirstLit(tv) + SATnumLits(tv);
cm->currentTopConflictCount = count;
stats = cm->each;
stats->nLatestConflictDecisions++;
return(maxV ^ !value);
}
}
continue;
}
else if(lit == 0)
continue;
v = SATgetNode(lit);
inverted = SATisInverted(v);
v = SATnormalNode(v);
value = SATvalue(v) ^ inverted;
if(value >= 2) {
var = SATgetVariable(v);
value = (var->conflictLits[0] >= var->conflictLits[1]) ? 0 : 1;
cm->currentTopConflict = (long*)SATfirstLit(tv) + SATnumLits(tv);
cm->currentTopConflictCount = count;
stats = cm->each;
stats->nLatestConflictDecisions++;
return(v ^ !value);
}
}
return(0);
}
Here is the caller graph for this function:
| long sat_DecisionBasedOnScore | ( | satManager_t * | cm, |
| satLevel_t * | d | ||
| ) |
Function********************************************************************
Synopsis [ Decision making based on score based heuristic ]
Description [ Decision making based on score based heuristic ]
SideEffects []
SeeAlso []
Definition at line 296 of file satDecision.c.
{
int size, i;
long v;
int value;
satVariable_t *var;
satArray_t *orderedVariableArray;
satStatistics_t *stats;
satOption_t *option;
option = cm->option;
orderedVariableArray = cm->orderedVariableArray;
size = orderedVariableArray->num;
for(i=cm->currentVarPos; i<size; i++) {
v = orderedVariableArray->space[i];
if(SATvalue(v) < 2) continue;
var = SATgetVariable(v);
value = (var->scores[0] >= var->scores[1]) ? 0 : 1;
stats = cm->each;
if((var->scores[0]+var->scores[1]) < 1) {
stats->nLowScoreDecisions++;
}
if((option->decisionHeuristic & DVH_DECISION))
stats->nDVHDecisions++;
else
stats->nVSIDSDecisions++;
cm->currentVarPos = i;
d->currentVarPos = i;
return(v ^ !value);
}
return(0);
}
Here is the caller graph for this function:
| long sat_DecisionBasedOnShrink | ( | satManager_t * | cm | ) |
Definition at line 387 of file satDecision.c.
{
satArray_t *arr;
long nv, v;
if(cm->shrinkArray == 0)
return(0);
arr = cm->shrinkArray;
if(arr->num == 0)
return(0);
while(arr->num) {
v = arr->space[arr->num-1];
nv = SATnormalNode(v);
arr->num--;
if(SATvalue(nv) > 1)
return(v);
}
return(0);
}
| void sat_InitScore | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [ Generate initial score ]
Description [ Generate initial score ]
SideEffects []
SeeAlso []
if(cm->obj && cm->obj->num) { sat_MarkTransitiveFaninForArray(cm, cm->obj, VisitedMask); objExist = 1; }
if(cm->obj && cm->obj->num) { sat_UnmarkTransitiveFaninForArray( cm, cm->obj, VisitedMask, ResetVisitedMask); }
Definition at line 627 of file satDecision.c.
{
int objExist;
int j, inverted;
long *plit, v, nv, i;
int size;
int count0, count1;
satArray_t *ordered, *newOrdered;
satVariable_t *var;
ordered = cm->orderedVariableArray;
if(ordered == 0)
ordered = sat_ArrayAlloc(cm->initNumVariables);
else
ordered->num = 0;
cm->orderedVariableArray = ordered;
objExist = 0;
for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
v = i;
if((SATflags(v) & IsBDDMask)) {
continue;
}
if((SATflags(v) & IsCNFMask)) {
size = SATnumLits(v);
plit = (long*)SATfirstLit(v);
for(j=0; j<size; j++, plit++) {
nv = SATgetNode(*plit);
inverted = !(SATisInverted(nv));
nv = SATnormalNode(nv);
var = SATgetVariable(nv);
var->litsCount[inverted]++;
}
continue;
}
if(!(SATflags(v) & CoiMask)) continue;
if(!(SATflags(v) & VisitedMask) && objExist) continue;
if(SATvalue(v) != 2 && SATlevel(v) == 0) continue;
count0 = count1 = SATnFanout(v);
if(count0 == 0 && SATleftChild(v) == 2 && SATrightChild(v) == 2) {
count0 = 0;
count1 = 0;
}
else if(SATleftChild(v) != 2) {
count0 += 2;
count1++;
}
else {
count0 += 3;
count1 += 3;
}
var = SATgetVariable(v);
var->litsCount[0] += count0;
var->litsCount[1] += count1;
sat_ArrayInsert(ordered, v);
}
//Bing:
if(cm->unitLits){
for(i=0; i<cm->unitLits->num; i++) {
v = cm->unitLits->space[i];
v = SATnormalNode(v);
SATflags(v) |= NewMask;
}
}
if(cm->assertion) {
for(i=0; i<cm->assertion->num; i++) {
v = cm->assertion->space[i];
v = SATnormalNode(v);
SATflags(v) |= NewMask;
}
}
newOrdered = sat_ArrayAlloc((ordered->num) * 2);
size = ordered->num;
for(i=0; i<size; i++) {
v = ordered->space[i];
var = SATgetVariable(v);
var->scores[0] = var->lastLitsCount[0] = var->litsCount[0];
var->scores[1] = var->lastLitsCount[1] = var->litsCount[1];
if(SATflags(v) & NewMask);
else if(var->scores[0] == 0 && var->scores[1] == 0 && !(SATflags(v) & NewMask)) {
sat_ArrayInsert(cm->pureLits, (v));
}
else if(var->scores[0] == 0 && !(SATflags(v) & NewMask)) {
sat_ArrayInsert(cm->pureLits, (v));
}
else if(var->scores[1] == 0 && !(SATflags(v) & NewMask)) {
sat_ArrayInsert(cm->pureLits, SATnot(v));
}
else {
sat_ArrayInsert(newOrdered, v);
sat_ArrayInsert(newOrdered, (var->scores[0] > var->scores[1]) ? var->scores[0] : var->scores[1]);
}
}
//Bing:
if(cm->unitLits){
for(i=0; i<cm->unitLits->num; i++) {
v = cm->unitLits->space[i];
v = SATnormalNode(v);
SATflags(v) &= ResetNewMask;
}
}
if(cm->assertion) {
for(i=0; i<cm->assertion->num; i++) {
v = cm->assertion->space[i];
v = SATnormalNode(v);
SATflags(v) &= ResetNewMask;
}
}
cm->orderedVariableArray = ordered;
size = newOrdered->num;
qsort(newOrdered->space, size>>1, sizeof(long)*2, ScoreCompare);
cm->currentVarPos = 0;
ordered->num = 0;
for(i=0; i<size; i++) {
v = newOrdered->space[i];
var = SATgetVariable(v);
var->pos = (i>>1);
sat_ArrayInsert(ordered, v);
i++;
}
sat_ArrayFree(newOrdered);
if(cm->option->verbose > 3)
sat_PrintScore(cm);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_InitScoreForMixed | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [ Generate initial score for CNF and AIG ]
Description [ Generate initial score for CNF and AIG]
SideEffects []
SeeAlso []
objExist = 0; if(cm->obj && cm->obj->num) { sat_MarkTransitiveFaninForArray(cm, cm->obj, VisitedMask); objExist = 1; }
if(!(SATflags(v) & VisitedMask) && objExist) continue;
if(cm->obj && cm->obj->num) { sat_UnmarkTransitiveFaninForArray( cm, cm->obj, VisitedMask, ResetVisitedMask); }
Definition at line 793 of file satDecision.c.
{
int j, inverted;
long *plit, v, nv, i;
int size;
int count0, count1;
satArray_t *ordered, *newOrdered;
satVariable_t *var;
ordered = cm->orderedVariableArray;
if(ordered == 0)
ordered = sat_ArrayAlloc(cm->initNumVariables);
else
ordered->num = 0;
cm->orderedVariableArray = ordered;
for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
v = i;
if((SATflags(v) & IsBDDMask)) {
continue;
}
if((SATflags(v) & IsCNFMask)) {
size = SATnumLits(v);
plit =(long*) SATfirstLit(v);
for(j=0; j<size; j++, plit++) {
nv = SATgetNode(*plit);
inverted = !(SATisInverted(nv));
nv = SATnormalNode(nv);
var = SATgetVariable(nv);
var->litsCount[inverted]++;
}
continue;
}
if(!(SATflags(v) & CoiMask)) continue;
if(SATvalue(v) != 2 && SATlevel(v) == 0) continue;
count0 = count1 = SATnFanout(v);
if(count0 == 0 && SATleftChild(v) == 2 && SATrightChild(v) == 2) {
count0 = 0;
count1 = 0;
}
else if(SATleftChild(v) != 2) {
count0 += 2;
count1++;
}
else {
count0 += 3;
count1 += 3;
}
var = SATgetVariable(v);
var->litsCount[0] += count0;
var->litsCount[1] += count1;
sat_ArrayInsert(ordered, v);
}
for(i=0; i<cm->unitLits->num; i++) {
v = cm->unitLits->space[i];
v = SATnormalNode(v);
SATflags(v) |= NewMask;
}
if(cm->assertion) {
for(i=0; i<cm->assertion->num; i++) {
v = cm->assertion->space[i];
v = SATnormalNode(v);
SATflags(v) |= NewMask;
}
}
newOrdered = sat_ArrayAlloc((ordered->num) * 2);
size = ordered->num;
for(i=0; i<size; i++) {
v = ordered->space[i];
var = SATgetVariable(v);
var->scores[0] = var->lastLitsCount[0] = var->litsCount[0];
var->scores[1] = var->lastLitsCount[1] = var->litsCount[1];
if(SATflags(v) & NewMask);
else if(var->scores[0] == 0 && var->scores[1] == 0 && !(SATflags(v) & NewMask)) {
sat_ArrayInsert(cm->pureLits, (v));
}
else if(var->scores[0] == 0 && !(SATflags(v) & NewMask)) {
sat_ArrayInsert(cm->pureLits, (v));
}
else if(var->scores[1] == 0 && !(SATflags(v) & NewMask)) {
sat_ArrayInsert(cm->pureLits, SATnot(v));
}
else {
sat_ArrayInsert(newOrdered, v);
sat_ArrayInsert(newOrdered, (var->scores[0] > var->scores[1]) ? var->scores[0] : var->scores[1]);
}
}
for(i=0; i<cm->unitLits->num; i++) {
v = cm->unitLits->space[i];
v = SATnormalNode(v);
SATflags(v) &= ResetNewMask;
}
if(cm->assertion) {
for(i=0; i<cm->assertion->num; i++) {
v = cm->assertion->space[i];
v = SATnormalNode(v);
SATflags(v) &= ResetNewMask;
}
}
cm->orderedVariableArray = ordered;
size = newOrdered->num;
qsort(newOrdered->space, size>>1, sizeof(long)*2, ScoreCompare);
cm->currentVarPos = 0;
ordered->num = 0;
for(i=0; i<size; i++) {
v = newOrdered->space[i];
var = SATgetVariable(v);
var->pos = (i>>1);
sat_ArrayInsert(ordered, v);
i++;
}
sat_ArrayFree(newOrdered);
if(cm->option->verbose > 3)
sat_PrintScore(cm);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| satLevel_t* sat_MakeDecision | ( | satManager_t * | cm | ) |
AutomaticEnd Function********************************************************************
Synopsis [ Select decision variable]
Description [ Select decision variable]
SideEffects []
SeeAlso []
if(cm->option->verbose > 1) { var = SATgetVariable(v); fprintf(cm->stdOut, "decision at %3d on %6d <- %d score(%d %d) %d\n", d->level, v, value, var->scores[0], var->scores[1], cm->each->nDecisions); fflush(cm->stdOut); }
Definition at line 56 of file satDecision.c.
{
satLevel_t *d;
int value;
long v;
satStatistics_t *stats;
d = SATgetDecision(cm->currentDecision);
if(cm->queue->size)
return(d);
d = sat_AllocLevel(cm);
v = 0;
v = sat_DecisionBasedOnBDD(cm, d);
if(v == 0)
v = sat_DecisionBasedOnLatestConflict(cm, d);
if(v == 0)
v = sat_DecisionBasedOnScore(cm, d);
if(v == 0)
return(0);
stats = cm->each;
stats->nDecisions++;
value = !(SATisInverted(v));
v = SATnormalNode(v);
d->decisionNode = v;
d->nConflict = cm->each->nConflictCl;
SATvalue(v) = value;
SATmakeImplied(v, d);
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
return(d);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_UpdateDVH | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| satArray_t * | clauseArray, | ||
| int | bLevel, | ||
| long | unitLit | ||
| ) |
Function********************************************************************
Synopsis [ Update the score of variables by deepest variable hike]
Description [ Update the score of variables by deepest variable hike]
SideEffects []
SeeAlso []
CONSIDER ....
Definition at line 511 of file satDecision.c.
{
satArray_t *ordered;
satLevel_t *td;
satVariable_t *var, *tvar, *ttvar;
int score, tscore, ttscore;
int value;
long v;
int gap, i, insert;
ordered = cm->orderedVariableArray;
unitLit = SATnormalNode(unitLit);
gap = cm->currentDecision - bLevel;
td = SATgetDecision(bLevel+1);
if(gap <= 1) {
}
var = SATgetVariable(unitLit);
tvar = SATgetVariable(td->decisionNode);
score = (var->scores[1] > var->scores[0]) ? var->scores[1] : var->scores[0];
tscore = (tvar->scores[1] > tvar->scores[0]) ? tvar->scores[1] : tvar->scores[0];
if(score >= tscore) {
return;
}
tscore += 1;
value = SATvalue(unitLit);
if(value == 0)var->scores[1] = tscore;
else var->scores[0] = tscore;
ordered = cm->orderedVariableArray;
insert = 0;
for(i=var->pos; i>=1; i--) {
v = ordered->space[i-1];
ttvar = SATgetVariable(v);
ttscore = (ttvar->scores[1] > ttvar->scores[0]) ? ttvar->scores[1] : ttvar->scores[0];
if(tscore > ttscore && i>1) {
ttvar->pos = i;
ordered->space[i] = v;
continue;
}
var->pos = i;
ordered->space[i] = unitLit;
insert = 1;
break;
}
if(insert == 0) {
var->pos = i;
ordered->space[0] = unitLit;
}
for(i=d->level; i>0; i--) {
td = SATgetDecision(i);
if(td->currentVarPos < var->pos)
break;
td->currentVarPos = var->pos;
}
cm->currentVarPos = td->currentVarPos;
}
Here is the caller graph for this function:
| void sat_UpdateScore | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [ Update the score of variables ]
Description [ Update the score of variables ]
SideEffects []
SeeAlso []
Definition at line 423 of file satDecision.c.
{
satArray_t *one, *tmp;
satArray_t *ordered;
satVariable_t *var;
int size, i;
long v;
int value;
ordered = cm->orderedVariableArray;
one = sat_ArrayAlloc(ordered->num);
tmp = sat_ArrayAlloc(ordered->num);
size = ordered->num;
for(i=0; i<size; i++) {
v = ordered->space[i];
if(SATvalue(v) < 2 && SATlevel(v) == 0)
continue;
var = SATgetVariable(v);
var->scores[0] = (var->scores[0]>>1) + var->litsCount[0] - var->lastLitsCount[0];
var->scores[1] = (var->scores[1]>>1) + var->litsCount[1] - var->lastLitsCount[1];
var->lastLitsCount[0] = var->litsCount[0];
var->lastLitsCount[1] = var->litsCount[1];
if((var->scores[0] + var->scores[1]) < 1) {
sat_ArrayInsert(one, v);
}
else {
value = (var->scores[0] > var->scores[1]) ? var->scores[0] : var->scores[1];
sat_ArrayInsert(tmp, v);
sat_ArrayInsert(tmp, value);
}
}
SatCm = cm;
qsort(tmp->space, (tmp->num)>>1, sizeof(long)*2, ScoreCompare);
ordered->num = 0;
size = tmp->num;
for(i=0; i<size; i++) {
v = tmp->space[i];
sat_ArrayInsert(ordered, v);
var = SATgetVariable(v);
var->pos = (i>>1);
i++;
}
size = one->num;
for(i=0; i<size; i++) {
v = one->space[i];
var = SATgetVariable(v);
var->pos = ordered->num;
sat_ArrayInsert(ordered, v);
}
sat_ArrayFree(one);
sat_ArrayFree(tmp);
cm->orderedVariableArray = ordered;
cm->currentVarPos = 0;
for(i=1; i<cm->currentDecision; i++) {
cm->decisionHead[i].currentVarPos = 0;
}
if(cm->option->verbose > 3)
sat_PrintScore(cm);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int ScoreCompare | ( | const void * | node1, |
| const void * | node2 | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [ Compare score to sort variable array]
Description [ Compare score to sort variable array]
SideEffects []
SeeAlso []
var1 = SatCm->variableArray[SATnodeID(v1)]; var2 = SatCm->variableArray[SATnodeID(v2)]; s1 = (var1.scores[0] > var1.scores[1]) ? var1.scores[0] : var1.scores[1]; s2 = (var2.scores[0] > var2.scores[1]) ? var2.scores[0] : var2.scores[1];
Definition at line 952 of file satDecision.c.
{
int v1;
int v2;
int s1, s2;
v1 = *(int *)(node1);
v2 = *(int *)(node2);
s1 = *((int *)(node1) + 1);
s2 = *((int *)(node2) + 1);
if(s1 == s2) {
return(v1 > v2);
}
return(s1 < s2);
}
Here is the caller graph for this function:
Variable Documentation
satManager_t* SatCm [static] |
Definition at line 22 of file satDecision.c.
char rcsid [] UNUSED = "$Id: satDecision.c,v 1.28 2009/04/11 18:26:37 fabio Exp $" [static] |
CFile***********************************************************************
FileName [satDecision.c]
PackageName [sat]
Synopsis [Routines for various decision heuristics.]
Author [HoonSang Jin]
Copyright [ This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]
Definition at line 21 of file satDecision.c.
