1 /* =========FOR INTERNAL USE ONLY. NO DISTRIBUTION PLEASE ========== */
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:
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.
22 --- This software and any associated documentation is provided "as is"
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.
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 *********************************************************************/
49 const int MAX_LINE_LENGTH = 65536;
50 const int MAX_WORD_LENGTH = 64;
52 //This cnf parser function is based on the GRASP code by Joao Marques Silva
53 void read_cnf(SAT_Manager mng, char * filename )
55 // cout <<"read cnf "<<endl;
56 char line_buffer[MAX_LINE_LENGTH];
57 char word_buffer[MAX_WORD_LENGTH];
62 if(opendir(filename)){
63 cerr << "Can't open input file, it's a directory" << endl;
67 ifstream inp (filename, ios::in);
69 cerr << "Can't open input file" << endl;
72 while (inp.getline(line_buffer, MAX_LINE_LENGTH)) {
74 if (line_buffer[0] == 'c') {
77 else if (line_buffer[0] == 'p') {
81 int arg = sscanf (line_buffer, "p cnf %d %d", &var_num, &cl_num);
83 cerr << "Unable to read number of variables and clauses"
84 << "at line " << line_num << endl;
87 SAT_SetNumVariables(mng, var_num); //first element not used.
89 else { // Clause definition or continuation
90 char *lp = line_buffer;
92 char *wp = word_buffer;
93 while (*lp && ((*lp == ' ') || (*lp == '\t'))) {
96 while (*lp && (*lp != ' ') && (*lp != '\t') && (*lp != '\n')) {
99 *wp = '\0'; // terminate string
101 if (strlen(word_buffer) != 0) { // check if number is there
102 int var_idx = atoi (word_buffer);
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);
112 if (clause_vars.size() != 0 && (clause_vars.size() == clause_lits.size())) { //yeah, can add this clause
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() );
119 else {} //it contain var of both polarity, so is automatically satisfied, just skip it
129 cerr << "Input line " << line_num << " too long. Unable to continue..." << endl;
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() ) {
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() );
142 // cout <<"done read cnf"<<endl;
146 void handle_result(SAT_Manager mng, int outcome, char * filename )
148 char * result = "UNKNOWN";
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)) {
156 cout <<"("<< i<<")"; break;
158 cout << "-" << i; break;
162 cerr << "Unknown variable value state"<< endl;
171 cout << "Instance Unsatisfiable" << endl;
174 result = "ABORT : TIME OUT";
175 cout << "Time out, unable to determine the satisfiability of the instance"<<endl;
178 result = "ABORT : MEM OUT";
179 cout << "Memory out, unable to determine the satisfiability of the instance"<<endl;
182 cerr << "Unknown outcome" << endl;
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;
207 void output_status(SAT_Manager mng)
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;
220 void verify_solution(SAT_Manager mng)
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);
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;
237 cerr << "Verify Satisfiable solution failed, please file a bug report, thanks. " << endl;
243 cout <<"c "<< num_verified << " Clauses are true, Verify Solution successful."<<endl;;
246 int main(int argc, char ** argv)
248 SAT_Manager mng = SAT_InitManager();
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;
255 cout << "Z-Chaff Version: " << SAT_Version(mng) << endl;
256 cout << "Solving " << argv[1] << " ......" << endl;
258 read_cnf (mng, argv[1] );
261 read_cnf (mng, argv[1] );
262 SAT_SetTimeLimit(mng, atoi(argv[2]));
265 /* if you want some statistics during the solving, uncomment following line */
266 // SAT_AddHookFun(mng,output_status, 5000);
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);
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]);