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
7 Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon
8 CRIL - Univ. Artois, France
9 Labri - Univ. Bordeaux, France
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).
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:
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).
29 --------------- Original Minisat Copyrights
31 Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
32 Copyright (c) 2007-2010, Niklas Sorensson
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:
40 The above copyright notice and this permission notice shall be included in all copies or
41 substantial portions of the Software.
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 **************************************************************************************************/
54 #include <sys/resource.h>
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"
62 using namespace Glucose;
64 //=================================================================================================
66 static const char* _certified = "CORE -- CERTIFIED UNSAT";
68 void printStats(Solver& solver)
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);
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);
87 if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used);
88 printf("c CPU time : %g s\n", cpu_time);
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(); }
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){
105 printf("\n"); printf("*** INTERRUPTED ***\n"); }
109 //=================================================================================================
112 int main(int argc, char** argv)
115 printf("c\nc This is glucose 4.0 -- based on MiniSAT (Many thanks to MiniSAT team)\nc\n");
118 setUsageHelp("c USAGE: %s [options] <input-file> <result-output-file>\n\n where input may be either in plain or gzipped DIMACS.\n");
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");
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);
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");
140 parseOptions(argc, argv, true);
143 double initial_time = cpuTime();
146 //if (!pre) S.eliminate(true);
149 S.verbEveryConflicts = vv;
152 S.certifiedUNSAT = opt_certified;
153 if(S.certifiedUNSAT) {
154 if(!strcmp(opt_certified_file,"NULL")) {
155 S.certifiedOutput = fopen("/dev/stdout", "wb");
157 S.certifiedOutput = fopen(opt_certified_file, "wb");
159 fprintf(S.certifiedOutput,"o proof DRUP\n");
163 // Use signal handlers that forcibly quit until the solver will be able to respond to
165 signal(SIGINT, SIGINT_exit);
166 signal(SIGXCPU,SIGINT_exit);
169 // Set limit on CPU-time:
170 if (cpu_lim != INT32_MAX){
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");
179 // Set limit on virtual memory:
180 if (mem_lim != INT32_MAX){
181 rlim_t new_mem_lim = (rlim_t)mem_lim * 1024*1024;
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");
191 printf("c Reading from standard input... Use '--help' for help.\n");
193 gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb");
195 printf("ERROR! Could not open file: %s\n", argc == 1 ? "<stdin>" : argv[1]), exit(1);
197 if (S.verbosity > 0){
198 printf("c ========================================[ Problem Statistics ]===========================================\n");
201 FILE* res = (argc >= 3) ? fopen(argv[argc-1], "wb") : NULL;
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()); }
209 double parsed_time = cpuTime();
210 if (S.verbosity > 0){
211 printf("c | Parse time: %12.2f s |\n", parsed_time - initial_time);
214 // Change to signal-handlers that will only notify the solver and allow it to terminate
216 signal(SIGINT, SIGINT_interrupt);
217 signal(SIGXCPU,SIGINT_interrupt);
220 if(pre/* && !S.isIncremental()*/) {
221 printf("c | Preprocesing is fully done\n");
223 double simplified_time = cpuTime();
224 if (S.verbosity > 0){
225 printf("c | Simplification time: %12.2f s |\n", simplified_time - parsed_time);
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");
237 printf("s UNSATISFIABLE\n");
243 printf("c =======================================[ Writing DIMACS ]===============================================\n");
244 S.toDimacs((const char*)dimacs);
251 lbool ret = S.solveLimited(dummy);
253 if (S.verbosity > 0){
256 printf(ret == l_True ? "s SATISFIABLE\n" : ret == l_False ? "s UNSATISFIABLE\n" : "s INDETERMINATE\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");
267 fprintf(res, "UNSAT\n");
272 if(S.showModel && ret==l_True) {
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);
282 if (S.certifiedUNSAT) fprintf(S.certifiedOutput, "0\n"), fclose(S.certifiedOutput);
285 exit(ret == l_True ? 10 : ret == l_False ? 20 : 0); // (faster than "return", which will invoke the destructor for 'Solver')
287 return (ret == l_True ? 10 : ret == l_False ? 20 : 0);
289 } catch (OutOfMemoryException&){
290 printf("c =========================================================================================================\n");
291 printf("INDETERMINATE\n");