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:
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.
20 // --- This software and any associated documentation is provided "as is"
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.
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 // *********************************************************************
47 const int MAX_LINE_LENGTH = 65536;
48 const int MAX_WORD_LENGTH = 64;
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];
55 unsigned omit_idx = 0;
57 ifstream inp(filename, ios::in);
59 cerr << "Can't open input file" << endl;
63 while (inp.getline(line_buffer, MAX_LINE_LENGTH)) {
65 if (line_buffer[0] == 'c') {
68 else if (line_buffer[0] == 'p') {
71 int arg = sscanf(line_buffer, "p cnf %d %d", &var_num, &cl_num);
73 cerr << "Unable to read number of variables and clauses"
74 << "at line " << line_num << endl;
77 SAT_SetNumVariables(mng, var_num); // first element not used.
78 } else { // Clause definition or continuation
79 char *lp = line_buffer;
81 char *wp = word_buffer;
82 while (*lp && ((*lp == ' ') || (*lp == '\t'))) {
85 while (*lp && (*lp != ' ') && (*lp != '\t') && (*lp != '\n')) {
88 *wp = '\0'; // terminate string
90 if (strlen(word_buffer) != 0) { // check if number is there
91 int var_idx = atoi(word_buffer);
99 clause_vars.insert(var_idx);
100 clause_lits.insert((var_idx << 1) + sign);
104 if (omit_idx < omit.size()-1 && omit[omit_idx] < cl_id )
106 if (omit_idx < omit.size()) {
107 if (omit[omit_idx] == cl_id) {
112 if (clause_vars.size() != 0 &&
113 clause_vars.size() == clause_lits.size()) {
115 for (set<int>::iterator itr = clause_lits.begin();
116 itr != clause_lits.end(); ++itr) {
117 temp.push_back(*itr);
119 SAT_AddClause(mng, & temp.begin()[0], temp.size() );
130 cerr << "Input line " << line_num << " too long. Unable to continue..."
135 if (clause_lits.size() && clause_vars.size() == clause_lits.size()) {
137 for (set<int>::iterator itr = clause_lits.begin();
138 itr != clause_lits.end(); ++itr) {
139 temp.push_back(*itr);
141 SAT_AddClause(mng, & temp.begin()[0], temp.size() );
147 int get_num_clause(char * filename) {
148 char line_buffer[MAX_LINE_LENGTH];
149 ifstream inp(filename, ios::in);
151 cerr << "Can't open input file" << endl;
154 while (inp.getline(line_buffer, MAX_LINE_LENGTH)) {
156 cerr << "Too large an input line. Unable to continue..." << endl;
159 if (line_buffer[0] == 'p') {
162 int arg = sscanf(line_buffer, "p cnf %d %d", &var_num, &cl_num);
164 cerr << "Unable to read number of variables and clauses" << endl;
170 cerr << "Can't find the header in CNF: p cnf NumVar NumCls " << endl;
175 void handle_result(SAT_Manager mng, int outcome, char * filename) {
176 char * result = "UNKNOWN";
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)) {
184 cout << "(" << i<< ")";
193 cerr << "Unknown variable value state"<< endl;
203 cout << "Instance unsatisfiable" << endl;
206 result = "ABORT : TIME OUT";
207 cout << "Time out, unable to determine the outcome of the instance";
211 result = "ABORT : MEM OUT";
212 cout << "Memory out, unable to determine the outcome of the instance";
216 cerr << "Unknown outcome" << endl;
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;
232 // other statistics comes here
233 cout << "Total Run Time\t\t\t\t" << SAT_GetCPUTime(mng) << endl << endl;
234 cout << result << endl;
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;
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);
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))
266 cerr << "Verify Satisfiable solution failed, please "
267 << "file a bug report, thanks. " << endl;
273 cout << num_verified << " Clauses are true, Verify Solution successful. ";
276 int main(int argc, char ** argv) {
278 cerr << "ZMinimal: Find Minimal Core. " << endl;
279 cerr << "Copyright 2003-2004, Princeton University" << endl << endl;
280 cerr << "Usage: "<< argv[0] << " cnf_file " << endl;
284 int num_cls = get_num_clause(argv[1]);
285 cout << "Total : " << num_cls << " passes";
286 for (int i = 0; i < num_cls; ++i) {
288 cout << endl << i << ":\t";
292 SAT_Manager mng = SAT_InitManager();
294 read_cnf_omit(mng, argv[1], omit);
295 int result = SAT_Solve(mng);
296 if (result != SATISFIABLE) {
303 SAT_ReleaseManager(mng);
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) {
312 cout << omit[i] << " ";