VIS

src/sat/satInterface.c

Go to the documentation of this file.
00001 
00019 #include "satInt.h"
00020 
00021 static char rcsid[] UNUSED = "$Id: satInterface.c,v 1.20 2009/04/11 18:26:37 fabio Exp $";
00022 
00023 /*---------------------------------------------------------------------------*/
00024 /* Constant declarations                                                     */
00025 /*---------------------------------------------------------------------------*/
00026 
00029 /*---------------------------------------------------------------------------*/
00030 /* Static function prototypes                                                */
00031 /*---------------------------------------------------------------------------*/
00032 
00033 
00037 /*---------------------------------------------------------------------------*/
00038 /* Definition of exported functions                                          */
00039 /*---------------------------------------------------------------------------*/
00051 void sat_SetOptionForUP(satManager_t * cm)
00052 {
00053   cm->option->includeLevelZeroLiteral = 1;
00054   cm->option->minimizeConflictClause = 0;
00055   cm->option->clauseDeletionHeuristic = 0;
00056   cm->dependenceTable = st_init_table(st_ptrcmp, st_ptrhash);
00057   cm->anteTable = st_init_table(st_numcmp, st_numhash);
00058   cm->fp = fopen(cm->option->unsatCoreFileName, "w");
00059 }
00060 
00072 int
00073 sat_ReadCNF(satManager_t *cm, char *filename)
00074 {
00075 FILE *fin;
00076 satArray_t *clauseArray;
00077 char line[16384], word[1024], *lp;
00078 int nVar, nCl, nArg;
00079 int i, id, sign;
00080 long v;
00081 int begin;
00082  long cls_idx;
00083 
00084   if(!(fin = fopen(filename, "r"))) {
00085     fprintf(cm->stdOut, "%s ERROR : Can't open CNF file %s\n",
00086             cm->comment, filename);
00087     return(0);
00088   }
00089 
00090   //Bing: for unsat core
00091   if(cm->option->coreGeneration)
00092     sat_SetOptionForUP(cm);
00093 
00094   begin = 0;
00095   clauseArray = sat_ArrayAlloc(1024);
00096   while(fgets(line, 16384, fin)) {
00097     lp = sat_RemoveSpace(line);
00098     if(lp[0] == '\n')   continue;
00099     if(lp[0] == '#')    continue;
00100     if(lp[0] == 'c')    continue;
00101     if(lp[0] == 'p') {
00102       nArg = sscanf(line, "p cnf %d %d", &nVar, &nCl);
00103       if(nArg < 2) {
00104         fprintf(cm->stdErr, "ERROR : Unable to read the number of variables and clauses from CNF file %s\n", filename);
00105         fclose(fin);
00106         sat_ArrayFree(clauseArray);
00107         return(0);
00108       }
00109       begin = 1;
00110 
00111       for(i=1; i<=nVar; i++) {
00112         v = sat_CreateNode(cm, 2, 2);
00113         SATflags(v) |= CoiMask;
00114         SATvalue(v) = 2;
00115       }
00116 
00117       cm->initNumVariables = nVar;
00118       cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1);
00119       memset(cm->variableArray, 0, sizeof(satVariable_t) * (cm->initNumVariables+1));
00120       continue;
00121     }
00122     else if(begin == 0) continue;
00123 
00124     clauseArray->num = 0;
00125     while(1) {
00126       lp = sat_RemoveSpace(lp);
00127       lp = sat_CopyWord(lp, word);
00128 
00129       if(strlen(word)) {
00130         id = atoi(word);
00131         sign = 1;
00132 
00133         if(id != 0) {
00134           if(id < 0) {
00135             id = -id;
00136             sign = 0;
00137           }
00138           sat_ArrayInsert(clauseArray, (id*satNodeSize + sign));
00139         }
00140         else {
00141           if(clauseArray->num == 1) {
00142             v = clauseArray->space[0];
00143             sat_ArrayInsert(cm->unitLits, SATnot(v));
00144             cm->initNumClauses++;
00145             cm->initNumLiterals += clauseArray->num;
00146             //Bing: for unsat core
00147             if(cm->option->coreGeneration){
00148               cls_idx = sat_AddUnitClause(cm, clauseArray);
00149               if(cm->option->coreGeneration){
00150                 v = SATnormalNode(v);
00151                 st_insert(cm->anteTable,(char *)v,(char *)cls_idx);
00152               }
00153             }
00154           }
00155           else {
00156             sat_AddClause(cm, clauseArray);
00157             cm->initNumClauses++;
00158             cm->initNumLiterals += clauseArray->num;
00159           }
00160           break;
00161         }
00162       }
00163     }
00164   }
00165   if(cm->initNumClauses == 0) {
00166     fprintf(cm->stdOut, "%s ERROR : CNF is not valid\n", cm->comment);
00167     return(0);
00168   }
00169 
00170   if(cm->initNumClauses != nCl) {
00171     fprintf(cm->stdOut, "%s WARNING : wrong number of clauses\n", cm->comment);
00172   }
00173 
00174   fclose(fin);
00175   sat_ArrayFree(clauseArray);
00176 
00177   return(1);
00178 }
00179 
00191 int
00192 sat_ReadCNFFromArray(
00193         satManager_t *cm,
00194         satArray_t *cnfArray,
00195         st_table *mappedTable)
00196 {
00197 satArray_t *clauseArray;
00198 int nVar, nCl;
00199 int i;
00200 long tv, v, c, *space;
00201 
00202   if(cnfArray == 0) {
00203     fprintf(cm->stdOut, "%s ERROR : Can't find CNF array \n", cm->comment);
00204     return(0);
00205   }
00206 
00207   nVar = 0;
00208   nCl = 0;
00209   for(i=1; i<cnfArray->num; i++) {
00210     v = cnfArray->space[i];
00211     if(v <= 0)  nCl++;
00212     else {
00213       v = SATnormalNode(v);
00214       if(v > nVar)      nVar = v;
00215     }
00216   }
00217   nVar = nVar / satNodeSize;
00218   for(i=1; i<=nVar; i++) {
00219     v = sat_CreateNode(cm, 2, 2);
00220     SATflags(v) |= CoiMask;
00221     SATvalue(v) = 2;
00222   }
00223 
00224   cm->initNumVariables = nVar;
00225   cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1);
00226   memset(cm->variableArray, 0, sizeof(satVariable_t) * (cm->initNumVariables+1));
00227 
00228   clauseArray = sat_ArrayAlloc(1024);
00229   for(i=0, space=cnfArray->space; i<cnfArray->num; i++, space++){
00230     if(*space <= 0) {
00231       space++;
00232       i++;
00233       if(i>=cnfArray->num)
00234         break;
00235       clauseArray->num = 0;
00236       while(*space > 0) {
00237         v = (*space);
00238         sat_ArrayInsert(clauseArray, SATnot(v));
00239         i++;
00240         space++;
00241       }
00242 
00246       tv = *space;
00247 
00248       if(clauseArray->num > 1)
00249         c = sat_AddClause(cm, clauseArray);
00250       else {
00251         c = sat_AddUnitClause(cm, clauseArray);
00252         if(cm->option->coreGeneration) {
00253           st_insert(cm->anteTable,(char *)(long)(SATnormalNode(v)),(char *)(long)c);
00254         }
00255       }
00256       if(clauseArray->num == 1)
00257         sat_ArrayInsert(cm->unitLits, (v));
00258 
00259       if(tv < -1) { /* this is blocking clause */
00260         st_insert(mappedTable, (char *)c, (char *)(-tv));
00261       }
00262 
00263       cm->initNumClauses++;
00264       cm->initNumLiterals += clauseArray->num;
00265       i--;
00266       space--;
00267     }
00268   }
00269   sat_ArrayFree(clauseArray);
00270 
00271 
00272   return(1);
00273 }
00274 
00286 int
00287 sat_WriteCNFFromArray(satArray_t *cnfArray, char *filename)
00288 {
00289 FILE *fin;
00290 int nVar, nCl;
00291 int i ;
00292 long v, *space;
00293 
00294   if(cnfArray == 0) {
00295     fprintf(stdout, "ERROR : Can't find CNF array \n");
00296     return(0);
00297   }
00298 
00299   if(!(fin=fopen(filename, "w"))) {
00300     fprintf(stdout, "ERROR : Can't find file %s\n", filename);
00301     return(0);
00302   }
00303 
00304   nVar = 0;
00305   nCl = 0;
00306   for(i=1; i<cnfArray->num; i++) {
00307     v = cnfArray->space[i];
00308     if(v <= 0)  nCl++;
00309     else {
00310       v = SATnormalNode(v);
00311       if(v > nVar)      nVar = v;
00312     }
00313   }
00314   nVar = nVar / satNodeSize;
00315 
00316   fprintf(fin, "p cnf %d %d\n", nVar, nCl);
00317 
00318   for(i=0, space=cnfArray->space; i<cnfArray->num; i++, space++){
00319     if(*space <= 0) {
00320       space++;
00321       i++;
00322       if(i>=cnfArray->num)
00323         break;
00324 
00325       while(*space > 0) {
00326         v = (*space);
00327         if(SATisInverted(v))    v = -(SATnodeID(v));
00328         else                    v = SATnodeID(v);
00329         fprintf(fin, "%ld ", v);
00330         i++;
00331         space++;
00332       }
00333       fprintf(fin, "0\n");
00334 
00335       i--;
00336       space--;
00337     }
00338   }
00339   fclose(fin);
00340 
00341   return(1);
00342 }
00354 char *
00355 sat_CopyWord(char *lp, char *word)
00356 {
00357 char *wp;
00358 
00359   for(wp = word; ; lp++, wp++) {
00360     if((*lp == ' ') || (*lp == '\t') || (*lp == '\n'))  break;
00361     *wp = *lp;
00362   }
00363   *wp = '\0';
00364   return(lp);
00365 }
00366 
00378 char *
00379 sat_RemoveSpace(char *line)
00380 {
00381 int i;
00382 
00383   for(i=0; ; i++) {
00384     if(line[i] == ' ')          continue;
00385     else if(line[i] == '\t')    continue;
00386     return(&(line[i]));
00387   }
00388 }
00389 
00390 
00405 void
00406 sat_WriteCNFWithPartialAssignment(satManager_t *cm, char *filename)
00407 {
00408 int nVars, nCls, j;
00409 int size, satisfied;
00410 int inverted, value;
00411 long *plit, v, tv, tsize, i;
00412 FILE *fout;
00413 
00414   nVars = 0;
00415   nCls = 0;
00416   tsize = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict;
00417   for(i=satNodeSize; i<tsize; i+=satNodeSize) {
00418     if(SATleftChild(i) == 2 && SATrightChild(i) == 2)   continue;
00419     if(!(SATflags(i) & IsCNFMask))      {
00420       if(!(SATflags(i) & CoiMask))      continue;
00421       fprintf(cm->stdOut, "Warning : current implementation can't take care of AIG node\n");
00422       continue;
00423     }
00424     if(SATreadInUse(i) == 0)    continue;
00425 
00426     size = SATnumLits(i);
00427     satisfied = 0;
00428     plit = (long *)SATfirstLit(i);
00429     for(j=0; j<size; j++, plit++) {
00430       v = SATgetNode(*plit);
00431       inverted = SATisInverted(v);
00432       v = SATnormalNode(v);
00433       value = SATvalue(v) ^ inverted;
00434       if(value == 1) {
00435         satisfied = 1;
00436         break;
00437       }
00438       if(v > nVars)     nVars = v;
00439     }
00440     if(satisfied)       continue;
00441 
00442     nCls++;
00443   }
00444   nVars /= satNodeSize;
00445 
00446   if(!(fout = fopen(filename, "w"))) {
00447     fprintf(cm->stdOut, "%s ERROR : Can't open file %s\n",
00448             cm->comment, filename);
00449     exit(0);
00450   }
00451 
00452   fprintf(fout, "p cnf %d %d\n", nVars, nCls);
00453   tsize = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict;
00454   for(i=satNodeSize; i<tsize; i+=satNodeSize) {
00455     if(SATleftChild(i) == 2 && SATrightChild(i) == 2)   continue;
00456     if(!(SATflags(i) & IsCNFMask))      {
00457       if(!(SATflags(i) & CoiMask))      continue;
00458       continue;
00459     }
00460     if(SATreadInUse(i) == 0)    continue;
00461 
00462     satisfied = 0;
00463     size = SATnumLits(i);
00464     plit = (long *)SATfirstLit(i);
00465     for(j=0; j<size; j++, plit++) {
00466       v = SATgetNode(*plit);
00467       inverted = SATisInverted(v);
00468       v = SATnormalNode(v);
00469       value = SATvalue(v) ^ inverted;
00470       if(value == 1) {
00471         satisfied = 1;
00472         break;
00473       }
00474     }
00475     if(satisfied)       continue;
00476 
00477     plit = (long *)SATfirstLit(i);
00478     for(j=0; j<size; j++, plit++) {
00479       v = SATgetNode(*plit);
00480       inverted = SATisInverted(v);
00481       v = SATnormalNode(v);
00482       value = SATvalue(v) ^ inverted;
00483       if(value < 2) {
00484         continue;
00485       }
00486       tv = SATnodeID(v);
00487       fprintf(fout, "%ld ", inverted ? -tv : tv);
00488     }
00489     fprintf(fout, "0\n");
00490   }
00491   fclose(fout);
00492 }
00504 void
00505 sat_WriteCNF(satManager_t *cm, char *filename)
00506 {
00507 FILE *fout;
00508 long i, tv, *plit, size, j;
00509 int csize, inverted;
00510 int nVar, nCl;
00511 long left, right;
00512 
00513   if(!(fout = fopen(filename, "w"))) {
00514     fprintf(cm->stdOut, "%s ERROR : Can't open file %s\n",
00515             cm->comment, filename);
00516     exit(0);
00517   }
00518 
00519   nVar = cm->initNumVariables;
00520   nCl = 0;
00521   size = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict;
00522   for(i=satNodeSize; i<size; i+=satNodeSize) {
00523     if(SATleftChild(i) == 2 && SATrightChild(i) == 2)   continue;
00524     if(SATflags(i) & IsCNFMask) {
00525       if(SATreadInUse(i) == 0)  continue;
00526       nCl++;
00527       continue;
00528     }
00529     if(!(SATflags(i) & CoiMask))        continue;
00530     nCl += 3;
00531   }
00532   sat_CountUnitLiteralClauses(cm, cm->assertion, &nCl);
00533   sat_CountUnitLiteralClauses(cm, cm->unitLits, &nCl);
00534   sat_CountUnitLiteralClauses(cm, cm->auxObj, &nCl);
00535   sat_CountUnitLiteralClauses(cm, cm->obj, &nCl);
00536 
00537   fprintf(fout, "p cnf %d %d\n", nVar, nCl);
00538 
00539   sat_PrintUnitLiteralClauses(cm, cm->assertion, fout);
00540   sat_PrintUnitLiteralClauses(cm, cm->unitLits, fout);
00541   sat_PrintUnitLiteralClauses(cm, cm->auxObj, fout);
00542   sat_PrintUnitLiteralClauses(cm, cm->obj, fout);
00543 
00544   size = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict;
00545   for(i=satNodeSize; i<size; i+=satNodeSize) {
00546     if(SATleftChild(i) == 2 && SATrightChild(i) == 2)   continue;
00547     if(SATflags(i) & IsCNFMask) {
00548       csize = SATnumLits(i);
00549       plit = (long*)SATfirstLit(i);
00550       for(j=0; j<csize; j++, plit++) {
00551          tv = SATgetNode(*plit);
00552          inverted = SATisInverted(tv);
00553          tv = SATnormalNode(tv);
00554          tv = SATnodeID(tv);
00555          fprintf(fout, "%ld ", inverted ? -tv : tv);
00556       }
00557       fprintf(fout, "0\n");
00558       continue;
00559     }
00560     if(!(SATflags(i) & CoiMask))        continue;
00561 
00562 
00563     left = SATleftChild(i);
00564     inverted = SATisInverted(left);
00565     left = SATnormalNode(left);
00566     left = SATnodeID(left);
00567     left = inverted ? -left : left;
00568 
00569     right = SATrightChild(i);
00570     inverted = SATisInverted(right);
00571     right = SATnormalNode(right);
00572     right = SATnodeID(right);
00573     right = inverted ? -right : right;
00574 
00575     j = SATnodeID(i);
00576 
00577     fprintf(fout, "%ld %ld %ld 0\n", -left, -right, j);
00578     fprintf(fout, "%ld %ld 0\n", left, -j);
00579     fprintf(fout, "%ld %ld 0\n", right, -j);
00580   }
00581 
00582   fclose(fout);
00583 }
00584 
00596 void
00597 sat_WriteCNFWithPointer(satManager_t *cm, FILE *fout)
00598 {
00599 long i, j, size, tv, *plit;
00600 int csize, inverted;
00601 int nVar, nCl;
00602 long left, right;
00603 
00604   nVar = cm->initNumVariables;
00605   nCl = 0;
00606   size = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict;
00607   for(i=satNodeSize; i<size; i+=satNodeSize) {
00608     if(SATleftChild(i) == 2 && SATrightChild(i) == 2)   continue;
00609     if(SATflags(i) & IsCNFMask) {
00610       if(SATreadInUse(i) == 0)  continue;
00611       nCl++;
00612       continue;
00613     }
00614     if(!(SATflags(i) & CoiMask))        continue;
00615     nCl += 3;
00616   }
00617   sat_CountUnitLiteralClauses(cm, cm->assertion, &nCl);
00618   sat_CountUnitLiteralClauses(cm, cm->unitLits, &nCl);
00619   sat_CountUnitLiteralClauses(cm, cm->auxObj, &nCl);
00620   sat_CountUnitLiteralClauses(cm, cm->obj, &nCl);
00621 
00622   fprintf(fout, "p cnf %d %d\n", nVar, nCl);
00623 
00624   sat_PrintUnitLiteralClauses(cm, cm->assertion, fout);
00625   sat_PrintUnitLiteralClauses(cm, cm->unitLits, fout);
00626   sat_PrintUnitLiteralClauses(cm, cm->auxObj, fout);
00627   sat_PrintUnitLiteralClauses(cm, cm->obj, fout);
00628 
00629   size = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict;
00630   for(i=satNodeSize; i<size; i+=satNodeSize) {
00631     if(SATleftChild(i) == 2 && SATrightChild(i) == 2)   continue;
00632     if(SATflags(i) & IsCNFMask) {
00633       csize = SATnumLits(i);
00634       plit = (long*)SATfirstLit(i);
00635       for(j=0; j<csize; j++, plit++) {
00636          tv = SATgetNode(*plit);
00637          inverted = SATisInverted(tv);
00638          tv = SATnormalNode(tv);
00639          tv = SATnodeID(tv);
00640          fprintf(fout, "%ld ", inverted ? -tv : tv);
00641       }
00642       fprintf(fout, "0\n");
00643       continue;
00644     }
00645     if(!(SATflags(i) & CoiMask))        continue;
00646 
00647 
00648     left = SATleftChild(i);
00649     inverted = SATisInverted(left);
00650     left = SATnormalNode(left);
00651     left = SATnodeID(left);
00652     left = inverted ? -left : left;
00653 
00654     right = SATrightChild(i);
00655     inverted = SATisInverted(right);
00656     right = SATnormalNode(right);
00657     right = SATnodeID(right);
00658     right = inverted ? -right : right;
00659 
00660     j = SATnodeID(i);
00661 
00662     fprintf(fout, "%ld %ld %ld 0\n", -left, -right, j);
00663     fprintf(fout, "%ld %ld 0\n", left, -j);
00664     fprintf(fout, "%ld %ld 0\n", right, -j);
00665   }
00666 
00667 }
00679 void
00680 sat_CountUnitLiteralClauses(
00681         satManager_t *cm,
00682         satArray_t *arr,
00683         int *nCl)
00684 {
00685 int i, count;
00686 long v;
00687 
00688   if(arr == 0)  return;
00689   count = 0;
00690   for(i=0; i<arr->num; i++) {
00691     v = arr->space[i];
00692     if(v == 1)  count++;
00693   }
00694 
00695   *nCl += arr->num - count;
00696 }
00697 
00709 void
00710 sat_PrintUnitLiteralClauses(
00711         satManager_t *cm,
00712         satArray_t *arr,
00713         FILE *fout)
00714 {
00715 int i, inverted;
00716 long v;
00717 
00718   if(arr == 0)  return;
00719   for(i=0; i<arr->num; i++) {
00720     v = arr->space[i];
00721     if(v == 1)  continue;
00722     inverted = SATisInverted(v);
00723     v = SATnormalNode(v);
00724     v = SATnodeID(v);
00725     fprintf(fout, "%ld 0\n", inverted ? -v : v);
00726   }
00727 }