glucose-syrup/parallel/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
  55
  56 #include "utils/System.h"
  57 #include "utils/ParseUtils.h"
  58 #include "utils/Options.h"
  59 #include "core/Dimacs.h"
  60 #include "core/SolverTypes.h"
  61
  62 #include "simp/SimpSolver.h"
  63 #include "parallel/ParallelSolver.h"
  64 #include "parallel/MultiSolvers.h"
  65
  66 using namespace Glucose;
  67
  68
  69
  70 static MultiSolvers* pmsolver;
  71
  72 // Terminate by notifying the solver and back out gracefully. This is mainly to have a test-case
  73 // for this feature of the Solver as it may take longer than an immediate call to '_exit()'.
  74 //static void SIGINT_interrupt(int signum) { pmsolver->interrupt(); }
  75
  76
  77 // Note that '_exit()' rather than 'exit()' has to be used. The reason is that 'exit()' calls
  78 // destructors and may cause deadlocks if a malloc/free function happens to be running (these
  79 // functions are guarded by locks for multithreaded use).
  80 static void SIGINT_exit(int signum) {
  81     printf("\n"); printf("*** INTERRUPTED ***\n");
  82     if (pmsolver->verbosity() > 0){
  83         pmsolver->printFinalStats();
  84         printf("\n"); printf("*** INTERRUPTED ***\n"); }
  85     _exit(1); }
  86
  87
  88 //=================================================================================================
  89 // Main:
  90
  91
  92 int main(int argc, char** argv)
  93 {
  94     double realTimeStart = realTime();
  95   printf("c\nc This is glucose-syrup 4.0 (glucose in many threads) --  based on MiniSAT (Many thanks to MiniSAT team)\nc\n");
  96     try {
  97         setUsageHelp("c USAGE: %s [options] <input-file> <result-output-file>\n\n  where input may be either in plain or gzipped DIMACS.\n");
  98         // printf("This is MiniSat 2.0 beta\n");
  99
 100 #if defined(__linux__)
 101         fpu_control_t oldcw, newcw;
 102         _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
 103         printf("c WARNING: for repeatability, setting FPU to use double precision\n");
 104 #endif
 105         // Extra options:
 106         //
 107         IntOption    verb   ("MAIN", "verb",   "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2));
 108         BoolOption   mod   ("MAIN", "model",   "show model.", false);
 109         IntOption    vv  ("MAIN", "vv",   "Verbosity every vv conflicts", 10000, IntRange(1,INT32_MAX));
 110         IntOption    cpu_lim("MAIN", "cpu-lim","Limit on CPU time allowed in seconds.\n", INT32_MAX, IntRange(0, INT32_MAX));
 111         IntOption    mem_lim("MAIN", "mem-lim","Limit on memory usage in megabytes.\n", INT32_MAX, IntRange(0, INT32_MAX));
 112
 113         parseOptions(argc, argv, true);
 114
 115         MultiSolvers msolver;
 116         pmsolver = & msolver;
 117         msolver.setVerbosity(verb);
 118         msolver.setVerbEveryConflicts(vv);
 119         msolver.setShowModel(mod);
 120
 121         double initial_time = cpuTime();
 122
 123                 // Use signal handlers that forcibly quit until the solver will be able to respond to
 124         // interrupts:
 125         signal(SIGINT, SIGINT_exit);
 126         signal(SIGXCPU,SIGINT_exit);
 127
 128         // Set limit on CPU-time:
 129         if (cpu_lim != INT32_MAX){
 130             rlimit rl;
 131             getrlimit(RLIMIT_CPU, &rl);
 132             if (rl.rlim_max == RLIM_INFINITY || (rlim_t)cpu_lim < rl.rlim_max){
 133                 rl.rlim_cur = cpu_lim;
 134                 if (setrlimit(RLIMIT_CPU, &rl) == -1)
 135                     printf("c WARNING! Could not set resource limit: CPU-time.\n");
 136             } }
 137
 138         // Set limit on virtual memory:
 139         if (mem_lim != INT32_MAX){
 140             rlim_t new_mem_lim = (rlim_t)mem_lim * 1024*1024;
 141             rlimit rl;
 142             getrlimit(RLIMIT_AS, &rl);
 143             if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){
 144                 rl.rlim_cur = new_mem_lim;
 145                 if (setrlimit(RLIMIT_AS, &rl) == -1)
 146                     printf("c WARNING! Could not set resource limit: Virtual memory.\n");
 147             } }
 148
 149         if (argc == 1)
 150             printf("c Reading from standard input... Use '--help' for help.\n");
 151
 152         gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb");
 153         if (in == NULL)
 154             printf("c ERROR! Could not open file: %s\n", argc == 1 ? "<stdin>" : argv[1]), exit(1);
 155
 156         if (msolver.verbosity() > 0){
 157             printf("c ========================================[ Problem Statistics ]===========================================\n");
 158             printf("c |                                                                                                       |\n"); }
 159
 160         parse_DIMACS(in, msolver);
 161         gzclose(in);
 162
 163
 164
 165         FILE* res = (argc >= 3) ? fopen(argv[argc-1], "wb") : NULL;
 166
 167         if (msolver.verbosity() > 0){
 168             printf("c |  Number of variables:  %12d                                                                   |\n", msolver.nVars());
 169             printf("c |  Number of clauses:    %12d                                                                   |\n", msolver.nClauses()); }
 170
 171         double parsed_time = cpuTime();
 172         if (msolver.verbosity() > 0){
 173             printf("c |  Parse time:           %12.2f s                                                                 |\n", parsed_time - initial_time);
 174             printf("c |                                                                                                       |\n"); }
 175
 176         // Change to signal-handlers that will only notify the solver and allow it to terminate
 177         // voluntarily:
 178         //signal(SIGINT, SIGINT_interrupt);
 179         //signal(SIGXCPU,SIGINT_interrupt);
 180
 181
 182         int ret2 = msolver.simplify();
 183         if(ret2)
 184            msolver.eliminate();
 185         double simplified_time = cpuTime();
 186         if (msolver.verbosity() > 0){
 187             printf("c |  Simplification time:  %12.2f s                                                                 |\n", simplified_time - parsed_time);
 188             printf("c |                                                                                                       |\n"); }
 189
 190         if (!ret2 || !msolver.okay()){
 191             //if (S.certifiedOutput != NULL) fprintf(S.certifiedOutput, "0\n"), fclose(S.certifiedOutput);
 192             if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res);
 193             if (msolver.verbosity() > 0){
 194                 printf("c =========================================================================================================\n");
 195                 printf("Solved by unit propagation\n");
 196                 printf("c real time : %g s\n", realTime() - realTimeStart);
 197                 printf("c cpu time  : %g s\n", cpuTime());
 198                 printf("\n"); }
 199             printf("s UNSATISFIABLE\n");
 200             exit(20);
 201         }
 202
 203       //  vec<Lit> dummy;
 204         lbool ret = msolver.solve();
 205
 206
 207         printf("c\n");
 208         printf("c real time : %g s\n", realTime() - realTimeStart);
 209         printf("c cpu time  : %g s\n", cpuTime());
 210         if (msolver.verbosity() > 0){
 211             msolver.printFinalStats();
 212             printf("\n"); }
 213
 214         //-------------- Result is put in a external file
 215         /* I must admit I have to print the model of one thread... But which one? FIXME !!
 216           if (res != NULL){
 217           if (ret == l_True){
 218             fprintf(res, "SAT\n");
 219             for (int i = 0; i < S.nVars(); i++)
 220               if (S.model[i] != l_Undef)
 221                 fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1);
 222             fprintf(res, " 0\n");
 223           }else if (ret == l_False)
 224             fprintf(res, "UNSAT\n");
 225           else
 226             fprintf(res, "INDET\n");
 227           fclose(res);
 228
 229         //-------------- Want certified output
 230         } else {
 231         */
 232           printf(ret == l_True ? "s SATISFIABLE\n" : ret == l_False ? "s UNSATISFIABLE\n" : "s INDETERMINATE\n");
 233
 234           if(msolver.getShowModel() && ret==l_True) {
 235             printf("v ");
 236             for (int i = 0; i < msolver.model.size() ; i++)
 237               if (msolver.model[i] != l_Undef)
 238                 printf("%s%s%d", (i==0)?"":" ", (msolver.model[i]==l_True)?"":"-", i+1);
 239             printf(" 0\n");
 240           }
 241
 242
 243
 244 #ifdef NDEBUG
 245         exit(ret == l_True ? 10 : ret == l_False ? 20 : 0);     // (faster than "return", which will invoke the destructor for 'Solver')
 246 #else
 247         return (ret == l_True ? 10 : ret == l_False ? 20 : 0);
 248 #endif
 249     } catch (OutOfMemoryException&){
 250       printf("c ===================================================================================================\n");
 251         printf("INDETERMINATE\n");
 252         exit(0);
 253     }
 254 }