backends/minisat/core/Main.C

   1 /******************************************************************************************[Main.C]
   2 MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
   3
   4 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
   5 associated documentation files (the "Software"), to deal in the Software without restriction,
   6 including without limitation the rights to use, copy, modify, merge, publish, distribute,
   7 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
   8 furnished to do so, subject to the following conditions:
   9
  10 The above copyright notice and this permission notice shall be included in all copies or
  11 substantial portions of the Software.
  12
  13 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
  14 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  15 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
  16 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
  17 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  18 **************************************************************************************************/
  19
  20 #include <ctime>
  21 #include <cstring>
  22 #include <stdint.h>
  23 #include <errno.h>
  24
  25 #include <signal.h>
  26 #include <zlib.h>
  27
  28 #include "Solver.h"
  29
  30 /*************************************************************************************/
  31 #ifdef _MSC_VER
  32 #include <ctime>
  33
  34 static inline double cpuTime(void) {
  35     return (double)clock() / CLOCKS_PER_SEC; }
  36 #else
  37
  38 #include <sys/time.h>
  39 #include <sys/resource.h>
  40 #include <unistd.h>
  41
  42 static inline double cpuTime(void) {
  43     struct rusage ru;
  44     getrusage(RUSAGE_SELF, &ru);
  45     return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }
  46 #endif
  47
  48
  49 #if defined(__linux__)
  50 static inline int memReadStat(int field)
  51 {
  52     char    name[256];
  53     pid_t pid = getpid();
  54     sprintf(name, "/proc/%d/statm", pid);
  55     FILE*   in = fopen(name, "rb");
  56     if (in == NULL) return 0;
  57     int     value;
  58     for (; field >= 0; field--)
  59         fscanf(in, "%d", &value);
  60     fclose(in);
  61     return value;
  62 }
  63 static inline uint64_t memUsed() { return (uint64_t)memReadStat(0) * (uint64_t)getpagesize(); }
  64
  65
  66 #elif defined(__FreeBSD__)
  67 static inline uint64_t memUsed(void) {
  68     struct rusage ru;
  69     getrusage(RUSAGE_SELF, &ru);
  70     return ru.ru_maxrss*1024; }
  71
  72
  73 #else
  74 static inline uint64_t memUsed() { return 0; }
  75 #endif
  76
  77 #if defined(__linux__)
  78 #include <fpu_control.h>
  79 #endif
  80
  81 //=================================================================================================
  82 // DIMACS Parser:
  83
  84 #define CHUNK_LIMIT 1048576
  85
  86 class StreamBuffer {
  87     gzFile  in;
  88     char    buf[CHUNK_LIMIT];
  89     int     pos;
  90     int     size;
  91
  92     void assureLookahead() {
  93         if (pos >= size) {
  94             pos  = 0;
  95             size = gzread(in, buf, sizeof(buf)); } }
  96
  97 public:
  98     StreamBuffer(gzFile i) : in(i), pos(0), size(0) {
  99         assureLookahead(); }
 100
 101     int  operator *  () { return (pos >= size) ? EOF : buf[pos]; }
 102     void operator ++ () { pos++; assureLookahead(); }
 103 };
 104
 105 //- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
 106
 107 template<class B>
 108 static void skipWhitespace(B& in) {
 109     while ((*in >= 9 && *in <= 13) || *in == 32)
 110         ++in; }
 111
 112 template<class B>
 113 static void skipLine(B& in) {
 114     for (;;){
 115         if (*in == EOF || *in == '\0') return;
 116         if (*in == '\n') { ++in; return; }
 117         ++in; } }
 118
 119 template<class B>
 120 static int parseInt(B& in) {
 121     int     val = 0;
 122     bool    neg = false;
 123     skipWhitespace(in);
 124     if      (*in == '-') neg = true, ++in;
 125     else if (*in == '+') ++in;
 126     if (*in < '0' || *in > '9') reportf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
 127     while (*in >= '0' && *in <= '9')
 128         val = val*10 + (*in - '0'),
 129         ++in;
 130     return neg ? -val : val; }
 131
 132 template<class B>
 133 static void readClause(B& in, Solver& S, vec<Lit>& lits) {
 134     int     parsed_lit, var;
 135     lits.clear();
 136     for (;;){
 137         parsed_lit = parseInt(in);
 138         if (parsed_lit == 0) break;
 139         var = abs(parsed_lit)-1;
 140         while (var >= S.nVars()) S.newVar();
 141         lits.push( (parsed_lit > 0) ? Lit(var) : ~Lit(var) );
 142     }
 143 }
 144
 145 template<class B>
 146 static bool match(B& in, char* str) {
 147     for (; *str != 0; ++str, ++in)
 148         if (*str != *in)
 149             return false;
 150     return true;
 151 }
 152
 153
 154 template<class B>
 155 static void parse_DIMACS_main(B& in, Solver& S) {
 156     vec<Lit> lits;
 157     for (;;){
 158         skipWhitespace(in);
 159         if (*in == EOF)
 160             break;
 161         else if (*in == 'p'){
 162             if (match(in, "p cnf")){
 163                 int vars    = parseInt(in);
 164                 int clauses = parseInt(in);
 165                 reportf("|  Number of variables:  %-12d                                         |\n", vars);
 166                 reportf("|  Number of clauses:    %-12d                                         |\n", clauses);
 167             }else{
 168                 reportf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
 169             }
 170         } else if (*in == 'c' || *in == 'p')
 171             skipLine(in);
 172         else
 173             readClause(in, S, lits),
 174             S.addClause(lits);
 175     }
 176 }
 177
 178 // Inserts problem into solver.
 179 //
 180 static void parse_DIMACS(gzFile input_stream, Solver& S) {
 181     StreamBuffer in(input_stream);
 182     parse_DIMACS_main(in, S); }
 183
 184
 185 //=================================================================================================
 186
 187
 188 void printStats(Solver& solver)
 189 {
 190     double   cpu_time = cpuTime();
 191     uint64_t mem_used = memUsed();
 192     reportf("restarts              : %lld\n", solver.starts);
 193     reportf("conflicts             : %-12lld   (%.0f /sec)\n", solver.conflicts   , solver.conflicts   /cpu_time);
 194     reportf("decisions             : %-12lld   (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions   /cpu_time);
 195     reportf("propagations          : %-12lld   (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
 196     reportf("conflict literals     : %-12lld   (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
 197     if (mem_used != 0) reportf("Memory used           : %.2f MB\n", mem_used / 1048576.0);
 198     reportf("CPU time              : %g s\n", cpu_time);
 199 }
 200
 201 Solver* solver;
 202 static void SIGINT_handler(int signum) {
 203     reportf("\n"); reportf("*** INTERRUPTED ***\n");
 204     printStats(*solver);
 205     reportf("\n"); reportf("*** INTERRUPTED ***\n");
 206     exit(1); }
 207
 208
 209 //=================================================================================================
 210 // Main:
 211
 212 void printUsage(char** argv)
 213 {
 214     reportf("USAGE: %s [options] <input-file> <result-output-file>\n\n  where input may be either in plain or gzipped DIMACS.\n\n", argv[0]);
 215     reportf("OPTIONS:\n\n");
 216     reportf("  -polarity-mode = {true,false,rnd}\n");
 217     reportf("  -decay         = <num> [ 0 - 1 ]\n");
 218     reportf("  -rnd-freq      = <num> [ 0 - 1 ]\n");
 219     reportf("  -verbosity     = {0,1,2}\n");
 220     reportf("\n");
 221 }
 222
 223
 224 const char* hasPrefix(const char* str, const char* prefix)
 225 {
 226     int len = strlen(prefix);
 227     if (strncmp(str, prefix, len) == 0)
 228         return str + len;
 229     else
 230         return NULL;
 231 }
 232
 233
 234 int main(int argc, char** argv)
 235 {
 236     Solver      S;
 237     S.verbosity = 1;
 238
 239
 240     int         i, j;
 241     const char* value;
 242     for (i = j = 0; i < argc; i++){
 243         if ((value = hasPrefix(argv[i], "-polarity-mode="))){
 244             if (strcmp(value, "true") == 0)
 245                 S.polarity_mode = Solver::polarity_true;
 246             else if (strcmp(value, "false") == 0)
 247                 S.polarity_mode = Solver::polarity_false;
 248             else if (strcmp(value, "rnd") == 0)
 249                 S.polarity_mode = Solver::polarity_rnd;
 250             else{
 251                 reportf("ERROR! unknown polarity-mode %s\n", value);
 252                 exit(0); }
 253
 254         }else if ((value = hasPrefix(argv[i], "-rnd-freq="))){
 255             double rnd;
 256             if (sscanf(value, "%lf", &rnd) <= 0 || rnd < 0 || rnd > 1){
 257                 reportf("ERROR! illegal rnd-freq constant %s\n", value);
 258                 exit(0); }
 259             S.random_var_freq = rnd;
 260
 261         }else if ((value = hasPrefix(argv[i], "-decay="))){
 262             double decay;
 263             if (sscanf(value, "%lf", &decay) <= 0 || decay <= 0 || decay > 1){
 264                 reportf("ERROR! illegal decay constant %s\n", value);
 265                 exit(0); }
 266             S.var_decay = 1 / decay;
 267
 268         }else if ((value = hasPrefix(argv[i], "-verbosity="))){
 269             int verbosity = (int)strtol(value, NULL, 10);
 270             if (verbosity == 0 && errno == EINVAL){
 271                 reportf("ERROR! illegal verbosity level %s\n", value);
 272                 exit(0); }
 273             S.verbosity = verbosity;
 274
 275         }else if (strcmp(argv[i], "-h") == 0 || strcmp(argv[i], "-help") == 0 || strcmp(argv[i], "--help") == 0){
 276             printUsage(argv);
 277             exit(0);
 278
 279         }else if (strncmp(argv[i], "-", 1) == 0){
 280             reportf("ERROR! unknown flag %s\n", argv[i]);
 281             exit(0);
 282
 283         }else
 284             argv[j++] = argv[i];
 285     }
 286     argc = j;
 287
 288
 289     reportf("This is MiniSat 2.0 beta\n");
 290 #if defined(__linux__)
 291     fpu_control_t oldcw, newcw;
 292     _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
 293     reportf("WARNING: for repeatability, setting FPU to use double precision\n");
 294 #endif
 295     double cpu_time = cpuTime();
 296
 297     solver = &S;
 298     signal(SIGINT,SIGINT_handler);
 299     signal(SIGHUP,SIGINT_handler);
 300
 301     if (argc == 1)
 302         reportf("Reading from standard input... Use '-h' or '--help' for help.\n");
 303
 304     gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb");
 305     if (in == NULL)
 306         reportf("ERROR! Could not open file: %s\n", argc == 1 ? "<stdin>" : argv[1]), exit(1);
 307
 308     reportf("============================[ Problem Statistics ]=============================\n");
 309     reportf("|                                                                             |\n");
 310
 311     parse_DIMACS(in, S);
 312     gzclose(in);
 313     FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL;
 314
 315     double parse_time = cpuTime() - cpu_time;
 316     reportf("|  Parsing time:         %-12.2f s                                       |\n", parse_time);
 317
 318     if (!S.simplify()){
 319         reportf("Solved by unit propagation\n");
 320         if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res);
 321         printf("UNSATISFIABLE\n");
 322         exit(20);
 323     }
 324
 325     bool ret = S.solve();
 326     printStats(S);
 327     reportf("\n");
 328     printf(ret ? "SATISFIABLE\n" : "UNSATISFIABLE\n");
 329     if (res != NULL){
 330         if (ret){
 331             fprintf(res, "SAT\n");
 332             for (int i = 0; i < S.nVars(); i++)
 333                 if (S.model[i] != l_Undef)
 334                     fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1);
 335             fprintf(res, " 0\n");
 336         }else
 337             fprintf(res, "UNSAT\n");
 338         fclose(res);
 339     }
 340
 341 #ifdef NDEBUG
 342     exit(ret ? 10 : 20);     // (faster than "return", which will invoke the destructor for 'Solver')
 343 #endif
 344 }