#include "satInt.h"#include "puresatInt.h"
Include dependency graph for satConflict.c:
Go to the source code of this file.
Functions | |
| static int | levelCompare (const void *node1, const void *node2) |
| int | sat_ConflictAnalysis (satManager_t *cm, satLevel_t *d) |
| int | sat_ConflictAnalysisForLifting (satManager_t *cm, satLevel_t *d) |
| int | sat_ConflictAnalysisWithBlockingClause (satManager_t *cm, satLevel_t *d) |
| int | sat_StrongConflictAnalysis (satManager_t *cm, satLevel_t *d) |
| int | sat_AddConflictClauseAndBacktrack (satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, long fdaLit, int bLevel, int objectFlag, int strongFlag) |
| int | sat_AddConflictClauseAndBacktrackForLifting (satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, long fdaLit, int bLevel, int objectFlag, int strongFlag) |
| int | sat_AddConflictClauseWithNoScoreAndBacktrack (satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, long fdaLit, int bLevel, int objectFlag, int strongFlag) |
| int | sat_ConflictAnalysisUsingAuxImplication (satManager_t *cm, satArray_t *clauseArray) |
| int | sat_ConflictAnalysisForCoreGen (satManager_t *cm, satLevel_t *d) |
| void | sat_FindUIP (satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, int *objectFlag, int *bLevel, long *fdaLit) |
| void | sat_FindUIPWithRT (satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, int *objectFlag, int *bLevel, long *fdaLit) |
| void | sat_FindUIPAndNonUIP (satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, int *objectFlag, int *bLevel, long *fdaLit) |
| void | sat_FindUIPForCoreGen (satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, int *objectFlag, int *bLevel, long *fdaLit) |
| void | sat_FindUIPForCoreGenWithRT (satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, int *objectFlag, int *bLevel, long *fdaLit) |
| void | sat_MinimizeConflictClause (satManager_t *cm, satArray_t *clauseArray) |
| void | sat_ResetFlagForClauseArray (satManager_t *cm, satArray_t *clauseArray) |
| void | sat_MarkNodeInConflict (satManager_t *cm, satLevel_t *d, int *nMarked, int *objectFlag, int *bLevel, satArray_t *clauseArray) |
| void | sat_MarkNodeInImpliedNode (satManager_t *cm, satLevel_t *d, long v, int *nMarked, int *objectFlag, int *bLevel, satArray_t *clauseArray) |
| void | sat_MarkNodeSub (satManager_t *cm, long v, int *nMarked, int *bLevel, satLevel_t *d, satArray_t *clauseArray) |
| void | sat_MarkNodeInImpliedNodeNoObj (satManager_t *cm, satLevel_t *d, long v, int *nMarked, int *oFlag, int *bLevel, satArray_t *clauseArray) |
| void | sat_MarkNodeInImpliedNodeObjConservative (satManager_t *cm, satLevel_t *d, long v, int *nMarked, int *oFlag, int *bLevel, satArray_t *clauseArray) |
| void | sat_MarkNodeInConflictClauseNoObj (satManager_t *cm, satLevel_t *d, int *nMarked, int *oFlag, int *bLevel, satArray_t *clauseArray) |
| void | sat_MarkNodeInConflictClauseObjConservative (satManager_t *cm, satLevel_t *d, int *nMarked, int *oFlag, int *bLevel, satArray_t *clauseArray) |
| void | sat_Backtrack (satManager_t *cm, int level) |
| void | sat_Undo (satManager_t *cm, satLevel_t *d) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: satConflict.c,v 1.31 2009/04/11 18:26:37 fabio Exp $" |
| static satManager_t * | SATcm |
Function Documentation
| static int levelCompare | ( | const void * | node1, |
| const void * | node2 | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [ Compare decision level of variable ]
Description [ Compare decision level of variable ]
SideEffects []
SeeAlso []
Definition at line 2619 of file satConflict.c.
{
long v1, v2;
int l1, l2;
v1 = *(int *)(node1);
v2 = *(int *)(node2);
l1 = SATcm->variableArray[SATnodeID(v1)].level;
l2 = SATcm->variableArray[SATnodeID(v2)].level;
if(l1 == l2) return(v1 > v2);
return (l1 > l2);
}
Here is the caller graph for this function:
| int sat_AddConflictClauseAndBacktrack | ( | satManager_t * | cm, |
| satArray_t * | clauseArray, | ||
| satLevel_t * | d, | ||
| long | fdaLit, | ||
| int | bLevel, | ||
| int | objectFlag, | ||
| int | strongFlag | ||
| ) |
Function********************************************************************
Synopsis [ Add conflict clause and backtrack.]
Description [ Add conflict clause and backtrack.]
SideEffects []
SeeAlso []
Definition at line 371 of file satConflict.c.
{
int inverted;
long conflicting, learned;
satOption_t *option;
satStatistics_t *stats;
satArray_t *nClauseArray;
RTManager_t * rm = cm->rm;
option = cm->option;
stats = cm->each;
inverted = SATisInverted(fdaLit);
fdaLit = SATnormalNode(fdaLit);
conflicting = d->conflict;
if(option->verbose > 2) {
if(option->verbose > 4)
sat_PrintNode(cm, conflicting);
fprintf(cm->stdOut, "conflict at %3d on %6ld bLevel %d UnitLit ",
d->level, conflicting, bLevel);
sat_PrintNodeAlone(cm, fdaLit);
fprintf(cm->stdOut, "\n");
}
d->conflict = 0;
/* unit literal conflict clause */
if(clauseArray->num == 1) {
learned = sat_AddUnitConflictClause(cm, clauseArray, objectFlag);
stats->nUnitConflictCl++;
cm->currentTopConflict = cm->literals->last-1;
cm->currentTopConflictCount = 0;
sat_Backtrack(cm, 0);
if(SATlevel(fdaLit) == 0) {
if(cm->option->coreGeneration){
if(cm->option->RT){
st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
st_insert(cm->RTreeTable, (char *)learned, (char *)rm->root);
RT_oriClsIdx(rm->root) = learned;
}
else{
st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
}
}
cm->currentDecision = -1;
return (-1);
}
d = SATgetDecision(cm->currentDecision);
cm->implicatedSoFar -= d->implied->num;
SATante(fdaLit) = 0;
SATvalue(fdaLit) = inverted;
SATmakeImplied(fdaLit, d);
if((SATflags(fdaLit) & InQueueMask) == 0) {
sat_Enqueue(cm->queue, fdaLit);
SATflags(fdaLit) |= InQueueMask;
}
clauseArray->num = 0;
if(option->incTraceObjective && objectFlag == 0)
sat_ArrayInsert(cm->nonobjUnitLitArray, SATnot(fdaLit));
if(option->incDistill && objectFlag)
sat_ArrayInsert(cm->objUnitLitArray, SATnot(fdaLit));
if(objectFlag)
SATflags(fdaLit) |= ObjMask;
/* Bing: UNSAT core generation */
if(cm->option->coreGeneration){
if(cm->option->RT){
st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
st_insert(cm->RTreeTable, (char *)learned, (char *)rm->root);
RT_oriClsIdx(rm->root) = learned;
}
else{
st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
}
}
return(bLevel);
}
if(strongFlag && (SATnumConflict(conflicting) % 5) == 0 &&
clauseArray->num > 4) {
nClauseArray = sat_ArrayAlloc(clauseArray->num);
memcpy(nClauseArray->space, clauseArray->space, sizeof(long)*clauseArray->num);
nClauseArray->num = clauseArray->num;
clauseArray->num = 0;
bLevel = sat_ConflictAnalysisUsingAuxImplication(cm, nClauseArray);
sat_ArrayFree(nClauseArray);
}
else {
/* add conflict learned clause */
learned = sat_AddConflictClause(cm, clauseArray, objectFlag);
cm->currentTopConflict = cm->literals->last-1;
cm->currentTopConflictCount = 0;
/* Bing: UNSAT core generation */
if(cm->option->coreGeneration){
if(cm->option->RT){
st_insert(cm->RTreeTable, (char *)learned, (char *)rm->root);
RT_oriClsIdx(rm->root) = learned;
}
else{
st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
}
}
if(option->verbose > 2) {
sat_PrintNode(cm, learned);
fflush(cm->stdOut);
}
/* apply Deepest Variable Hike decision heuristic */
if(option->decisionHeuristic & DVH_DECISION)
sat_UpdateDVH(cm, d, clauseArray, bLevel, fdaLit);
/* Backtrack and failure driven assertion */
sat_Backtrack(cm, bLevel);
d = SATgetDecision(bLevel);
cm->implicatedSoFar -= d->implied->num;
SATante(fdaLit) = learned;
SATvalue(fdaLit) = inverted;
SATmakeImplied(fdaLit, d);
if((SATflags(fdaLit) & InQueueMask) == 0) {
sat_Enqueue(cm->queue, fdaLit);
SATflags(fdaLit) |= InQueueMask;
}
clauseArray->num = 0;
if(objectFlag)
SATflags(fdaLit) |= ObjMask;
}
return(bLevel);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int sat_AddConflictClauseAndBacktrackForLifting | ( | satManager_t * | cm, |
| satArray_t * | clauseArray, | ||
| satLevel_t * | d, | ||
| long | fdaLit, | ||
| int | bLevel, | ||
| int | objectFlag, | ||
| int | strongFlag | ||
| ) |
Function********************************************************************
Synopsis [ Add conflict clause and backtrack.]
Description [ Add conflict clause and backtrack.]
SideEffects []
SeeAlso []
if(option->decisionHeuristic & DVH_DECISION) sat_UpdateDVH(cm, d, clauseArray, bLevel, fdaLit);
Definition at line 545 of file satConflict.c.
{
int inverted;
long conflicting, learned;
satOption_t *option;
satStatistics_t *stats;
satArray_t *nClauseArray;
option = cm->option;
stats = cm->each;
inverted = SATisInverted(fdaLit);
fdaLit = SATnormalNode(fdaLit);
conflicting = d->conflict;
if(option->verbose > 2) {
if(option->verbose > 4)
sat_PrintNode(cm, conflicting);
fprintf(cm->stdOut, "conflict at %3d on %6ld bLevel %d UnitLit ",
d->level, conflicting, bLevel);
sat_PrintNodeAlone(cm, fdaLit);
fprintf(cm->stdOut, "\n");
}
d->conflict = 0;
/* unit literal conflict clause */
if(clauseArray->num == 1) {
learned = sat_AddUnitConflictClause(cm, clauseArray, objectFlag);
stats->nUnitConflictCl++;
cm->currentTopConflict = cm->literals->last-1;
cm->currentTopConflictCount = 0;
sat_Backtrack(cm, 0);
if(SATlevel(fdaLit) == 0) {
if(cm->option->coreGeneration){
st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
}
cm->currentDecision = -1;
return (-1);
}
d = SATgetDecision(cm->currentDecision);
cm->implicatedSoFar -= d->implied->num;
SATante(fdaLit) = 0;
SATvalue(fdaLit) = inverted;
SATmakeImplied(fdaLit, d);
if((SATflags(fdaLit) & InQueueMask) == 0) {
sat_Enqueue(cm->queue, fdaLit);
SATflags(fdaLit) |= InQueueMask;
}
clauseArray->num = 0;
if(option->incTraceObjective && objectFlag == 0)
sat_ArrayInsert(cm->nonobjUnitLitArray, SATnot(fdaLit));
if(option->incDistill && objectFlag)
sat_ArrayInsert(cm->objUnitLitArray, SATnot(fdaLit));
if(objectFlag)
SATflags(fdaLit) |= ObjMask;
/* Bing: UNSAT core generation */
if(cm->option->coreGeneration){
st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
}
return(0);
}
if(strongFlag && (SATnumConflict(conflicting) % 5) == 0 &&
clauseArray->num > 4) {
nClauseArray = sat_ArrayAlloc(clauseArray->num);
memcpy(nClauseArray->space, clauseArray->space, sizeof(long)*clauseArray->num);
nClauseArray->num = clauseArray->num;
clauseArray->num = 0;
bLevel = sat_ConflictAnalysisUsingAuxImplication(cm, nClauseArray);
sat_ArrayFree(nClauseArray);
}
else {
/* add conflict learned clause */
learned = sat_AddConflictClause(cm, clauseArray, objectFlag);
cm->currentTopConflict = cm->literals->last-1;
cm->currentTopConflictCount = 0;
/* Bing: UNSAT core generation */
if(cm->option->coreGeneration){
st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
}
if(option->verbose > 2) {
sat_PrintNode(cm, learned);
fflush(cm->stdOut);
}
/* apply Deepest Variable Hike decision heuristic */
/* Backtrack and failure driven assertion */
sat_Backtrack(cm, bLevel);
d = SATgetDecision(bLevel);
cm->implicatedSoFar -= d->implied->num;
SATante(fdaLit) = learned;
SATvalue(fdaLit) = inverted;
SATmakeImplied(fdaLit, d);
if((SATflags(fdaLit) & InQueueMask) == 0) {
sat_Enqueue(cm->queue, fdaLit);
SATflags(fdaLit) |= InQueueMask;
}
clauseArray->num = 0;
if(objectFlag)
SATflags(fdaLit) |= ObjMask;
}
return(bLevel);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int sat_AddConflictClauseWithNoScoreAndBacktrack | ( | satManager_t * | cm, |
| satArray_t * | clauseArray, | ||
| satLevel_t * | d, | ||
| long | fdaLit, | ||
| int | bLevel, | ||
| int | objectFlag, | ||
| int | strongFlag | ||
| ) |
Function********************************************************************
Synopsis [ Add conflict clause with no score update and backtrack.]
Description [ Add conflict clause with no score update and backtrack.]
SideEffects []
SeeAlso []
Definition at line 696 of file satConflict.c.
{
int inverted;
long conflicting, learned;
satOption_t *option;
satStatistics_t *stats;
satArray_t *nClauseArray;
option = cm->option;
stats = cm->each;
inverted = SATisInverted(fdaLit);
fdaLit = SATnormalNode(fdaLit);
conflicting = d->conflict;
if(option->verbose > 2) {
if(option->verbose > 4)
sat_PrintNode(cm, conflicting);
fprintf(cm->stdOut, "conflict at %3d on %6ld bLevel %d UnitLit ",
d->level, conflicting, bLevel);
sat_PrintNodeAlone(cm, fdaLit);
fprintf(cm->stdOut, "\n");
}
d->conflict = 0;
/* unit literal conflict clause */
if(clauseArray->num == 1) {
learned = sat_AddUnitConflictClause(cm, clauseArray, objectFlag);
stats->nUnitConflictCl++;
cm->currentTopConflict = cm->literals->last-1;
cm->currentTopConflictCount = 0;
sat_Backtrack(cm, 0);
if(SATlevel(fdaLit) == 0) {
if(cm->option->coreGeneration){
st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
}
cm->currentDecision = -1;
return (-1);
}
d = SATgetDecision(cm->currentDecision);
cm->implicatedSoFar -= d->implied->num;
SATante(fdaLit) = 0;
SATvalue(fdaLit) = inverted;
SATmakeImplied(fdaLit, d);
if((SATflags(fdaLit) & InQueueMask) == 0) {
sat_Enqueue(cm->queue, fdaLit);
SATflags(fdaLit) |= InQueueMask;
}
clauseArray->num = 0;
if(option->incTraceObjective && objectFlag == 0)
sat_ArrayInsert(cm->nonobjUnitLitArray, SATnot(fdaLit));
if(option->incDistill && objectFlag)
sat_ArrayInsert(cm->objUnitLitArray, SATnot(fdaLit));
if(objectFlag)
SATflags(fdaLit) |= ObjMask;
/* Bing: UNSAT core generation */
if(cm->option->coreGeneration){
st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
}
return(bLevel);
}
if(strongFlag && (SATnumConflict(conflicting) % 5) == 0 &&
clauseArray->num > 4) {
nClauseArray = sat_ArrayAlloc(clauseArray->num);
memcpy(nClauseArray->space, clauseArray->space, sizeof(long)*clauseArray->num);
nClauseArray->num = clauseArray->num;
clauseArray->num = 0;
bLevel = sat_ConflictAnalysisUsingAuxImplication(cm, nClauseArray);
sat_ArrayFree(nClauseArray);
}
else {
/* add conflict learned clause */
learned = sat_AddConflictClauseNoScoreUpdate(cm, clauseArray, objectFlag);
cm->currentTopConflict = cm->literals->last-1;
cm->currentTopConflictCount = 0;
/* Bing: UNSAT core generation */
if(cm->option->coreGeneration){
st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
}
if(option->verbose > 2) {
sat_PrintNode(cm, learned);
fflush(cm->stdOut);
}
/* apply Deepest Variable Hike decision heuristic */
if(option->decisionHeuristic & DVH_DECISION)
sat_UpdateDVH(cm, d, clauseArray, bLevel, fdaLit);
/* Backtrack and failure driven assertion */
sat_Backtrack(cm, bLevel);
d = SATgetDecision(bLevel);
cm->implicatedSoFar -= d->implied->num;
SATante(fdaLit) = learned;
SATvalue(fdaLit) = inverted;
SATmakeImplied(fdaLit, d);
if((SATflags(fdaLit) & InQueueMask) == 0) {
sat_Enqueue(cm->queue, fdaLit);
SATflags(fdaLit) |= InQueueMask;
}
clauseArray->num = 0;
if(objectFlag)
SATflags(fdaLit) |= ObjMask;
}
return(bLevel);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_Backtrack | ( | satManager_t * | cm, |
| int | level | ||
| ) |
Function********************************************************************
Synopsis [ Backtrack to given decision level ]
Description [ Backtrack to given decision level ]
SideEffects []
SeeAlso []
Definition at line 2518 of file satConflict.c.
{
satLevel_t *d;
/*Bing*/
if(cm->option->ForceFinish == 0)
if(level < 0) return;
d = SATgetDecision(cm->currentDecision);
while(1) {
if(d->level <= level)
break;
sat_Undo(cm, d);
cm->currentDecision--;
if(cm->currentDecision == -1)
break;
d = SATgetDecision(cm->currentDecision);
}
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int sat_ConflictAnalysis | ( | satManager_t * | cm, |
| satLevel_t * | d | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [ Conflict Analysis]
Description [ Conflict Analysis]
SideEffects []
SeeAlso []
Bing : UNSAT core generation
Definition at line 60 of file satConflict.c.
{
satStatistics_t *stats;
satOption_t *option;
satArray_t *clauseArray;
int objectFlag;
int bLevel;
long fdaLit, conflicting;
conflicting = d->conflict;
if(d->level == 0) {
if(cm->option->coreGeneration)
sat_ConflictAnalysisForCoreGen(cm, d);
cm->currentDecision--;
return (-1);
}
stats = cm->each;
option = cm->option;
stats->nBacktracks++;
clauseArray = cm->auxArray;
bLevel = 0;
fdaLit = -1;
clauseArray->num = 0;
/* Find Unique Implication Point */
if(option->RT)
sat_FindUIPWithRT(cm, clauseArray, d, &objectFlag, &bLevel, &fdaLit);
else
sat_FindUIP(cm, clauseArray, d, &objectFlag, &bLevel, &fdaLit);
stats->nNonchonologicalBacktracks += (d->level - bLevel);
if(clauseArray->num == 0) {
sat_PrintImplicationGraph(cm, d);
sat_PrintNode(cm, conflicting);
}
/* If we could find UIP then it is critical error...
* at lease the decision node has to be detected as UIP.
*/
if(fdaLit == -1) {
fprintf(cm->stdOut, "%s ERROR : Illegal unit literal\n", cm->comment);
fflush(cm->stdOut);
sat_PrintNode(cm, conflicting);
sat_PrintImplicationGraph(cm, d);
sat_PrintDotForConflict(cm, d, conflicting, 0);
exit(0);
}
if(bLevel && cm->lowestBacktrackLevel > bLevel)
cm->lowestBacktrackLevel = bLevel;
bLevel = sat_AddConflictClauseAndBacktrack(
cm, clauseArray, d, fdaLit, bLevel, objectFlag, 0);
return(bLevel);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int sat_ConflictAnalysisForCoreGen | ( | satManager_t * | cm, |
| satLevel_t * | d | ||
| ) |
Function********************************************************************
Synopsis [ Conflict Analysis that is used for UNSAT core generation.]
Description [ Conflict Analysis that is used for UNSAT core generation.]
SideEffects []
SeeAlso []
Definition at line 962 of file satConflict.c.
{
satStatistics_t *stats;
satOption_t *option;
satArray_t *clauseArray;
int objectFlag;
int bLevel;
long fdaLit, learned, conflicting;
int inverted;
RTManager_t * rm = cm->rm;
if(d->level != 0) {
fprintf(stdout, "ERROR : Can't use this function at higher than level 0\n");
return(0);
}
conflicting = d->conflict;
stats = cm->each;
option = cm->option;
stats->nBacktracks++;
clauseArray = cm->auxArray;
bLevel = 0;
fdaLit = -1;
clauseArray->num = 0;
/* Find Unique Implication Point */
if(option->RT)
sat_FindUIPForCoreGenWithRT(cm, clauseArray, d, &objectFlag, &bLevel,&fdaLit);
else
sat_FindUIPForCoreGen(cm, clauseArray, d, &objectFlag, &bLevel, &fdaLit);
if(fdaLit < 0 )
fprintf(stdout, "ERROR : critical\n");
inverted = SATisInverted(fdaLit);
fdaLit = SATnormalNode(fdaLit);
d->conflict = 0;
assert(clauseArray->num == 1);
learned = sat_AddUnitConflictClause(cm, clauseArray, objectFlag);
SATante(fdaLit) = 0;
clauseArray->num = 0;
/* Bing: UNSAT core generation */
if(cm->option->coreGeneration){
st_insert(cm->anteTable,(char*)(long)SATnormalNode(fdaLit),(char*)(long)learned);
if(option->RT){
st_insert(cm->RTreeTable, (char *)learned, (char *)rm->root);
RT_oriClsIdx(rm->root) = learned;
}
else
st_insert(cm->dependenceTable, (char *)(long)learned, (char *)(long)cm->dependenceArray);
}
return 1;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int sat_ConflictAnalysisForLifting | ( | satManager_t * | cm, |
| satLevel_t * | d | ||
| ) |
Function********************************************************************
Synopsis [ Conflict Analysis for lifting instance]
Description [ Conflict Analysis for lifting instance]
SideEffects []
SeeAlso []
Definition at line 142 of file satConflict.c.
{
satStatistics_t *stats;
satOption_t *option;
satArray_t *clauseArray;
int objectFlag;
int bLevel;
long fdaLit, conflicting;
conflicting = d->conflict;
if(d->level == 0) {
cm->currentDecision--;
return (-1);
}
stats = cm->each;
option = cm->option;
stats->nBacktracks++;
clauseArray = cm->auxArray;
bLevel = 0;
fdaLit = -1;
clauseArray->num = 0;
/* Find Unique Implication Point */
sat_FindUIP(cm, clauseArray, d, &objectFlag, &bLevel, &fdaLit);
stats->nNonchonologicalBacktracks += (d->level - bLevel);
if(clauseArray->num == 0) {
sat_PrintImplicationGraph(cm, d);
sat_PrintNode(cm, conflicting);
}
/* If we could find UIP then it is critical error...
* at lease the decision node has to be detected as UIP.
*/
if(fdaLit == -1) {
fprintf(cm->stdOut, "%s ERROR : Illegal unit literal\n", cm->comment);
fflush(cm->stdOut);
sat_PrintNode(cm, conflicting);
sat_PrintImplicationGraph(cm, d);
sat_PrintDotForConflict(cm, d, conflicting, 0);
exit(0);
}
if(bLevel && cm->lowestBacktrackLevel > bLevel)
cm->lowestBacktrackLevel = bLevel;
bLevel = sat_AddConflictClauseAndBacktrackForLifting(
cm, clauseArray, d, fdaLit, bLevel, objectFlag, 0);
return(bLevel);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int sat_ConflictAnalysisUsingAuxImplication | ( | satManager_t * | cm, |
| satArray_t * | clauseArray | ||
| ) |
Function********************************************************************
Synopsis [ Minimize conflict clause by rebuilding implication graph.]
Description [ Minimize conflict clause by rebuilding implication graph.]
SideEffects []
SeeAlso []
if(tvalue != value) { fprintf(stdout, "ERROR : Inconsitent value is implied\n"); sat_ReportStatistics(cm, cm->each); }
fprintf(stdout, "tLevel %d gLevel %.1lf %ld -> %ld min %d max %d\n", tLevel, gMean, clauseArray->num, nClauseArray->num, minConflict, maxConflict);
Definition at line 845 of file satConflict.c.
{
int tLevel, level, bLevel;
int i, size;
int value, tvalue;
int minConflict, maxConflict;
long v, tv, conflicting;
satLevel_t *d;
satArray_t *nClauseArray;
double aMean, hMean, gMean;
int objectFlag;
long fdaLit;
SATcm = cm;
qsort(clauseArray->space, clauseArray->num, sizeof(int), levelCompare);
tLevel = cm->currentDecision;
tv = clauseArray->space[0];
v = SATnormalNode(tv);
level = SATlevel(v);
minConflict = cm->decisionHead[level].nConflict;
tv = clauseArray->space[clauseArray->num-1];
v = SATnormalNode(tv);
level = SATlevel(v);
maxConflict = cm->decisionHead[level].nConflict;
aMean = hMean = 0;
for(i=0; i<clauseArray->num; i++) {
tv = clauseArray->space[i];
v = SATnormalNode(tv);
level = SATlevel(v);
if(level < tLevel) tLevel = level;
aMean = aMean + (double)level;
hMean = hMean + 1.0/(double)level;
}
aMean = aMean/(double)clauseArray->num;
hMean = (double)clauseArray->num/hMean;
gMean = sqrt(aMean*hMean);
sat_Backtrack(cm, tLevel-1);
size = clauseArray->num;
for(i=0; i<size; i++) {
tv = clauseArray->space[i];
value = !SATisInverted(tv);
v = SATnormalNode(tv);
tvalue = SATvalue(v);
if(tvalue != 2) {
continue;
}
d = sat_AllocLevel(cm);
SATvalue(v) = value;
SATmakeImplied(v, d);
d->decisionNode = v;
d->nConflict = cm->each->nConflictCl;
if((SATflags(v) & InQueueMask) == 0) {
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
}
sat_ImplicationMain(cm, d);
if(d->conflict) {
conflicting = d->conflict;
break;
}
}
if(d->conflict) {
nClauseArray = cm->auxArray;
bLevel = 0;
fdaLit = -1;
nClauseArray->num = 0;
sat_FindUIP(cm, nClauseArray, d, &objectFlag, &bLevel, &fdaLit);
bLevel = sat_AddConflictClauseAndBacktrack(
cm, nClauseArray, d, fdaLit, bLevel, objectFlag, 0);
}
else {
bLevel = cm->currentDecision;
}
return(bLevel);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int sat_ConflictAnalysisWithBlockingClause | ( | satManager_t * | cm, |
| satLevel_t * | d | ||
| ) |
Function********************************************************************
Synopsis [ Conflict Analysis on blocking clause]
Description [ Conflict Analysis on blocking clause]
SideEffects []
SeeAlso []
Definition at line 216 of file satConflict.c.
{
satStatistics_t *stats;
satOption_t *option;
satArray_t *clauseArray;
int objectFlag;
int bLevel;
long fdaLit, conflicting;
conflicting = d->conflict;
if(d->level == 0) {
cm->currentDecision--;
return (-1);
}
stats = cm->each;
option = cm->option;
stats->nBacktracks++;
clauseArray = cm->auxArray;
bLevel = 0;
fdaLit = -1;
clauseArray->num = 0;
/* Find Unique Implication Point */
sat_FindUIP(cm, clauseArray, d, &objectFlag, &bLevel, &fdaLit);
stats->nNonchonologicalBacktracks += (d->level - bLevel);
if(clauseArray->num == 0) {
sat_PrintImplicationGraph(cm, d);
sat_PrintNode(cm, conflicting);
}
/* If we could find UIP then it is critical error...
* at lease the decision node has to be detected as UIP.
*/
if(fdaLit == -1) {
fprintf(cm->stdOut, "%s ERROR : Illegal unit literal\n", cm->comment);
fflush(cm->stdOut);
sat_PrintNode(cm, conflicting);
sat_PrintImplicationGraph(cm, d);
sat_PrintDotForConflict(cm, d, conflicting, 0);
exit(0);
}
if(bLevel && cm->lowestBacktrackLevel > bLevel)
cm->lowestBacktrackLevel = bLevel;
bLevel = sat_AddConflictClauseWithNoScoreAndBacktrack(
cm, clauseArray, d, fdaLit, bLevel, objectFlag, 0);
return(bLevel);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_FindUIP | ( | satManager_t * | cm, |
| satArray_t * | clauseArray, | ||
| satLevel_t * | d, | ||
| int * | objectFlag, | ||
| int * | bLevel, | ||
| long * | fdaLit | ||
| ) |
Function********************************************************************
Synopsis [ Find Unique implication point]
Description [ After finding unique implication point, the backtrack level and failure driven assertion are identified. ]
SideEffects []
SeeAlso []
Definition at line 1042 of file satConflict.c.
{
long conflicting;
int nMarked, value;
int first, i;
long *space, v;
satArray_t *implied;
satOption_t *option;
conflicting = d->conflict;
nMarked = 0;
option = cm->option;
if(option->incTraceObjective) *objectFlag = 0;
else *objectFlag = ObjMask;
(*objectFlag) |= (SATflags(conflicting) & ObjMask);
/* find seed from conflicting clause to find unique implication point.
* */
clauseArray->num = 0;
if(SATflags(conflicting) & IsCNFMask)
SATconflictUsage(conflicting)++;
sat_MarkNodeInConflict(
cm, d, &nMarked, objectFlag, bLevel, clauseArray);
/* Traverse implication graph backward */
first = 1;
implied = d->implied;
space = implied->space+implied->num-1;
/* Bing: UNSAT core generation */
if(cm->option->coreGeneration){
cm->dependenceArray = sat_ArrayAlloc(1);
sat_ArrayInsert(cm->dependenceArray,conflicting);
}
for(i=implied->num-1; i>=0; i--, space--) {
v = *space;
if(SATflags(v) & VisitedMask) {
SATflags(v) &= ResetVisitedMask;
--nMarked;
if(nMarked == 0 && (!first || i==0)) {
value = SATvalue(v);
*fdaLit = v^(!value);
sat_ArrayInsert(clauseArray, *fdaLit);
break;
}
/* Bing: UNSAT core genration */
if(cm->option->coreGeneration){
int ante = SATante(v);
if(ante!=0 && !(SATflags(ante) & IsCNFMask)){
printf("node %d is not CNF\n", ante);
exit(0);
}
if(ante==0){
if(!st_lookup(cm->anteTable, (char *)SATnormalNode(v), &ante)){
printf("ante = 0 and is not in anteTable %ld\n",v);
exit(0);
}
}
sat_ArrayInsert(cm->dependenceArray,ante);
}
sat_MarkNodeInImpliedNode(
cm, d, v, &nMarked, objectFlag, bLevel, clauseArray);
}
first = 0;
}
/* Minimize conflict clause */
if(option->minimizeConflictClause)
sat_MinimizeConflictClause(cm, clauseArray);
else
sat_ResetFlagForClauseArray(cm, clauseArray);
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_FindUIPAndNonUIP | ( | satManager_t * | cm, |
| satArray_t * | clauseArray, | ||
| satLevel_t * | d, | ||
| int * | objectFlag, | ||
| int * | bLevel, | ||
| long * | fdaLit | ||
| ) |
Function********************************************************************
Synopsis [ Find Unique implication point and find cut to generate additional conflict clause]
Description [ After finding unique implication point, the backtrack level and failure driven assertion are identified. ]
SideEffects []
SeeAlso []
HSJIN : Need to be update to make it consider UNSAT core generation
sat_MarkNodeInImpliedNode( cm, d, v, &nMarked, objectFlag, bLevel, clauseArray);
HSJIN : depth, lBacktrace and uBacktrace may affect to performance
Definition at line 1373 of file satConflict.c.
{
long conflicting;
int nMarked, value;
int first, i, j;
int size, oSize;
int depth, maxSize;
long *space, v, nv, maxV;
long ante, ante2;
long learned;
long *plit;
satArray_t *implied;
satArray_t *nClauseArray;
satOption_t *option;
int tLevel, inverted, lBacktrace, uBacktrace;
int minLimit, markLimit, tObjectFlag;
int inserted;
long tFdaLit;
conflicting = d->conflict;
nMarked = 0;
option = cm->option;
if(option->incTraceObjective) *objectFlag = 0;
else *objectFlag = ObjMask;
(*objectFlag) |= (SATflags(conflicting) & ObjMask);
/* find seed from conflicting clause to find unique implication point.
* */
clauseArray->num = 0;
if(SATflags(conflicting) & IsCNFMask)
SATconflictUsage(conflicting)++;
sat_MarkNodeInConflict(
cm, d, &nMarked, objectFlag, bLevel, clauseArray);
/* Traverse implication graph backward */
first = 1;
implied = d->implied;
space = implied->space+implied->num-1;
maxSize = 0;
maxV = 0;
/* Bing: UNSAT core generation */
if(cm->option->coreGeneration){
cm->dependenceArray = sat_ArrayAlloc(1);
sat_ArrayInsert(cm->dependenceArray,conflicting);
}
for(i=implied->num-1; i>=0; i--, space--) {
v = *space;
if(SATflags(v) & VisitedMask) {
SATflags(v) &= ResetVisitedMask;
--nMarked;
depth = cm->variableArray[SATnodeID(v)].depth;
if(nMarked == 0 && (!first || i==0)) {
value = SATvalue(v);
*fdaLit = v^(!value);
sat_ArrayInsert(clauseArray, *fdaLit);
break;
}
ante = SATante(v);
/* Bing: UNSAT core genration */
if(cm->option->coreGeneration){
if(ante!=0 && !(SATflags(ante) & IsCNFMask)){
printf("node %ld is not CNF\n", ante);
exit(0);
}
if(ante==0){
if(!st_lookup(cm->anteTable, (char *)SATnormalNode(v), &ante)){
printf("ante = 0 and is not in anteTable %ld\n",v);
exit(0);
}
}
sat_ArrayInsert(cm->dependenceArray,ante);
}
if(SATflags(ante) & IsCNFMask) {
SATconflictUsage(ante)++;
size = SATnumLits(ante);
oSize = clauseArray->num;
for(j=0, plit=(long*)SATfirstLit(ante); j<size; j++, plit++) {
nv = SATgetNode(*plit);
if(SATnormalNode(nv) != v) {
sat_MarkNodeSub(cm, nv, &nMarked, bLevel, d, clauseArray);
if(cm->variableArray[SATnodeID(nv)].depth <= depth) {
cm->variableArray[SATnodeID(nv)].depth = depth+1;
}
}
}
oSize = clauseArray->num-oSize;
if(oSize > maxSize) {
maxSize = oSize;
maxV = v;
}
}
else {
sat_MarkNodeSub(cm, ante, &nMarked, bLevel, d, clauseArray);
ante2 = SATante2(v);
if(ante2)
sat_MarkNodeSub(cm, ante2, &nMarked, bLevel, d, clauseArray);
}
}
first = 0;
}
/* Minimize conflict clause */
if(option->minimizeConflictClause)
sat_MinimizeConflictClause(cm, clauseArray);
else
sat_ResetFlagForClauseArray(cm, clauseArray);
if(maxSize > clauseArray->num/4 && maxSize > 5) {
nClauseArray = sat_ArrayAlloc(clauseArray->num);
nMarked = 0;
tLevel = 0;
tObjectFlag |= (SATflags(conflicting) & ObjMask);
sat_MarkNodeInConflict(
cm, d, &nMarked, &tObjectFlag, &tLevel, nClauseArray);
/* Traverse implication graph backward */
first = 1;
implied = d->implied;
space = implied->space+implied->num-1;
for(i=implied->num-1; i>=0; i--, space--) {
v = *space;
if(v == maxV) {
if(SATflags(v) & VisitedMask) {
SATflags(v) &= ResetVisitedMask;
--nMarked;
value = SATvalue(v);
sat_ArrayInsert(nClauseArray, v^(!value));
}
continue;
}
if(SATflags(v) & VisitedMask) {
SATflags(v) &= ResetVisitedMask;
--nMarked;
if(nMarked == 0 && (!first || i == 0)) {
value = SATvalue(v);
tFdaLit = v^(!value);
sat_ArrayInsert(nClauseArray, tFdaLit);
break;
}
ante= SATante(v);
inverted = SATisInverted(ante);
ante= SATnormalNode(ante);
if(SATflags(ante) & IsCNFMask) {
size = SATnumLits(ante);
for(j=0, plit=(long*)SATfirstLit(ante); j<size; j++, plit++) {
nv = SATgetNode(*plit);
if(SATnormalNode(nv) != v)
sat_MarkNodeSub(cm, nv, &nMarked, &tLevel, d, nClauseArray);
}
}
else {
sat_MarkNodeSub(cm, ante, &nMarked, &tLevel, d, nClauseArray);
ante2 = SATante2(v);
if(ante2)
sat_MarkNodeSub(cm, ante2, &nMarked, &tLevel, d, nClauseArray);
}
}
first = 0;
}
sat_MinimizeConflictClause(cm, nClauseArray);
inserted = 0;
if(clauseArray->num*4/5 > nClauseArray->num) {
learned = sat_AddConflictClauseNoScoreUpdate(cm, nClauseArray, tObjectFlag);
inserted = 1;
}
sat_ArrayFree(nClauseArray);
}
if( inserted == 0 &&
depth > 20) {
nClauseArray = sat_ArrayAlloc(clauseArray->num);
lBacktrace = depth/3;
uBacktrace = depth*2/3;
markLimit = 1;
minLimit = 1000;
while(1){
nMarked = 0;
tLevel = 0;
depth = 0;
nClauseArray->num = 0;
markLimit++;
if(markLimit > 3) break;
if(minLimit != 1000 && minLimit > 3)
break;
tObjectFlag |= (SATflags(conflicting) & ObjMask);
sat_MarkNodeInConflict(
cm, d, &nMarked, &tObjectFlag, &tLevel, nClauseArray);
first = 1;
implied = d->implied;
space = implied->space+implied->num-1;
for(i=implied->num-1; i>=0; i--, space--) {
v = *space;
if(uBacktrace < depth) {
sat_ResetFlagForClauseArray(cm, nClauseArray);
nClauseArray->num = 0;
for(; i>=0; i--, space--) {
v = *space;
if(SATflags(v) & VisitedMask) {
SATflags(v) &= ResetVisitedMask;
--nMarked;
if(nMarked == 0)
break;
}
}
break;
}
if(nMarked < minLimit)
minLimit = nMarked;
if(depth > lBacktrace && nMarked < markLimit) {
for(; i>=0; i--, space--) {
v = *space;
if(SATflags(v) & VisitedMask) {
SATflags(v) &= ResetVisitedMask;
--nMarked;
value = SATvalue(v);
sat_ArrayInsert(nClauseArray, v^(!value));
if(nMarked == 0)
break;
}
}
}
if(SATflags(v) & VisitedMask) {
depth = cm->variableArray[SATnodeID(v)].depth;
SATflags(v) &= ResetVisitedMask;
--nMarked;
if(nMarked == 0 && (!first || i == 0)) {
value = SATvalue(v);
tFdaLit = v^(!value);
sat_ArrayInsert(nClauseArray, tFdaLit);
break;
}
ante= SATante(v);
inverted = SATisInverted(ante);
ante= SATnormalNode(ante);
if(SATflags(ante) & IsCNFMask) {
size = SATnumLits(ante);
for(j=0, plit=(long*)SATfirstLit(ante); j<size; j++, plit++) {
nv = SATgetNode(*plit);
if(SATnormalNode(nv) != v)
sat_MarkNodeSub(cm, nv, &nMarked, &tLevel, d, nClauseArray);
}
}
else {
sat_MarkNodeSub(cm, ante, &nMarked, &tLevel, d, nClauseArray);
ante2 = SATante2(v);
if(ante2)
sat_MarkNodeSub(cm, ante2, &nMarked, &tLevel, d, nClauseArray);
}
}
first = 0;
}
if(nClauseArray->num == 0)
continue;
sat_MinimizeConflictClause(cm, nClauseArray);
if(clauseArray->num*4/5 > nClauseArray->num) {
learned = sat_AddConflictClauseNoScoreUpdate(cm, nClauseArray, tObjectFlag);
break;
}
}
sat_ArrayFree(nClauseArray);
}
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_FindUIPForCoreGen | ( | satManager_t * | cm, |
| satArray_t * | clauseArray, | ||
| satLevel_t * | d, | ||
| int * | objectFlag, | ||
| int * | bLevel, | ||
| long * | fdaLit | ||
| ) |
Function********************************************************************
Synopsis [ UIP Analysis that is used for UNSAT core generation.]
Description [ UIP Analysis that is used for UNSAT core generation.]
SideEffects []
SeeAlso []
Definition at line 1689 of file satConflict.c.
{
long conflicting;
int nMarked, value;
long v;
int first, i;
long *space;
satArray_t *implied;
satOption_t *option;
conflicting = d->conflict;
nMarked = 0;
option = cm->option;
if(option->incTraceObjective) *objectFlag = 0;
else *objectFlag = ObjMask;
(*objectFlag) |= (SATflags(conflicting) & ObjMask);
/* find seed from conflicting clause to find unique implication point. */
clauseArray->num = 0;
sat_MarkNodeInConflict(
cm, d, &nMarked, objectFlag, bLevel, clauseArray);
/* Traverse implication graph backward */
first = 1;
implied = d->implied;
space = implied->space+implied->num-1;
/* Bing: UNSAT core generation */
if(cm->option->coreGeneration){
cm->dependenceArray = sat_ArrayAlloc(1);
sat_ArrayInsert(cm->dependenceArray,conflicting);
}
for(i=implied->num-1; i>=0; i--, space--) {
v = *space;
if(SATflags(v) & VisitedMask) {
SATflags(v) &= ResetVisitedMask;
--nMarked;
if(nMarked == 0 && (!first || i==0)) {
value = SATvalue(v);
*fdaLit = v^(!value);
sat_ArrayInsert(clauseArray, *fdaLit);
break;
}
/* Bing: UNSAT core generation */
if(cm->option->coreGeneration){
int ante = SATante(v);
if(ante!=0 && !(SATflags(ante) & IsCNFMask)){
printf("node %d is not CNF\n", ante);
exit(0);
}
if(ante==0){
if(!st_lookup(cm->anteTable, (char *)SATnormalNode(v), &ante)){
printf("ante = 0 and is not in anteTable %ld\n",v);
exit(0);
}
}
sat_ArrayInsert(cm->dependenceArray,ante);
}
sat_MarkNodeInImpliedNode(
cm, d, v, &nMarked, objectFlag, bLevel, clauseArray);
}
first = 0;
}
sat_ResetFlagForClauseArray(cm, clauseArray);
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_FindUIPForCoreGenWithRT | ( | satManager_t * | cm, |
| satArray_t * | clauseArray, | ||
| satLevel_t * | d, | ||
| int * | objectFlag, | ||
| int * | bLevel, | ||
| long * | fdaLit | ||
| ) |
Function********************************************************************
Synopsis [find UIP with resolution generation]
Description []
SideEffects []
SeeAlso []
Definition at line 1784 of file satConflict.c.
{
long conflicting;
int nMarked, value;
long v,left,right,inverted,result;
int first, i,size=0;
long *space,*tmp;
satArray_t *implied;
satOption_t *option;
RTnode_t tmprt;
long *lp, *tmpIP,ante,ante2,node,j;
RTManager_t * rm = cm->rm;
conflicting = d->conflict;
nMarked = 0;
option = cm->option;
if(option->incTraceObjective) *objectFlag = 0;
else *objectFlag = ObjMask;
(*objectFlag) |= (SATflags(conflicting) & ObjMask);
/* find seed from conflicting clause to find unique implication point. */
clauseArray->num = 0;
sat_MarkNodeInConflict(
cm, d, &nMarked, objectFlag, bLevel, clauseArray);
/* Traverse implication graph backward */
first = 1;
implied = d->implied;
space = implied->space+implied->num-1;
if(cm->option->coreGeneration){
/*if last conflict is CNF*/
if(SATflags(conflicting)&IsCNFMask){
/*is conflict CNF*/
if(SATflags(conflicting)&IsConflictMask){
if(!st_lookup(cm->RTreeTable,(char*)conflicting,&tmprt)){
printf("RTree node of conflict cnf %ld is not in RTreeTable\n",ante);
exit(0);
}
else{
rm->root = tmprt;
#if PR
printf("Get formula for CONFLICT CLAUSE:%d\n",ante);
#endif
}
}
/*CNF but not conflict*/
else{
rm->root = RTCreateNode(rm);
size = SATnumLits(conflicting);
RT_fSize(rm->root) = size;
lp = (long*)SATfirstLit(conflicting);
sat_BuildRT(cm,rm->root, lp, tmpIP,size,0);
}
}
/*if last conflict is AIG*/
else{
rm->root = RTCreateNode(rm);
node = SATnormalNode(conflicting);
left = SATleftChild(node);
right = SATrightChild(node);
result = PureSat_IdentifyConflict(cm,left,right,conflicting);
inverted = SATisInverted(left);
left = SATnormalNode(left);
left = inverted ? SATnot(left) : left;
inverted = SATisInverted(right);
right = SATnormalNode(right);
right = inverted ? SATnot(right) : right;
j = node;
if(result == 1){
tmp = ALLOC(long,3);
tmp[0] = left;
tmp[1] = SATnot(j);
size = 2;
}
else if(result == 2){
tmp = ALLOC(long,3);
tmp[0] = right;
tmp[1] = SATnot(j);
size = 2;
}
else if(result == 3){
tmp = ALLOC(long,4);
tmp[0] = SATnot(left);
tmp[1] = SATnot(right);
tmp[2] = j;
size = 3;
}
else{
printf("wrong returned result value, exit\n");
exit(0);
}
lp = tmp;
sat_BuildRT(cm,rm->root, lp, tmpIP,size,1);
FREE(tmp);
}
}
for(i=implied->num-1; i>=0; i--, space--) {
v = *space;
if(SATflags(v) & VisitedMask) {
SATflags(v) &= ResetVisitedMask;
--nMarked;
if(nMarked == 0 && (!first || i==0)) {
value = SATvalue(v);
*fdaLit = v^(!value);
sat_ArrayInsert(clauseArray, *fdaLit);
break;
}
if(cm->option->coreGeneration){
ante = SATante(v);
if(ante==0){
if(!(st_lookup(cm->anteTable, (char *)SATnormalNode(v),&ante))){
printf("ante = 0 and is not in anteTable %ld\n",v);
exit(0);
}
}
/*build non-leaf node*/
tmprt = RTCreateNode(rm);
RT_pivot(tmprt) = SATnormalNode(v);
RT_right(tmprt) = rm->root;
rm->root = tmprt;
if((SATflags(ante)&IsConflictMask)&&(SATflags(ante)&IsCNFMask)){
if(!st_lookup(cm->RTreeTable,(char*)ante,&tmprt)){
printf("RTree node of conflict cnf %ld is not in RTreeTable\n",ante);
exit(0);
}
else{
RT_left(rm->root) = tmprt;
#if PR
printf("Get formula for CONFLICT CLAUSE:%d\n",ante);
#endif
}
}
else{ /* if not conflict CNF*/
/*left */
tmprt = RTCreateNode(rm);
RT_left(rm->root) = tmprt;
/*left is AIG*/
if(!(SATflags(ante) & IsCNFMask)){
/*generate formula for left*/
tmp = ALLOC(long,3);
value = SATvalue(v);
node = SATnormalNode(v);
node = value==1?node:SATnot(node);
tmp[0] = node;
size = 1;
if(ante != SATnormalNode(v)){
value = SATvalue(ante);
node = SATnormalNode(ante);
node = value==1?SATnot(node):node;
tmp[1] = node;
size++;
ante2 = SATante2(v);
if(ante2){
value = SATvalue(ante2);
node = SATnormalNode(ante2);
node = value==1?SATnot(node):node;
tmp[2] = node;
size++;
}
}
lp = tmp;
sat_BuildRT(cm,tmprt,lp,tmpIP,size,1);
FREE(tmp);
}
/* left is CNF*/
else{
lp = (long*)SATfirstLit(ante);
size = SATnumLits(ante);
RT_fSize(tmprt) = size;
sat_BuildRT(cm,tmprt, lp, tmpIP,size,0);
}
} /*else{ // if not conflict CNF*/
}/*if(cm->option->coreGeneration){*/
sat_MarkNodeInImpliedNode(
cm, d, v, &nMarked, objectFlag, bLevel, clauseArray);
}
first = 0;
}
sat_ResetFlagForClauseArray(cm, clauseArray);
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_FindUIPWithRT | ( | satManager_t * | cm, |
| satArray_t * | clauseArray, | ||
| satLevel_t * | d, | ||
| int * | objectFlag, | ||
| int * | bLevel, | ||
| long * | fdaLit | ||
| ) |
Function********************************************************************
Synopsis [find UIP with resolution generation]
Description []
SideEffects []
SeeAlso []
Definition at line 1143 of file satConflict.c.
{
long conflicting;
int nMarked, value;
int first, i,j;
long *space, v,left,right,inverted,result,*tmp;
satArray_t *implied;
satOption_t *option;
RTnode_t tmprt;
int size = 0;
long *lp,*tmpIP,ante,ante2,node;
RTManager_t * rm = cm->rm;
conflicting = d->conflict;
nMarked = 0;
option = cm->option;
if(option->incTraceObjective) *objectFlag = 0;
else *objectFlag = ObjMask;
(*objectFlag) |= (SATflags(conflicting) & ObjMask);
/* find seed from conflicting clause to find unique implication point.
* */
clauseArray->num = 0;
sat_MarkNodeInConflict(
cm, d, &nMarked, objectFlag, bLevel, clauseArray);
/* Traverse implication graph backward */
first = 1;
implied = d->implied;
space = implied->space+implied->num-1;
if(cm->option->coreGeneration){
/*if last conflict is CNF*/
if(SATflags(conflicting)&IsCNFMask){
/*is conflict CNF*/
if(SATflags(conflicting)&IsConflictMask){
if(!st_lookup(cm->RTreeTable,(char*)conflicting,&tmprt)){
printf("RTree node of conflict cnf %ld is not in RTreeTable\n",ante);
exit(0);
}
else{
rm->root = tmprt;
#if PR
printf("Get formula for CONFLICT CLAUSE:%d\n",ante);
#endif
}
}
/*CNF but not conflict*/
else{
rm->root = RTCreateNode(rm);
size = SATnumLits(conflicting);
RT_fSize(rm->root) = size;
lp = (long*)SATfirstLit(conflicting);
sat_BuildRT(cm,rm->root, lp, tmpIP,size,0);
}
}
/*if last conflict is AIG*/
else{
rm->root = RTCreateNode(rm);
node = SATnormalNode(conflicting);
left = SATleftChild(node);
right = SATrightChild(node);
result = PureSat_IdentifyConflict(cm,left,right,conflicting);
inverted = SATisInverted(left);
left = SATnormalNode(left);
left = inverted ? SATnot(left) : left;
inverted = SATisInverted(right);
right = SATnormalNode(right);
right = inverted ? SATnot(right) : right;
j = node;
if(result == 1){
tmp = ALLOC(long,3);
tmp[0] = left;
tmp[1] = SATnot(j);
size = 2;
}
else if(result == 2){
tmp = ALLOC(long,3);
tmp[0] = right;
tmp[1] = SATnot(j);
size = 2;
}
else if(result == 3){
tmp = ALLOC(long,4);
tmp[0] = SATnot(left);
tmp[1] = SATnot(right);
tmp[2] = j;
size = 3;
}
else{
printf("wrong returned result value, exit\n");
exit(0);
}
lp = tmp;
sat_BuildRT(cm,rm->root, lp, tmpIP,size,1);
FREE(tmp);
}
}
for(i=implied->num-1; i>=0; i--, space--) {
v = *space;
if(SATflags(v) & VisitedMask) {
SATflags(v) &= ResetVisitedMask;
--nMarked;
if(nMarked == 0 && (!first || i==0)) {
value = SATvalue(v);
*fdaLit = v^(!value);
sat_ArrayInsert(clauseArray, *fdaLit);
break;
}
if(cm->option->coreGeneration){
ante = SATante(v);
if(ante==0){
if(!(st_lookup(cm->anteTable, (char *)SATnormalNode(v),&ante))){
printf("ante = 0 and is not in anteTable %ld\n",v);
exit(0);
}
}
/*build non-leaf node*/
tmprt = RTCreateNode(rm);
RT_pivot(tmprt) = SATnormalNode(v);
RT_right(tmprt) = rm->root;
rm->root = tmprt;
if((SATflags(ante)&IsConflictMask)&&(SATflags(ante)&IsCNFMask)){
if(!st_lookup(cm->RTreeTable,(char*)ante,&tmprt)){
printf("RTree node of conflict cnf %ld is not in RTreeTable\n",ante);
exit(0);
}
else{
RT_left(rm->root) = tmprt;
#if PR
printf("Get formula for CONFLICT CLAUSE:%d\n",ante);
#endif
}
}
else{ /* if not conflict CNF*/
/*left */
tmprt = RTCreateNode(rm);
RT_left(rm->root) = tmprt;
/*left is AIG*/
if(!(SATflags(ante) & IsCNFMask)){
/*generate formula for left*/
tmp = ALLOC(long,3);
value = SATvalue(v);
node = SATnormalNode(v);
node = value==1?node:SATnot(node);
tmp[0] = node;
size = 1;
if(ante != SATnormalNode(v)){
value = SATvalue(ante);
node = SATnormalNode(ante);
node = value==1?SATnot(node):node;
tmp[1] = node;
size++;
ante2 = SATante2(v);
if(ante2){
value = SATvalue(ante2);
node = SATnormalNode(ante2);
node = value==1?SATnot(node):node;
tmp[2] = node;
size++;
}
}
lp = tmp;
sat_BuildRT(cm,tmprt,lp,tmpIP,size,1);
FREE(tmp);
}
/* left is CNF*/
else{
lp = (long*)SATfirstLit(ante);
size = SATnumLits(ante);
RT_fSize(tmprt) = size;
sat_BuildRT(cm,tmprt, lp, tmpIP,size,0);
}
} /*else{ // if not conflict CNF*/
}/*if(cm->option->coreGeneration){*/
sat_MarkNodeInImpliedNode(
cm, d, v, &nMarked, objectFlag, bLevel, clauseArray);
}
first = 0;
}
/* Minimize conflict clause */
if(option->minimizeConflictClause)
sat_MinimizeConflictClause(cm, clauseArray);
else
sat_ResetFlagForClauseArray(cm, clauseArray);
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_MarkNodeInConflict | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| int * | nMarked, | ||
| int * | objectFlag, | ||
| int * | bLevel, | ||
| satArray_t * | clauseArray | ||
| ) |
Function********************************************************************
Synopsis [ Find seed for unique implication point analysis from conflicting clause]
Description [ Find seed for unique implication point analysis from conflicting clause]
SideEffects []
SeeAlso []
Definition at line 2112 of file satConflict.c.
{
satOption_t *option;
option = cm->option;
if(option->incTraceObjective == 0) {
sat_MarkNodeInConflictClauseNoObj(
cm, d, nMarked, objectFlag, bLevel, clauseArray);
}
else if(option->incTraceObjective == 1) { /* conservative */
sat_MarkNodeInConflictClauseObjConservative(
cm, d, nMarked, objectFlag, bLevel, clauseArray);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_MarkNodeInConflictClauseNoObj | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| int * | nMarked, | ||
| int * | oFlag, | ||
| int * | bLevel, | ||
| satArray_t * | clauseArray | ||
| ) |
Function********************************************************************
Synopsis [ Find seed for unique implication point analysis from conflicting clause]
Description [ Find seed for unique implication point analysis from conflicting clause]
SideEffects []
SeeAlso []
Definition at line 2361 of file satConflict.c.
{
long conflict, left, right, nv;
int inverted, size, value, i;
long *plit;
satOption_t *option;
conflict = d->conflict;
inverted = SATisInverted(conflict);
conflict = SATnormalNode(conflict);
option = cm->option;
if(SATflags(conflict) & IsCNFMask) {
size = SATnumLits(conflict);
for(i=0, plit=(long*)SATfirstLit(conflict); i<size; i++, plit++) {
nv = SATgetNode(*plit);
sat_MarkNodeSub(cm, nv, nMarked, bLevel, d, clauseArray);
}
}
else {
value = SATvalue(conflict);
if(value == 1) {
sat_MarkNodeSub(cm, conflict, nMarked, bLevel, d, clauseArray);
left = SATleftChild(conflict);
inverted = SATisInverted(left);
left = SATnormalNode(left);
value = SATvalue(left) ^ inverted;
if(value == 0) {
sat_MarkNodeSub(cm, left, nMarked, bLevel, d, clauseArray);
return;
}
right = SATrightChild(conflict);
inverted = SATisInverted(right);
right = SATnormalNode(right);
value = SATvalue(right) ^ inverted;
if(value == 0) {
sat_MarkNodeSub(cm, right, nMarked, bLevel, d, clauseArray);
return;
}
}
else if(value == 0) {
left = SATleftChild(conflict);
right = SATrightChild(conflict);
sat_MarkNodeSub(cm, conflict, nMarked, bLevel, d, clauseArray);
sat_MarkNodeSub(cm, left, nMarked, bLevel, d, clauseArray);
sat_MarkNodeSub(cm, right, nMarked, bLevel, d, clauseArray);
}
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_MarkNodeInConflictClauseObjConservative | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| int * | nMarked, | ||
| int * | oFlag, | ||
| int * | bLevel, | ||
| satArray_t * | clauseArray | ||
| ) |
Function********************************************************************
Synopsis [ Find seed for unique implication point analysis from conflicting clause]
Description [ Find seed for unique implication point analysis from conflicting clause]
SideEffects []
SeeAlso []
Definition at line 2433 of file satConflict.c.
{
long conflict, left, right, nv;
int inverted, size, value, i;
long *plit;
satOption_t *option;
conflict = d->conflict;
inverted = SATisInverted(conflict);
conflict = SATnormalNode(conflict);
option = cm->option;
if(SATflags(conflict) & IsCNFMask) {
size = SATnumLits(conflict);
for(i=0, plit=(long*)SATfirstLit(conflict); i<size; i++, plit++) {
nv = SATgetNode(*plit);
*oFlag |= (SATflags(nv) & ObjMask);
sat_MarkNodeSub(cm, nv, nMarked, bLevel, d, clauseArray);
}
}
else {
value = SATvalue(conflict);
if(value == 1) {
*oFlag |= (SATflags(conflict) & ObjMask);
sat_MarkNodeSub(cm, conflict, nMarked, bLevel, d, clauseArray);
left = SATleftChild(conflict);
inverted = SATisInverted(left);
left = SATnormalNode(left);
value = SATvalue(left) ^ inverted;
if(value == 0) {
*oFlag |= (SATflags(left) & ObjMask);
sat_MarkNodeSub(cm, left, nMarked, bLevel, d, clauseArray);
return;
}
right = SATrightChild(conflict);
inverted = SATisInverted(right);
right = SATnormalNode(right);
value = SATvalue(right) ^ inverted;
if(value == 0) {
*oFlag |= (SATflags(right) & ObjMask);
sat_MarkNodeSub(cm, right, nMarked, bLevel, d, clauseArray);
return;
}
}
else if(value == 0) {
*oFlag |= (SATflags(conflict) & ObjMask);
left = SATleftChild(conflict);
inverted = SATisInverted(left);
left = SATnormalNode(left);
*oFlag |= (SATflags(left) & ObjMask);
right = SATrightChild(conflict);
inverted = SATisInverted(right);
right = SATnormalNode(right);
*oFlag |= (SATflags(right) & ObjMask);
sat_MarkNodeSub(cm, conflict, nMarked, bLevel, d, clauseArray);
sat_MarkNodeSub(cm, left, nMarked, bLevel, d, clauseArray);
sat_MarkNodeSub(cm, right, nMarked, bLevel, d, clauseArray);
}
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_MarkNodeInImpliedNode | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| int * | nMarked, | ||
| int * | objectFlag, | ||
| int * | bLevel, | ||
| satArray_t * | clauseArray | ||
| ) |
Function********************************************************************
Synopsis [ Traverse the antecedent to find unique implication point]
Description [ Traverse the antecedent to find unique implication point]
SideEffects []
SeeAlso []
Definition at line 2145 of file satConflict.c.
{
satOption_t *option;
option = cm->option;
if(option->incTraceObjective == 0) {
sat_MarkNodeInImpliedNodeNoObj(
cm, d, v, nMarked, objectFlag, bLevel, clauseArray);
}
else if(option->incTraceObjective == 1) { /* conservative */
sat_MarkNodeInImpliedNodeObjConservative(
cm, d, v, nMarked, objectFlag, bLevel, clauseArray);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_MarkNodeInImpliedNodeNoObj | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| int * | nMarked, | ||
| int * | oFlag, | ||
| int * | bLevel, | ||
| satArray_t * | clauseArray | ||
| ) |
Function********************************************************************
Synopsis [ Traverse the antecedent to find unique implication point]
Description [ Traverse the antecedent to find unique implication point]
SideEffects []
SeeAlso []
Definition at line 2230 of file satConflict.c.
{
long ante, ante2, nv;
int inverted, size, i;
long *plit;
satOption_t *option;
ante= SATante(v);
/* Bing: UNSAT core generation */
if(cm->option->coreGeneration){
if(ante==0){
if(!(st_lookup(cm->anteTable, (char *)(long)SATnormalNode(v), &ante))){
printf("ante = 0 and is not in anteTable %ld\n",v);
exit(0);
}
}
}
inverted = SATisInverted(ante);
ante= SATnormalNode(ante);
option = cm->option;
if(SATflags(ante) & IsCNFMask) {
SATconflictUsage(ante)++;
size = SATnumLits(ante);
for(i=0, plit=(long*)SATfirstLit(ante); i<size; i++, plit++) {
nv = SATgetNode(*plit);
if((int)(SATnormalNode(nv)) == v) continue;
sat_MarkNodeSub(cm, nv, nMarked, bLevel, d, clauseArray);
}
}
else {
/*Bing: very inmportant for level zero conflict analysis*/
if(ante != SATnormalNode(v))
sat_MarkNodeSub(cm, ante, nMarked, bLevel, d, clauseArray);
ante2 = SATante2(v);
if(ante2)
sat_MarkNodeSub(cm, ante2, nMarked, bLevel, d, clauseArray);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_MarkNodeInImpliedNodeObjConservative | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| int * | nMarked, | ||
| int * | oFlag, | ||
| int * | bLevel, | ||
| satArray_t * | clauseArray | ||
| ) |
Function********************************************************************
Synopsis [ Traverse the antecedent to find unique implication point]
Description [ Traverse the antecedent to find unique implication point]
SideEffects []
SeeAlso []
Definition at line 2291 of file satConflict.c.
{
long ante, ante2, nv;
int inverted, size, i;
int objectFlag;
long *plit;
satOption_t *option;
ante= SATante(v);
/* Bing: UNSAT core generation */
if(cm->option->coreGeneration){
if(ante==0){
if(!(st_lookup(cm->anteTable, (char *)SATnormalNode(v), &ante))){
printf("ante = 0 and is not in anteTable %ld\n",v);
exit(0);
}
}
}
inverted = SATisInverted(ante);
ante= SATnormalNode(ante);
objectFlag = 0;
option = cm->option;
if(SATflags(ante) & IsCNFMask) {
SATconflictUsage(ante)++;
size = SATnumLits(ante);
for(i=0, plit=(long*)SATfirstLit(ante); i<size; i++, plit++) {
nv = SATgetNode(*plit);
nv = SATnormalNode(nv);
if(nv == v) continue;
sat_MarkNodeSub(cm, nv, nMarked, bLevel, d, clauseArray);
}
objectFlag |= SATflags(ante) & ObjMask;
}
else {
/*Bing: very inmportant for level zero conflict analysis*/
if(ante != SATnormalNode(v))
sat_MarkNodeSub(cm, ante, nMarked, bLevel, d, clauseArray);
ante2 = SATante2(v);
if(ante2) {
ante2 = SATnormalNode(ante2);
sat_MarkNodeSub(cm, ante2, nMarked, bLevel, d, clauseArray);
}
}
*oFlag |= objectFlag;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_MarkNodeSub | ( | satManager_t * | cm, |
| long | v, | ||
| int * | nMarked, | ||
| int * | bLevel, | ||
| satLevel_t * | d, | ||
| satArray_t * | clauseArray | ||
| ) |
Function********************************************************************
Synopsis [ If the node is implied in current level then mark it, otherwise add it to conflict clause]
Description [ If the node is implied in current level then mark it, otherwise add it to conflict clause]
SideEffects []
SeeAlso []
Definition at line 2181 of file satConflict.c.
{
satLevel_t *td;
satOption_t *option;
int value;
v = SATnormalNode(v);
td = SATgetDecision(SATlevel(v));
if(d == td) {
if(!(SATflags(v) & VisitedMask)) {
(*nMarked)++;
SATflags(v) |= VisitedMask;
}
}
else if(td->level < d->level) {
if(!(SATflags(v) & NewMask)) {
option = cm->option;
if((td->level != 0) ||
(td->level == 0 && option->includeLevelZeroLiteral)) {
SATflags(v) |= NewMask;
value = SATvalue(v);
sat_ArrayInsert(clauseArray, v^(!value));
if(*bLevel < td->level)
*bLevel = td->level;
}
}
}
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_MinimizeConflictClause | ( | satManager_t * | cm, |
| satArray_t * | clauseArray | ||
| ) |
Function********************************************************************
Synopsis [ Minimize the literals of conflict clause]
Description [ If the literal can be implied by other literals in conflict clause then we can delete it from conflict clause.]
SideEffects []
SeeAlso []
Definition at line 2011 of file satConflict.c.
{
int i, j, size, all, tsize;
int inverted;
long v, tv;
long ante, ante2;
long *plit;
satArray_t *newArray;
satVariable_t *var;
size = clauseArray->num;
newArray = sat_ArrayAlloc(size);
for(i=0; i<size; i++) {
v = clauseArray->space[i];
inverted = SATisInverted(v);
v = SATnormalNode(v);
ante = SATante(v);
ante = SATnormalNode(ante);
if(SATflags(ante) & IsCNFMask) {
tsize = SATnumLits(ante);
all = 1;
for(j=0, plit=(long*)SATfirstLit(ante); j<tsize; j++, plit++) {
tv = SATgetNode(*plit);
tv = SATnormalNode(tv);
if(tv == v) continue;
if(!(SATflags(tv) & NewMask)) {
all = 0;
break;
}
}
if(all) {
var = SATgetVariable(v);
if(inverted) (var->litsCount[1])++;
else (var->litsCount[0])++;
continue;
}
}
else {
if(SATflags(ante) & NewMask) {
ante2 = SATante2(v);
ante2 = SATnormalNode(ante2);
if((ante2==0) || (SATflags(ante2) & NewMask)) {
var = SATgetVariable(v);
if(inverted) (var->litsCount[1])++;
else (var->litsCount[0])++;
continue;
}
}
}
sat_ArrayInsert(newArray, v^inverted);
}
sat_ResetFlagForClauseArray(cm, clauseArray);
memcpy(clauseArray->space, newArray->space, sizeof(long)*(newArray->num));
clauseArray->num = newArray->num;
sat_ArrayFree(newArray);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_ResetFlagForClauseArray | ( | satManager_t * | cm, |
| satArray_t * | clauseArray | ||
| ) |
Function********************************************************************
Synopsis [ Reset flags that are used to indentify conflict clause]
Description [ Reset flags that are used to indentify conflict clause]
SideEffects []
SeeAlso []
Definition at line 2083 of file satConflict.c.
{
int size, i;
long v;
size = clauseArray->num;
for(i=0; i<size; i++) {
v = clauseArray->space[i];
v = SATnormalNode(v);
SATflags(v) &= ResetNewVisitedMask;
}
}
Here is the caller graph for this function:
| int sat_StrongConflictAnalysis | ( | satManager_t * | cm, |
| satLevel_t * | d | ||
| ) |
Function********************************************************************
Synopsis [ Strong Conflict Analysis.]
Description [ Strong Conflict Analysis.]
SideEffects []
SeeAlso []
Bing : UNSAT core generation
Definition at line 290 of file satConflict.c.
{
satStatistics_t *stats;
satOption_t *option;
satArray_t *clauseArray;
int objectFlag;
int bLevel;
long fdaLit, conflicting;
conflicting = d->conflict;
if(d->level == 0) {
if(cm->option->coreGeneration)
sat_ConflictAnalysisForCoreGen(cm, d);
cm->currentDecision--;
return (-1);
}
stats = cm->each;
option = cm->option;
stats->nBacktracks++;
if(SATflags(conflicting) & IsCNFMask) {
SATnumConflict(conflicting) += 1;
}
clauseArray = cm->auxArray;
bLevel = 0;
fdaLit = -1;
clauseArray->num = 0;
/* Find Unique Implication Point */
sat_FindUIPAndNonUIP(cm, clauseArray, d, &objectFlag, &bLevel, &fdaLit);
stats->nNonchonologicalBacktracks += (d->level - bLevel);
if(clauseArray->num == 0) {
sat_PrintImplicationGraph(cm, d);
sat_PrintNode(cm, conflicting);
}
/* If we could find UIP then it is critical error...
* at lease the decision node has to be detected as UIP.
*/
if(fdaLit == -1) {
fprintf(cm->stdOut, "%s ERROR : Illegal unit literal\n", cm->comment);
fflush(cm->stdOut);
sat_PrintNode(cm, conflicting);
sat_PrintImplicationGraph(cm, d);
sat_PrintDotForConflict(cm, d, conflicting, 0);
exit(0);
}
if(bLevel && cm->lowestBacktrackLevel > bLevel)
cm->lowestBacktrackLevel = bLevel;
bLevel = sat_AddConflictClauseAndBacktrack(
cm, clauseArray, d, fdaLit, bLevel, objectFlag, 1);
return(bLevel);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_Undo | ( | satManager_t * | cm, |
| satLevel_t * | d | ||
| ) |
Function********************************************************************
Synopsis [ Undo implication]
Description [ Undo implication]
SideEffects []
SeeAlso []
Definition at line 2555 of file satConflict.c.
{
satArray_t *implied, *satisfied;
satVariable_t *var;
int size, i;
long *space, v;
implied = d->implied;
space = implied->space;
size = implied->num;
for(i=0; i<size; i++, space++) {
v = *space;
SATvalue(v) = 2;
SATflags(v) &= ResetNewVisitedObjInQueueMask;
var = &(cm->variableArray[SATnodeID(v)]);
var->antecedent = 0;
var->antecedent2 = 0;
var->level = -1;
var->depth = 0;
}
cm->implicatedSoFar -= size;
if(d->satisfied) {
satisfied = d->implied;
space = satisfied->space;
size = satisfied->num;
for(i=0; i<size; i++, space++) {
v = *space;
SATflags(v) &= ResetBDDSatisfiedMask;
}
d->satisfied->num = 0;
}
if(d->level > 0) {
if((cm->decisionHead[d->level-1]).currentVarPos < cm->currentVarPos)
cm->currentVarPos = (cm->decisionHead[d->level-1]).currentVarPos;
}
else
cm->currentVarPos = d->currentVarPos;
d->implied->num = 0;
d->currentVarPos = 0;
d->conflict = 0;
}
Here is the caller graph for this function:
Variable Documentation
satManager_t* SATcm [static] |
Definition at line 25 of file satConflict.c.
char rcsid [] UNUSED = "$Id: satConflict.c,v 1.31 2009/04/11 18:26:37 fabio Exp $" [static] |
CFile***********************************************************************
FileName [satConflict.c]
PackageName [sat]
Synopsis [Routines for sat conflict analysism and unsat proof generation for both CNF format and AIG format]
Author [HoonSang Jin, Bing Li]
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 23 of file satConflict.c.
