1/******************************************************************************************[Main.C] 2MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson 3 4Permission is hereby granted, free of charge, to any person obtaining a copy of this software and 5associated documentation files (the "Software"), to deal in the Software without restriction, 6including without limitation the rights to use, copy, modify, merge, publish, distribute, 7sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is 8furnished to do so, subject to the following conditions: 9 10The above copyright notice and this permission notice shall be included in all copies or 11substantial portions of the Software. 12 13THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT 14NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND 15NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, 16DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT 17OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. 18**************************************************************************************************/ 19 20#include "Solver.h" 21#include <ctime> 22#include <unistd.h> 23#include <signal.h> 24#include <iostream> 25#include <fstream> 26 27//================================================================================================= 28// DIMACS Parser: // Inserts problem into solver. 29 30using namespace std; 31 32void addLit(int parsed_lit,Solver& S, vec<Lit>& lits) { 33 int var = abs(parsed_lit)-1; 34 while (var >= S.nVars()) S.newVar(); 35 lits.push( (parsed_lit > 0) ? Lit(var) : ~Lit(var) ); 36} 37 38void addClause(Solver& S, vec<Lit>& lits) { 39 /*for (int i=0;i<lits.size();i++) 40 cout << (sign(lits[i]) ? "-" : "") << (var(lits[i])+1) << " "; 41 cout << "#" << endl;*/ 42 S.addClause(lits); 43 lits.clear(); 44} 45 46static void parse_DIMACS(char* filename, Solver& S) { 47 ifstream fin(filename); 48 if (fin.fail()) { cerr << "Error opening input file " << filename << endl; exit(1); } 49 string line,stok; 50 int itok; 51 vec<Lit> lits; 52 while(true) { // skip preamble (must have at least the p line) 53 fin >> stok; 54 if (stok=="c" || stok=="p") getline(fin,line); 55 else break; 56 } 57 addLit(atoi(stok.c_str()),S,lits); // first lit of first clause 58 while (true) { 59 fin >> itok; 60 if (fin.eof()) { 61 if (lits.size()>0) addClause(S,lits); // in case last clause had no trailing 0 62 break; 63 } 64 if (itok==0) addClause(S,lits); 65 else addLit(itok,S,lits); 66 } 67} 68//================================================================================================= 69 70 71void printStats(SolverStats& stats, double& cpu_time, int64& mem_used) 72{ 73 cpu_time = cpuTime(); 74 mem_used = memUsed(); 75 reportf("restarts : %"I64_fmt"\n", stats.starts); 76 reportf("conflicts : %-12"I64_fmt" (%.0f /sec)\n", stats.conflicts , stats.conflicts /cpu_time); 77 reportf("decisions : %-12"I64_fmt" (%.0f /sec)\n", stats.decisions , stats.decisions /cpu_time); 78 reportf("propagations : %-12"I64_fmt" (%.0f /sec)\n", stats.propagations, stats.propagations/cpu_time); 79 reportf("conflict literals : %-12"I64_fmt" (%4.2f %% deleted)\n", stats.tot_literals, (stats.max_literals - stats.tot_literals)*100 / (double)stats.max_literals); 80 if (mem_used != 0) reportf("Memory used : %.2f MB\n", mem_used / 1048576.0); 81 reportf("CPU time : %g s\n", cpu_time); 82} 83 84void printProofStats(double cpu_time, int64 mem_used) { 85 double cpu_time1 = cpuTime(); 86 int64 mem_used1 = memUsed(); 87 if (mem_used1!= 0) reportf("Extra memory used : %.2f MB\n", 88 (mem_used1-mem_used)/1048576.0); 89 reportf("Extra CPU time : %g s\n", (cpu_time1-cpu_time)); 90} 91 92Solver* solver; 93static void SIGINT_handler(int signum) { 94 reportf("\n"); reportf("*** INTERRUPTED ***\n"); 95 double cpu_time = 0; 96 int64 mem_used = 0; 97 printStats(solver->stats,cpu_time,mem_used); 98 reportf("\n"); reportf("*** INTERRUPTED ***\n"); 99 exit(1); } 100 101 102//================================================================================================= 103// Simplistic proof-checker -- just to illustrate the use of 'ProofTraverser': 104 105 106#include "Sort.h" 107 108static void resolve(vec<Lit>& main, vec<Lit>& other, Var x) 109{ 110 Lit p; 111 bool ok1 = false, ok2 = false; 112 for (int i = 0; i < main.size(); i++){ 113 if (var(main[i]) == x){ 114 ok1 = true, p = main[i]; 115 main[i] = main.last(); 116 main.pop(); 117 break; 118 } 119 } 120 121 for (int i = 0; i < other.size(); i++){ 122 if (var(other[i]) != x) 123 main.push(other[i]); 124 else{ 125 if (p != ~other[i]) 126 printf("PROOF ERROR! Resolved on variable with SAME polarity in both clauses: %d\n", x+1); 127 ok2 = true; 128 } 129 } 130 131 if (!ok1 || !ok2) 132 printf("PROOF ERROR! Resolved on missing variable: %d\n", x+1); 133 134 sortUnique(main); 135} 136 137 138struct Checker : public ProofTraverser { 139 vec<vec<Lit> > clauses; 140 141 void root (const vec<Lit>& c) { 142 //**/printf("%d: ROOT", clauses.size()); 143 //for (int i = 0; i < c.size(); i++) 144 // printf(" %s%d", sign(c[i])?"-":"", var(c[i])+1); 145 //printf("\n"); 146 clauses.push(); 147 c.copyTo(clauses.last()); } 148 149 void chain (const vec<ClauseId>& cs, const vec<Var>& xs) { 150 //**/printf("%d: CHAIN %d", clauses.size(), cs[0]-1); 151 //for (int i = 0; i < xs.size(); i++) printf(" [%d] %d", (xs[i]>>1)+1, cs[i+1]-1); 152 clauses.push(); 153 vec<Lit>& c = clauses.last(); 154 155 //HA: the -1 to compensate for id_counter base 1 156 //HA: the >> 1 to drop sign info from vars 157 clauses[cs[0]-1].copyTo(c); 158 for (int i = 0; i < xs.size(); i++) 159 resolve(c, clauses[cs[i+1]-1], xs[i] >> 1); 160 //**/printf(" =>"); for (int i = 0; i < c.size(); i++) 161 // printf(" %s%d", sign(c[i])?"-":"", var(c[i])+1); printf("\n"); 162 } 163 164 void deleted(ClauseId c) { 165 clauses[c].clear(); } 166}; 167 168 169//HA: called with no second arg, so goal gets default value 170void checkProof(Proof* proof, ClauseId goal = ClauseId_NULL) 171{ 172 Checker trav; 173 int res_count = 0; 174 proof->traverse(trav, res_count, goal); 175 printf("%d resolution steps.\n",res_count); 176 vec<Lit>& c = trav.clauses.last(); 177 printf("Final clause:"); 178 if (c.size() == 0) 179 printf(" <empty>\n"); 180 else{ 181 for (int i = 0; i < c.size(); i++) 182 printf(" %s%d", sign(c[i])?"-":"", var(c[i])+1); 183 printf("\n"); 184 } 185} 186 187 188//================================================================================================= 189// Main: 190 191 192static const char* doc = 193 "USAGE: minisat <input-file> [options]\n" 194 " -r <result file> Write result (the word \"SAT\" plus model, or just \"UNSAT\") to file.\n" 195 " -p <proof trace> Write the trace to this file.\n" 196 " -c Check the trace by simple (read \"slow\") proof checker.\n" 197 " -x Extract proof from trace.\n" 198; 199 200int main(int argc, char** argv) 201{ 202 char* input = NULL; 203 char* result = NULL; 204 char* proof = NULL; 205 bool check = false; 206 bool compress = false; 207 208 // Parse options: 209 // 210 for (int i = 1; i < argc; i++){ 211 if (argv[i][0] != '-'){ 212 if (input != NULL) 213 fprintf(stderr, "ERROR! Only one input file may be specified.\n"), exit(1); 214 input = argv[i]; 215 }else{ 216 switch (argv[i][1]){ 217 case 'r': 218 i++; if (i >= argc) fprintf(stderr, "ERROR! Missing filename after '-r' option.\n"); 219 result = argv[i]; 220 break; 221 case 'p': 222 i++; if (i >= argc) fprintf(stderr, "ERROR! Missing filename after '-p' option.\n"); 223 proof = argv[i]; 224 break; 225 case 'c': 226 check = true; 227 break; 228 case 'x': 229 compress = true; 230 break; 231 case 'h': 232 reportf("%s", doc); 233 exit(0); 234 default: 235 fprintf(stderr, "ERROR! Invalid option: %s\n", argv[i]), exit(1); 236 } 237 } 238 } 239 240 // Parse input and perform SAT: 241 // 242 Solver S; 243 if (proof != NULL || check) S.proof = new Proof(); 244 if (input == NULL) { fprintf(stderr, "ERROR! Input file not specified"); exit(1); } 245 parse_DIMACS(input, S); 246 247 FILE* res = (result != NULL) ? fopen(result, "wb") : NULL; 248 249 if (!S.okay()){ 250 if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res); 251 if (S.proof != NULL && proof != NULL) S.proof->save(proof); 252 if (S.proof != NULL && check) printf("Checking proof...\n"), checkProof(S.proof); 253 reportf("Trivial problem\n"); 254 reportf("UNSATISFIABLE\n"); 255 exit(20); 256 } 257 258 S.verbosity = 1; 259 solver = &S; 260 signal(SIGINT,SIGINT_handler); 261 signal(SIGHUP,SIGINT_handler); 262 263 S.solve(); 264 265 double cpu_time = 0; int64 mem_used = 0; 266 printStats(S.stats,cpu_time,mem_used); 267 reportf("\n"); 268 reportf(S.okay() ? "SATISFIABLE\n" : "UNSATISFIABLE\n"); 269 270 if (res != NULL){ 271 if (S.okay()){ 272 fprintf(res, "SAT\n"); 273 for (int i = 0; i < S.nVars(); i++) 274 if (S.model[i] != l_Undef) 275 fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1); 276 fprintf(res, " 0\n"); 277 }else 278 fprintf(res, "UNSAT\n"); 279 fclose(res); 280 } 281 282 // Post-processing of proof in case of UNSAT 283 if (S.proof != NULL && !S.okay()){ 284 if (compress) { // ...compress, and possibly check 285 reportf("Compressing proof...\n"); 286 Proof compressed; 287 S.proof->compress(compressed,S.proof->last()); 288 if (check) 289 reportf("Checking compressed proof...\n"), 290 checkProof(&compressed); 291 if (proof != NULL) compressed.save(proof); 292 printProofStats(cpu_time,mem_used); 293 } else if (check) { // ...check 294 reportf("Checking proof...\n"), 295 checkProof(S.proof); 296 if (proof != NULL) S.proof->save(proof); 297 printProofStats(cpu_time,mem_used); 298 } else if (proof != NULL) S.proof->save(proof); 299 } 300 301 // (faster than "return", which will invoke the destructor for 'Solver') 302 exit(S.okay() ? 10 : 20); 303 304} 305