glucose-syrup/simp/Main.cc

   1 /***************************************************************************************[Main.cc]
   2  Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon
   3                                 CRIL - Univ. Artois, France
   4                                 LRI  - Univ. Paris Sud, France (2009-2013)
   5                                 Labri - Univ. Bordeaux, France
   6
   7  Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon
   8                                 CRIL - Univ. Artois, France
   9                                 Labri - Univ. Bordeaux, France
  10
  11 Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of
  12 Glucose (sources until 2013, Glucose 3.0, single core) are exactly the same as Minisat on which it
  13 is based on. (see below).
  14
  15 Glucose-Syrup sources are based on another copyright. Permissions and copyrights for the parallel
  16 version of Glucose-Syrup (the "Software") are granted, free of charge, to deal with the Software
  17 without restriction, including the rights to use, copy, modify, merge, publish, distribute,
  18 sublicence, and/or sell copies of the Software, and to permit persons to whom the Software is
  19 furnished to do so, subject to the following conditions:
  20
  21 - The above and below copyrights notices and this permission notice shall be included in all
  22 copies or substantial portions of the Software;
  23 - The parallel version of Glucose (all files modified since Glucose 3.0 releases, 2013) cannot
  24 be used in any competitive event (sat competitions/evaluations) without the express permission of
  25 the authors (Gilles Audemard / Laurent Simon). This is also the case for any competitive event
  26 using Glucose Parallel as an embedded SAT engine (single core or not).
  27
  28
  29 --------------- Original Minisat Copyrights
  30
  31 Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
  32 Copyright (c) 2007-2010, Niklas Sorensson
  33
  34 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
  35 associated documentation files (the "Software"), to deal in the Software without restriction,
  36 including without limitation the rights to use, copy, modify, merge, publish, distribute,
  37 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
  38 furnished to do so, subject to the following conditions:
  39
  40 The above copyright notice and this permission notice shall be included in all copies or
  41 substantial portions of the Software.
  42
  43 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
  44 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  45 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
  46 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
  47 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  48  **************************************************************************************************/
  49
  50 #include <errno.h>
  51
  52 #include <signal.h>
  53 #include <zlib.h>
  54 #include <sys/resource.h>
  55
  56 #include "utils/System.h"
  57 #include "utils/ParseUtils.h"
  58 #include "utils/Options.h"
  59 #include "core/Dimacs.h"
  60 #include "simp/SimpSolver.h"
  61
  62 using namespace Glucose;
  63
  64 //=================================================================================================
  65
  66 static const char* _certified = "CORE -- CERTIFIED UNSAT";
  67
  68 void printStats(Solver& solver)
  69 {
  70     double cpu_time = cpuTime();
  71     double mem_used = 0;//memUsedPeak();
  72     printf("c restarts              : %" PRIu64" (%" PRIu64" conflicts in avg)\n", solver.starts,(solver.starts>0 ?solver.conflicts/solver.starts : 0));
  73     printf("c blocked restarts      : %" PRIu64" (multiple: %" PRIu64") \n", solver.nbstopsrestarts,solver.nbstopsrestartssame);
  74     printf("c last block at restart : %" PRIu64"\n",solver.lastblockatrestart);
  75     printf("c nb ReduceDB           : %" PRIu64"\n", solver.nbReduceDB);
  76     printf("c nb removed Clauses    : %" PRIu64"\n",solver.nbRemovedClauses);
  77     printf("c nb learnts DL2        : %" PRIu64"\n", solver.nbDL2);
  78     printf("c nb learnts size 2     : %" PRIu64"\n", solver.nbBin);
  79     printf("c nb learnts size 1     : %" PRIu64"\n", solver.nbUn);
  80
  81     printf("c conflicts             : %-12" PRIu64"   (%.0f /sec)\n", solver.conflicts   , solver.conflicts   /cpu_time);
  82     printf("c decisions             : %-12" PRIu64"   (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions   /cpu_time);
  83     printf("c propagations          : %-12" PRIu64"   (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
  84     printf("c conflict literals     : %-12" PRIu64"   (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
  85     printf("c nb reduced Clauses    : %" PRIu64"\n",solver.nbReducedClauses);
  86
  87     if (mem_used != 0) printf("Memory used           : %.2f MB\n", mem_used);
  88     printf("c CPU time              : %g s\n", cpu_time);
  89 }
  90
  91
  92
  93 static Solver* solver;
  94 // Terminate by notifying the solver and back out gracefully. This is mainly to have a test-case
  95 // for this feature of the Solver as it may take longer than an immediate call to '_exit()'.
  96 static void SIGINT_interrupt(int signum) { solver->interrupt(); }
  97
  98 // Note that '_exit()' rather than 'exit()' has to be used. The reason is that 'exit()' calls
  99 // destructors and may cause deadlocks if a malloc/free function happens to be running (these
 100 // functions are guarded by locks for multithreaded use).
 101 static void SIGINT_exit(int signum) {
 102     printf("\n"); printf("*** INTERRUPTED ***\n");
 103     if (solver->verbosity > 0){
 104         printStats(*solver);
 105         printf("\n"); printf("*** INTERRUPTED ***\n"); }
 106     _exit(1); }
 107
 108
 109 //=================================================================================================
 110 // Main:
 111
 112 int main(int argc, char** argv)
 113 {
 114     try {
 115       printf("c\nc This is glucose 4.0 --  based on MiniSAT (Many thanks to MiniSAT team)\nc\n");
 116
 117
 118       setUsageHelp("c USAGE: %s [options] <input-file> <result-output-file>\n\n  where input may be either in plain or gzipped DIMACS.\n");
 119
 120
 121 #if defined(__linux__)
 122         fpu_control_t oldcw, newcw;
 123         _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
 124         //printf("c WARNING: for repeatability, setting FPU to use double precision\n");
 125 #endif
 126         // Extra options:
 127         //
 128         IntOption    verb   ("MAIN", "verb",   "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2));
 129         BoolOption   mod   ("MAIN", "model",   "show model.", false);
 130         IntOption    vv  ("MAIN", "vv",   "Verbosity every vv conflicts", 10000, IntRange(1,INT32_MAX));
 131         BoolOption   pre    ("MAIN", "pre",    "Completely turn on/off any preprocessing.", true);
 132         StringOption dimacs ("MAIN", "dimacs", "If given, stop after preprocessing and write the result to this file.");
 133         IntOption    cpu_lim("MAIN", "cpu-lim","Limit on CPU time allowed in seconds.\n", INT32_MAX, IntRange(0, INT32_MAX));
 134         IntOption    mem_lim("MAIN", "mem-lim","Limit on memory usage in megabytes.\n", INT32_MAX, IntRange(0, INT32_MAX));
 135  //       BoolOption opt_incremental ("MAIN","incremental", "Use incremental SAT solving",false);
 136
 137          BoolOption    opt_certified      (_certified, "certified",    "Certified UNSAT using DRUP format", false);
 138          StringOption  opt_certified_file      (_certified, "certified-output",    "Certified UNSAT output file", "NULL");
 139
 140         parseOptions(argc, argv, true);
 141
 142         SimpSolver  S;
 143         double      initial_time = cpuTime();
 144
 145         S.parsing = 1;
 146         //if (!pre) S.eliminate(true);
 147
 148         S.verbosity = verb;
 149         S.verbEveryConflicts = vv;
 150         S.showModel = mod;
 151
 152         S.certifiedUNSAT = opt_certified;
 153         if(S.certifiedUNSAT) {
 154             if(!strcmp(opt_certified_file,"NULL")) {
 155             S.certifiedOutput =  fopen("/dev/stdout", "wb");
 156             } else {
 157                 S.certifiedOutput =  fopen(opt_certified_file, "wb");
 158             }
 159             fprintf(S.certifiedOutput,"o proof DRUP\n");
 160         }
 161
 162         solver = &S;
 163         // Use signal handlers that forcibly quit until the solver will be able to respond to
 164         // interrupts:
 165         signal(SIGINT, SIGINT_exit);
 166         signal(SIGXCPU,SIGINT_exit);
 167
 168
 169         // Set limit on CPU-time:
 170         if (cpu_lim != INT32_MAX){
 171             rlimit rl;
 172             getrlimit(RLIMIT_CPU, &rl);
 173             if (rl.rlim_max == RLIM_INFINITY || (rlim_t)cpu_lim < rl.rlim_max){
 174                 rl.rlim_cur = cpu_lim;
 175                 if (setrlimit(RLIMIT_CPU, &rl) == -1)
 176                     printf("c WARNING! Could not set resource limit: CPU-time.\n");
 177             } }
 178
 179         // Set limit on virtual memory:
 180         if (mem_lim != INT32_MAX){
 181             rlim_t new_mem_lim = (rlim_t)mem_lim * 1024*1024;
 182             rlimit rl;
 183             getrlimit(RLIMIT_AS, &rl);
 184             if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){
 185                 rl.rlim_cur = new_mem_lim;
 186                 if (setrlimit(RLIMIT_AS, &rl) == -1)
 187                     printf("c WARNING! Could not set resource limit: Virtual memory.\n");
 188             } }
 189
 190         if (argc == 1)
 191             printf("c Reading from standard input... Use '--help' for help.\n");
 192
 193         gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb");
 194         if (in == NULL)
 195             printf("ERROR! Could not open file: %s\n", argc == 1 ? "<stdin>" : argv[1]), exit(1);
 196
 197       if (S.verbosity > 0){
 198             printf("c ========================================[ Problem Statistics ]===========================================\n");
 199             printf("c |                                                                                                       |\n"); }
 200
 201         FILE* res = (argc >= 3) ? fopen(argv[argc-1], "wb") : NULL;
 202         parse_DIMACS(in, S);
 203         gzclose(in);
 204
 205        if (S.verbosity > 0){
 206             printf("c |  Number of variables:  %12d                                                                   |\n", S.nVars());
 207             printf("c |  Number of clauses:    %12d                                                                   |\n", S.nClauses()); }
 208
 209         double parsed_time = cpuTime();
 210         if (S.verbosity > 0){
 211             printf("c |  Parse time:           %12.2f s                                                                 |\n", parsed_time - initial_time);
 212             printf("c |                                                                                                       |\n"); }
 213
 214         // Change to signal-handlers that will only notify the solver and allow it to terminate
 215         // voluntarily:
 216         signal(SIGINT, SIGINT_interrupt);
 217         signal(SIGXCPU,SIGINT_interrupt);
 218
 219         S.parsing = 0;
 220         if(pre/* && !S.isIncremental()*/) {
 221           printf("c | Preprocesing is fully done\n");
 222           S.eliminate(true);
 223         double simplified_time = cpuTime();
 224         if (S.verbosity > 0){
 225             printf("c |  Simplification time:  %12.2f s                                                                 |\n", simplified_time - parsed_time);
 226  }
 227         }
 228         printf("c |                                                                                                       |\n");
 229         if (!S.okay()){
 230             if (S.certifiedUNSAT) fprintf(S.certifiedOutput, "0\n"), fclose(S.certifiedOutput);
 231             if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res);
 232             if (S.verbosity > 0){
 233                 printf("c =========================================================================================================\n");
 234                printf("Solved by simplification\n");
 235                 printStats(S);
 236                 printf("\n"); }
 237             printf("s UNSATISFIABLE\n");
 238             exit(20);
 239         }
 240
 241         if (dimacs){
 242             if (S.verbosity > 0)
 243                 printf("c =======================================[ Writing DIMACS ]===============================================\n");
 244             S.toDimacs((const char*)dimacs);
 245             if (S.verbosity > 0)
 246                 printStats(S);
 247             exit(0);
 248         }
 249
 250         vec<Lit> dummy;
 251         lbool ret = S.solveLimited(dummy);
 252
 253         if (S.verbosity > 0){
 254             printStats(S);
 255             printf("\n"); }
 256         printf(ret == l_True ? "s SATISFIABLE\n" : ret == l_False ? "s UNSATISFIABLE\n" : "s INDETERMINATE\n");
 257
 258         if (res != NULL){
 259             if (ret == l_True){
 260                 printf("SAT\n");
 261                 for (int i = 0; i < S.nVars(); i++)
 262                     if (S.model[i] != l_Undef)
 263                         fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1);
 264                 fprintf(res, " 0\n");
 265             } else {
 266               if (ret == l_False){
 267                 fprintf(res, "UNSAT\n");
 268               }
 269             }
 270             fclose(res);
 271         } else {
 272           if(S.showModel && ret==l_True) {
 273             printf("v ");
 274             for (int i = 0; i < S.nVars(); i++)
 275               if (S.model[i] != l_Undef)
 276                 printf("%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1);
 277             printf(" 0\n");
 278           }
 279
 280         }
 281
 282         if (S.certifiedUNSAT) fprintf(S.certifiedOutput, "0\n"), fclose(S.certifiedOutput);
 283
 284 #ifdef NDEBUG
 285         exit(ret == l_True ? 10 : ret == l_False ? 20 : 0);     // (faster than "return", which will invoke the destructor for 'Solver')
 286 #else
 287         return (ret == l_True ? 10 : ret == l_False ? 20 : 0);
 288 #endif
 289     } catch (OutOfMemoryException&){
 290                 printf("c =========================================================================================================\n");
 291         printf("INDETERMINATE\n");
 292         exit(0);
 293     }
 294 }