zchaff64/sat_solver.cpp

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