source: vis_dev/zchaff/zminimal.cpp @ 82

Last change on this file since 82 was 10, checked in by cecile, 13 years ago

Zchaff

File size: 10.6 KB
Line 
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 <cstring>
41#include <set>
42#include <vector>
43
44using namespace std;
45
46#include "SAT.h"
47
48const int MAX_LINE_LENGTH       = 65536;
49const int MAX_WORD_LENGTH       = 64;
50
51void read_cnf_omit(SAT_Manager mng, char * filename, vector<int> & omit) {
52  char line_buffer[MAX_LINE_LENGTH];
53  char word_buffer[MAX_WORD_LENGTH];
54  set<int> clause_vars;
55  set<int> clause_lits;
56  unsigned omit_idx = 0;
57  int line_num = 0;
58  ifstream inp(filename, ios::in);
59  if (!inp) {
60    cerr << "Can't open input file" << endl;
61    exit(1);
62  }
63  int cl_id = -1;
64  while (inp.getline(line_buffer, MAX_LINE_LENGTH)) {
65    ++line_num;
66    if (line_buffer[0] == 'c') {
67      continue;
68    }
69    else if (line_buffer[0] == 'p') {
70      int var_num;
71      int cl_num;
72      int arg = sscanf(line_buffer, "p cnf %d %d", &var_num, &cl_num);
73      if (arg < 2) {
74        cerr << "Unable to read number of variables and clauses"
75             << "at line " << line_num << endl;
76        exit(3);
77      }
78      SAT_SetNumVariables(mng, var_num);  // first element not used.
79    } else {                             // Clause definition or continuation
80      char *lp = line_buffer;
81      do {
82        char *wp = word_buffer;
83        while (*lp && ((*lp == ' ') || (*lp == '\t'))) {
84          lp++;
85        }
86        while (*lp && (*lp != ' ') && (*lp != '\t') && (*lp != '\n')) {
87          *(wp++) = *(lp++);
88        }
89        *wp = '\0';                                 // terminate string
90
91        if (strlen(word_buffer) != 0) {     // check if number is there
92          int var_idx = atoi(word_buffer);
93          int sign = 0;
94
95          if (var_idx != 0) {
96            if (var_idx < 0) {
97              var_idx = -var_idx;
98              sign = 1;
99            }
100            clause_vars.insert(var_idx);
101            clause_lits.insert((var_idx << 1) + sign);
102          } else {
103            // add this clause
104            ++cl_id;
105            if (omit_idx < omit.size()-1 && omit[omit_idx] < cl_id )
106              ++omit_idx;
107            if (omit_idx < omit.size()) {
108              if (omit[omit_idx] == cl_id) {
109                clause_lits.clear();
110                clause_vars.clear();
111              }
112            }
113            if (clause_vars.size() != 0 &&
114                clause_vars.size() == clause_lits.size()) {
115              vector <int> temp;
116              for (set<int>::iterator itr = clause_lits.begin();
117                   itr != clause_lits.end(); ++itr) {
118                temp.push_back(*itr);
119              }
120              SAT_AddClause(mng, & temp.begin()[0], temp.size() );
121            }
122            clause_lits.clear();
123            clause_vars.clear();
124          }
125        }
126      }
127      while (*lp);
128    }
129  }
130  if (!inp.eof()) {
131    cerr << "Input line " << line_num << " too long. Unable to continue..."
132         << endl;
133    exit(2);
134  }
135
136  if (clause_lits.size() && clause_vars.size() == clause_lits.size()) {
137    vector <int> temp;
138    for (set<int>::iterator itr = clause_lits.begin();
139         itr != clause_lits.end(); ++itr) {
140      temp.push_back(*itr);
141    }
142    SAT_AddClause(mng, & temp.begin()[0], temp.size() );
143  }
144  clause_lits.clear();
145  clause_vars.clear();
146}
147
148int get_num_clause(char * filename) {
149  char line_buffer[MAX_LINE_LENGTH];
150  ifstream inp(filename, ios::in);
151  if (!inp) {
152    cerr << "Can't open input file" << endl;
153    exit(1);
154  }
155  while (inp.getline(line_buffer, MAX_LINE_LENGTH)) {
156    if (inp.fail()) {
157      cerr << "Too large an input line. Unable to continue..." << endl;
158      exit(2);
159    }
160    if (line_buffer[0] == 'p') {
161      int var_num;
162      int cl_num;
163      int arg = sscanf(line_buffer, "p cnf %d %d", &var_num, &cl_num);
164      if (arg < 2) {
165        cerr << "Unable to read number of variables and clauses" << endl;
166        exit(3);
167      }
168      return cl_num;
169    }
170  }
171  cerr << "Can't find the header in CNF:  p cnf NumVar NumCls " << endl;
172  exit(1);
173  return 0;
174}
175
176void handle_result(SAT_Manager mng, int outcome, char * filename) {
177  string result = "UNKNOWN";
178  switch (outcome) {
179    case SATISFIABLE:
180      cout << "Instance satisfiable" << endl;
181      // following lines will print out a solution if a solution exist
182      for (unsigned i = 1, sz = SAT_NumVariables(mng); i <= sz; ++i) {
183        switch (SAT_GetVarAsgnment(mng, i)) {
184          case -1:
185            cout << "(" << i<< ")";
186            break;
187          case 0:
188            cout << "-" << i;
189            break;
190          case 1:
191            cout << i;
192            break;
193          default:
194            cerr << "Unknown variable value state"<< endl;
195            exit(4);
196        }
197        cout << " ";
198      }
199      result  = "SAT";
200      cout << endl;
201      break;
202    case UNSATISFIABLE:
203      result  = "UNSAT";
204      cout << "Instance unsatisfiable" << endl;
205      break;
206    case TIME_OUT:
207      result  = "ABORT : TIME OUT";
208      cout << "Time out, unable to determine the outcome of the instance";
209      cout << endl;
210      break;
211    case MEM_OUT:
212      result  = "ABORT : MEM OUT";
213      cout << "Memory out, unable to determine the outcome of the instance";
214      cout << endl;
215      break;
216    default:
217      cerr << "Unknown outcome" << endl;
218      exit(5);
219  }
220  cout << "Max Decision Level\t\t\t" << SAT_MaxDLevel(mng) << endl;
221  cout << "Num. of Decisions\t\t\t" << SAT_NumDecisions(mng) << endl;
222  cout << "Num. of Variables\t\t\t" << SAT_NumVariables(mng) << endl;
223  cout << "Original Num Clauses\t\t\t" << SAT_InitNumClauses(mng) << endl;
224  cout << "Original Num Literals\t\t\t" << SAT_InitNumLiterals(mng) << endl;
225  cout << "Added Conflict Clauses\t\t\t" << SAT_NumAddedClauses(mng) -
226                                            SAT_InitNumClauses(mng)<< endl;
227  cout << "Added Conflict Literals\t\t\t" << SAT_NumAddedLiterals(mng) -
228                                             SAT_InitNumLiterals(mng) << endl;
229  cout << "Deleted Unrelevant clause\t\t" << SAT_NumDeletedClauses(mng) <<endl;
230  cout << "Deleted Unrelevant literals\t\t" <<SAT_NumDeletedLiterals(mng) <<endl;
231  cout << "Number of Implication\t\t\t" << SAT_NumImplications(mng)<< endl;
232
233  // other statistics comes here
234  cout << "Total Run Time\t\t\t\t" << SAT_GetCPUTime(mng) << endl << endl;
235  cout  << result << endl;
236}
237
238void output_status(SAT_Manager mng) {
239  cout << "Dec: " << SAT_NumDecisions(mng) << "\t ";
240  cout << "AddCl: " << SAT_NumAddedClauses(mng) << "\t";
241  cout << "AddLit: " << SAT_NumAddedLiterals(mng) << "\t";
242  cout << "DelCl: " << SAT_NumDeletedClauses(mng) << "\t";
243  cout << "DelLit: " << SAT_NumDeletedLiterals(mng) << "\t";
244  cout << "NumImp: " << SAT_NumImplications(mng) << "\t";
245  cout << "AveBubbleMove: " << SAT_AverageBubbleMove(mng) << "\t";
246  // other statistics comes here
247  cout << "RunTime:" << SAT_GetElapsedCPUTime(mng) << endl;
248}
249
250void verify_solution(SAT_Manager mng) {
251  int num_verified = 0;
252  for (int cl_idx = SAT_GetFirstClause (mng); cl_idx >= 0;
253       cl_idx = SAT_GetNextClause(mng, cl_idx)) {
254    int len = SAT_GetClauseNumLits(mng, cl_idx);
255    int * lits = new int[len+1];
256    SAT_GetClauseLits(mng, cl_idx, lits);
257    int i;
258    for (i = 0; i < len; ++i) {
259      int v_idx = lits[i] >> 1;
260      int sign = lits[i] & 0x1;
261      int var_value = SAT_GetVarAsgnment(mng, v_idx);
262      if ((var_value == 1 && sign == 0) ||
263          (var_value == 0 && sign == 1))
264        break;
265    }
266    if (i >= len) {
267      cerr << "Verify Satisfiable solution failed, please "
268           << "file a bug report, thanks. " << endl;
269      exit(6);
270    }
271    delete [] lits;
272      ++num_verified;
273  }
274  cout << num_verified << " Clauses are true, Verify Solution successful. ";
275}
276
277int main(int argc, char ** argv) {
278  if (argc != 2) {
279    cerr << "ZMinimal: Find Minimal Core. " << endl;
280    cerr << "Copyright 2003-2004, Princeton University" << endl << endl;
281    cerr << "Usage: "<< argv[0] << " cnf_file " << endl;
282    return 2;
283  }
284  vector<int> omit;
285  int num_cls = get_num_clause(argv[1]);
286  cout << "Total : " << num_cls << " passes";
287  for (int i = 0; i < num_cls; ++i) {
288    if (i % 50 == 0)
289      cout << endl << i << ":\t";
290    if (i % 10 == 0)
291      cout << " ";
292    cout.flush();
293    SAT_Manager mng = SAT_InitManager();
294    omit.push_back(i);
295    read_cnf_omit(mng, argv[1], omit);
296    int result = SAT_Solve(mng);
297    if (result != SATISFIABLE) {
298      cout << "*" ;
299    } else {
300      cout << "-";
301      omit.pop_back();
302    }
303    cout.flush();
304    SAT_ReleaseManager(mng);
305  }
306  cout << endl;
307  cout << "Instance Cls: " << num_cls << "  MinCore Cls: "
308       << num_cls - omit.size() << " Diff: " << omit.size() << endl;
309  cout << "Unneeded clauses are: ";
310  for (unsigned i = 0; i < omit.size(); ++i) {
311    if (i % 20 == 0)
312      cout << endl;
313    cout << omit[i] << " ";
314  }
315  cout << endl;
316  return 0;
317}
Note: See TracBrowser for help on using the repository browser.