zchaff64/zminimal.cpp

   1 // *********************************************************************
   2 // Copyright 2000-2004, Princeton University.  All rights reserved.
   3 // By using this software the USER indicates that he or she has read,
   4 // understood and will comply with the following:
   5 //
   6 // --- Princeton University hereby grants USER nonexclusive permission
   7 // to use, copy and/or modify this software for internal, noncommercial,
   8 // research purposes only. Any distribution, including commercial sale
   9 // or license, of this software, copies of the software, its associated
  10 // documentation and/or modifications of either is strictly prohibited
  11 // without the prior consent of Princeton University.  Title to copyright
  12 // to this software and its associated documentation shall at all times
  13 // remain with Princeton University.  Appropriate copyright notice shall
  14 // be placed on all software copies, and a complete copy of this notice
  15 // shall be included in all copies of the associated documentation.
  16 // No right is  granted to use in advertising, publicity or otherwise
  17 // any trademark,  service mark, or the name of Princeton University.
  18 //
  19 //
  20 // --- This software and any associated documentation is provided "as is"
  21 //
  22 // PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS
  23 // OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A
  24 // PARTICULAR PURPOSE, OR THAT  USE OF THE SOFTWARE, MODIFICATIONS, OR
  25 // ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS,
  26 // TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.
  27 //
  28 // Princeton University shall not be liable under any circumstances for
  29 // any direct, indirect, special, incidental, or consequential damages
  30 // with respect to any claim by USER or any third party on account of
  31 // or arising from the use, or inability to use, this software or its
  32 // associated documentation, even if Princeton University has been advised
  33 // of the possibility of those damages.
  34 // *********************************************************************
  35
  36 #include <iostream>
  37 #include <fstream>
  38 #include <cstdlib>
  39 #include <cstdio>
  40 #include <set>
  41 #include <vector>
  42
  43 using namespace std;
  44
  45 #include "SAT.h"
  46
  47 const int MAX_LINE_LENGTH       = 65536;
  48 const int MAX_WORD_LENGTH       = 64;
  49
  50 void read_cnf_omit(SAT_Manager mng, char * filename, vector<int> & omit) {
  51   char line_buffer[MAX_LINE_LENGTH];
  52   char word_buffer[MAX_WORD_LENGTH];
  53   set<int> clause_vars;
  54   set<int> clause_lits;
  55   unsigned omit_idx = 0;
  56   int line_num = 0;
  57   ifstream inp(filename, ios::in);
  58   if (!inp) {
  59     cerr << "Can't open input file" << endl;
  60     exit(1);
  61   }
  62   int cl_id = -1;
  63   while (inp.getline(line_buffer, MAX_LINE_LENGTH)) {
  64     ++line_num;
  65     if (line_buffer[0] == 'c') {
  66       continue;
  67     }
  68     else if (line_buffer[0] == 'p') {
  69       int var_num;
  70       int cl_num;
  71       int arg = sscanf(line_buffer, "p cnf %d %d", &var_num, &cl_num);
  72       if (arg < 2) {
  73         cerr << "Unable to read number of variables and clauses"
  74              << "at line " << line_num << endl;
  75         exit(3);
  76       }
  77       SAT_SetNumVariables(mng, var_num);  // first element not used.
  78     } else {                             // Clause definition or continuation
  79       char *lp = line_buffer;
  80       do {
  81         char *wp = word_buffer;
  82         while (*lp && ((*lp == ' ') || (*lp == '\t'))) {
  83           lp++;
  84         }
  85         while (*lp && (*lp != ' ') && (*lp != '\t') && (*lp != '\n')) {
  86           *(wp++) = *(lp++);
  87         }
  88         *wp = '\0';                                 // terminate string
  89
  90         if (strlen(word_buffer) != 0) {     // check if number is there
  91           int var_idx = atoi(word_buffer);
  92           int sign = 0;
  93
  94           if (var_idx != 0) {
  95             if (var_idx < 0) {
  96               var_idx = -var_idx;
  97               sign = 1;
  98             }
  99             clause_vars.insert(var_idx);
 100             clause_lits.insert((var_idx << 1) + sign);
 101           } else {
 102             // add this clause
 103             ++cl_id;
 104             if (omit_idx < omit.size()-1 && omit[omit_idx] < cl_id )
 105               ++omit_idx;
 106             if (omit_idx < omit.size()) {
 107               if (omit[omit_idx] == cl_id) {
 108                 clause_lits.clear();
 109                 clause_vars.clear();
 110               }
 111             }
 112             if (clause_vars.size() != 0 &&
 113                 clause_vars.size() == clause_lits.size()) {
 114               vector <int> temp;
 115               for (set<int>::iterator itr = clause_lits.begin();
 116                    itr != clause_lits.end(); ++itr) {
 117                 temp.push_back(*itr);
 118               }
 119               SAT_AddClause(mng, & temp.begin()[0], temp.size() );
 120             }
 121             clause_lits.clear();
 122             clause_vars.clear();
 123           }
 124         }
 125       }
 126       while (*lp);
 127     }
 128   }
 129   if (!inp.eof()) {
 130     cerr << "Input line " << line_num << " too long. Unable to continue..."
 131          << endl;
 132     exit(2);
 133   }
 134
 135   if (clause_lits.size() && clause_vars.size() == clause_lits.size()) {
 136     vector <int> temp;
 137     for (set<int>::iterator itr = clause_lits.begin();
 138          itr != clause_lits.end(); ++itr) {
 139       temp.push_back(*itr);
 140     }
 141     SAT_AddClause(mng, & temp.begin()[0], temp.size() );
 142   }
 143   clause_lits.clear();
 144   clause_vars.clear();
 145 }
 146
 147 int get_num_clause(char * filename) {
 148   char line_buffer[MAX_LINE_LENGTH];
 149   ifstream inp(filename, ios::in);
 150   if (!inp) {
 151     cerr << "Can't open input file" << endl;
 152     exit(1);
 153   }
 154   while (inp.getline(line_buffer, MAX_LINE_LENGTH)) {
 155     if (inp.fail()) {
 156       cerr << "Too large an input line. Unable to continue..." << endl;
 157       exit(2);
 158     }
 159     if (line_buffer[0] == 'p') {
 160       int var_num;
 161       int cl_num;
 162       int arg = sscanf(line_buffer, "p cnf %d %d", &var_num, &cl_num);
 163       if (arg < 2) {
 164         cerr << "Unable to read number of variables and clauses" << endl;
 165         exit(3);
 166       }
 167       return cl_num;
 168     }
 169   }
 170   cerr << "Can't find the header in CNF:  p cnf NumVar NumCls " << endl;
 171   exit(1);
 172   return 0;
 173 }
 174
 175 void handle_result(SAT_Manager mng, int outcome, char * filename) {
 176   char * result = "UNKNOWN";
 177   switch (outcome) {
 178     case SATISFIABLE:
 179       cout << "Instance satisfiable" << endl;
 180       // following lines will print out a solution if a solution exist
 181       for (unsigned i = 1, sz = SAT_NumVariables(mng); i <= sz; ++i) {
 182         switch (SAT_GetVarAsgnment(mng, i)) {
 183           case -1:
 184             cout << "(" << i<< ")";
 185             break;
 186           case 0:
 187             cout << "-" << i;
 188             break;
 189           case 1:
 190             cout << i;
 191             break;
 192           default:
 193             cerr << "Unknown variable value state"<< endl;
 194             exit(4);
 195         }
 196         cout << " ";
 197       }
 198       result  = "SAT";
 199       cout << endl;
 200       break;
 201     case UNSATISFIABLE:
 202       result  = "UNSAT";
 203       cout << "Instance unsatisfiable" << endl;
 204       break;
 205     case TIME_OUT:
 206       result  = "ABORT : TIME OUT";
 207       cout << "Time out, unable to determine the outcome of the instance";
 208       cout << endl;
 209       break;
 210     case MEM_OUT:
 211       result  = "ABORT : MEM OUT";
 212       cout << "Memory out, unable to determine the outcome of the instance";
 213       cout << endl;
 214       break;
 215     default:
 216       cerr << "Unknown outcome" << endl;
 217       exit(5);
 218   }
 219   cout << "Max Decision Level\t\t\t" << SAT_MaxDLevel(mng) << endl;
 220   cout << "Num. of Decisions\t\t\t" << SAT_NumDecisions(mng) << endl;
 221   cout << "Num. of Variables\t\t\t" << SAT_NumVariables(mng) << endl;
 222   cout << "Original Num Clauses\t\t\t" << SAT_InitNumClauses(mng) << endl;
 223   cout << "Original Num Literals\t\t\t" << SAT_InitNumLiterals(mng) << endl;
 224   cout << "Added Conflict Clauses\t\t\t" << SAT_NumAddedClauses(mng) -
 225                                             SAT_InitNumClauses(mng)<< endl;
 226   cout << "Added Conflict Literals\t\t\t" << SAT_NumAddedLiterals(mng) -
 227                                              SAT_InitNumLiterals(mng) << endl;
 228   cout << "Deleted Unrelevant clause\t\t" << SAT_NumDeletedClauses(mng) <<endl;
 229   cout << "Deleted Unrelevant literals\t\t" <<SAT_NumDeletedLiterals(mng) <<endl;
 230   cout << "Number of Implication\t\t\t" << SAT_NumImplications(mng)<< endl;
 231
 232   // other statistics comes here
 233   cout << "Total Run Time\t\t\t\t" << SAT_GetCPUTime(mng) << endl << endl;
 234   cout  << result << endl;
 235 }
 236
 237 void output_status(SAT_Manager mng) {
 238   cout << "Dec: " << SAT_NumDecisions(mng) << "\t ";
 239   cout << "AddCl: " << SAT_NumAddedClauses(mng) << "\t";
 240   cout << "AddLit: " << SAT_NumAddedLiterals(mng) << "\t";
 241   cout << "DelCl: " << SAT_NumDeletedClauses(mng) << "\t";
 242   cout << "DelLit: " << SAT_NumDeletedLiterals(mng) << "\t";
 243   cout << "NumImp: " << SAT_NumImplications(mng) << "\t";
 244   cout << "AveBubbleMove: " << SAT_AverageBubbleMove(mng) << "\t";
 245   // other statistics comes here
 246   cout << "RunTime:" << SAT_GetElapsedCPUTime(mng) << endl;
 247 }
 248
 249 void verify_solution(SAT_Manager mng) {
 250   int num_verified = 0;
 251   for (int cl_idx = SAT_GetFirstClause (mng); cl_idx >= 0;
 252        cl_idx = SAT_GetNextClause(mng, cl_idx)) {
 253     int len = SAT_GetClauseNumLits(mng, cl_idx);
 254     int * lits = new int[len+1];
 255     SAT_GetClauseLits(mng, cl_idx, lits);
 256     int i;
 257     for (i = 0; i < len; ++i) {
 258       int v_idx = lits[i] >> 1;
 259       int sign = lits[i] & 0x1;
 260       int var_value = SAT_GetVarAsgnment(mng, v_idx);
 261       if ((var_value == 1 && sign == 0) ||
 262           (var_value == 0 && sign == 1))
 263         break;
 264     }
 265     if (i >= len) {
 266       cerr << "Verify Satisfiable solution failed, please "
 267            << "file a bug report, thanks. " << endl;
 268       exit(6);
 269     }
 270     delete [] lits;
 271       ++num_verified;
 272   }
 273   cout << num_verified << " Clauses are true, Verify Solution successful. ";
 274 }
 275
 276 int main(int argc, char ** argv) {
 277   if (argc != 2) {
 278     cerr << "ZMinimal: Find Minimal Core. " << endl;
 279     cerr << "Copyright 2003-2004, Princeton University" << endl << endl;
 280     cerr << "Usage: "<< argv[0] << " cnf_file " << endl;
 281     return 2;
 282   }
 283   vector<int> omit;
 284   int num_cls = get_num_clause(argv[1]);
 285   cout << "Total : " << num_cls << " passes";
 286   for (int i = 0; i < num_cls; ++i) {
 287     if (i % 50 == 0)
 288       cout << endl << i << ":\t";
 289     if (i % 10 == 0)
 290       cout << " ";
 291     cout.flush();
 292     SAT_Manager mng = SAT_InitManager();
 293     omit.push_back(i);
 294     read_cnf_omit(mng, argv[1], omit);
 295     int result = SAT_Solve(mng);
 296     if (result != SATISFIABLE) {
 297       cout << "*" ;
 298     } else {
 299       cout << "-";
 300       omit.pop_back();
 301     }
 302     cout.flush();
 303     SAT_ReleaseManager(mng);
 304   }
 305   cout << endl;
 306   cout << "Instance Cls: " << num_cls << "  MinCore Cls: "
 307        << num_cls - omit.size() << " Diff: " << omit.size() << endl;
 308   cout << "Unneeded clauses are: ";
 309   for (unsigned i = 0; i < omit.size(); ++i) {
 310     if (i % 20 == 0)
 311       cout << endl;
 312     cout << omit[i] << " ";
 313   }
 314   cout << endl;
 315   return 0;
 316 }