diff --git a/CHANGELOG b/CHANGELOG index 5f7510d..de807b3 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,7 @@ +Version 4.2.1 + - Lazy Clause Minimisation (IJCAI'17 paper By Chu Min Li etal. + - cmake and makefile modes + Version 4.1 - Adaptative (activated by default) strategies. See SAT 2016 paper. diff --git a/CMakeLists.txt b/CMakeLists.txt new file mode 100644 index 0000000..4c32148 --- /dev/null +++ b/CMakeLists.txt @@ -0,0 +1,50 @@ +cmake_minimum_required(VERSION 2.6) + +project(glucose) + +option(BUILD_SHARED_LIBS OFF "True for building shared object") + +set(CMAKE_CXX_FLAGS "-std=c++11") + +# Dependencies {{{ +find_package(ZLIB REQUIRED) +find_package(Threads REQUIRED) +# }}} + +set(main_simp "simp/Main.cc") +set(main_parallel "parallel/Main.cc") + +# Basic Library +file(GLOB lib_srcs RELATIVE ${CMAKE_CURRENT_SOURCE_DIR} mtl/*.cc core/*.cc simp/*.cc utils/*.cc) +list(REMOVE_ITEM lib_srcs ${main_simp} ${main_parallel}) + +message(${lib_srcs}) + +# Parallel Library +file(GLOB lib_parallel_srcs RELATIVE ${CMAKE_CURRENT_SOURCE_DIR} parallel/*.cc) +list(REMOVE_ITEM lib_parallel_srcs ${main_simp} ${main_parallel}) + + +if(BUILD_SHARED_LIBS) + set(lib_type "SHARED") +else() + set(lib_type "STATIC") +endif() + + +include_directories( + ${CMAKE_CURRENT_SOURCE_DIR} + ${ZLIB_INCLUDE_DIR}) + +link_libraries(${ZLIB_LIBRARY}) + +# base library +add_library(glucose ${lib_type} ${lib_srcs}) + +add_executable(glucose-simp ${main_simp}) +target_link_libraries(glucose-simp glucose) + +# PARALLEL STUFF: +add_library(glucosep ${lib_type} ${lib_srcs} ${lib_parallel_srcs}) +add_executable(glucose-syrup ${main_parallel}) +target_link_libraries(glucose-syrup glucosep ${CMAKE_THREAD_LIBS_INIT}) \ No newline at end of file diff --git a/README.md b/README.md index 7e68efa..f852db3 100644 --- a/README.md +++ b/README.md @@ -1,15 +1,28 @@ # Glucose SAT solver -This is the release 4.1 of the glucose SAT solver. + +This is the release 4.2.1 of the glucose SAT solver. It is based on [Minisat 2.2](http://minisat.se/MiniSat.html) -**Glucose is now parallel** - -You can call it Glucose Parallel or Glucose-Syrup (a lot of glucose in it). -An original mechanism for clause sharing (as described in the SAT 2014 paper, based on a 1-Watched literal scheme). -Can work with a lot of cores and limited memory. There is no determinism in the parallel version. +## Presentation +Glucose is an award winning SAT solver based on a scoring scheme we introduced in 2009 for the clause learning mechanism of so called “Modern” SAT sovlers (see our IJCAI’09 paper). It is designed to be parallel, since 2014 and was enterly rebooted in 2021. +Glucose is developed by a very friendly team: Gilles Audemard and Laurent Simon. + +The name of the Solver name is a contraction of the concept of “glue clauses”, a particular kind of clauses that glucose detects and preserves during search. -Very good performances on industrial (non crypto) problems. +Glucose is heavily based on Minisat, so please do cite Minisat also if you want to cite Glucose. Glucose is based on the [Minisat 2.2](http://minisat.se/MiniSat.html) version. We strongly encourage you to visit the Minisat web pages, and to try the original Minisat too. + +## A (very) short analysis of Glucose performances +Learning (in CDCL algorithms) was firstly introduced for completeness. But, if we study all Glucose 2’s traces of the competition 2011, for instance, phase 2, in the categories Applications and Crafted, Glucose 2 learnt 973,468,489 clauses (sum over all traces) but removed 909,123,525 of them, i.e. more than 93% of the clauses are removed. This view is really new and contradicts previous beliefs. Thus, we thought that one of the performance keys of our solver is not only based on the identification of good clauses, but also on the removing of bad ones. As a side effect, by aggressively deleting those clauses, Glucose increases the CDCL incompleteness (keeping learnt clauses is essential for completeness). We should also emphasize here that Glucose 2 was ranked fourth on the parallel track in the SAT 2011 competition beside the fact that it was sequential. This shows that even with a single core, our solver performed better, in user time (not CPU) than many parallel solvers exploiting the 8 cores of the parallel machine. One of the reasons for this is that Glucose 2 is good at finding the shortest (but easiest) proof as possible. + +Among the short list of [programs](http://www-cs-faculty.stanford.edu/~knuth/programs.html) of Prof. Don Knuth, you may want to take a deep look at the [SAT13.w](http://www-cs-faculty.stanford.edu/~knuth/programs/sat13.w), his CDCL implementation. Very interesting and insightful. With glucose-techniques inside! + +## Features + + - Sequential and Parallel solvers + - Incremental mode + - Certified UNSAT proofs + - Good performances on industrial (non crypto) problems. **Note**: Don’t change the preprocessing switches on this version (you can turn off the preprocessing but when using it, don’t play with the preprocessing options). We were reported some discrepancies in the results when using the -rcheck argument. You can choose to compile the following Glucose alternatives: @@ -21,6 +34,20 @@ You can choose to compile the following Glucose alternatives: Choose your directory (simp or parallel) and type ‘make’. +## How to use it + +We are often asked how to use/install/call our SAT solver. + + - Don't forget to install the libz library. It is needed to read .cnf.gz files (compressed cnf). This is probably the most frequent compilation error. + - You should type "make" into the simp (if you want to preprocess the file) or into the core directory. + - You may have a few warning (depending on your gcc version) but this should not hurt + - If Glucose compiles, you need now a CNF file to give it. CNF files are in Dimacs format, i.e. variables are numbers only and the formula is in conjunctive normal form. You may need to spend some time to search the web for this format. It is simple but you may need to write a few lines to handle it/play with it inside your own tool + - If everything's ok, and if Glucose found an answer to your problem, send us an email (we like to hear successes stories about glucose ) and now you have either + - To trust Glucose if it says "UNSAT" (your formula has no solution) + - To run Glucose again with certified UNSAT activated (to check that glucose was correctly answer UNSAT) + - To read the solution, if Glucose says "SAT". Your solution (with -model activated is printed at the end). + + ## Papers - "_Predicting Learnt Clauses Quality in Modern SAT Solver_". Gilles Audemard, Laurent Simon, in Twenty-first International Joint Conference on Artificial Intelligence (IJCAI'09), july 2009. @@ -33,3 +60,5 @@ Choose your directory (simp or parallel) and type ‘make’. - "_Glucose and Syrup in the SAT Race 2015_". Gilles Audemard, Laurent Simon, SAT race 2015. - "_Extreme cases in SAT problems_". Gilles Audemard, Laurent Simonn in International Conference on Theory and Applications of Satisfiability Testing (SAT'16), 2016. - "_Glucose and Syrup in the SAT’17_". Gilles Audemard, Laurent Simon, SAT competition 2017. + - "_Glucose and syrup: Nine years in the sat competitions_". illes Audemard, Laurent Simon, SAT competition 2018. + - "_On the glucose SAT solver_". Gilles Audemard, Laurent Simon, International Journal on Artificial Intelligence Tools 27 (01), 2018. \ No newline at end of file diff --git a/core/Main.cc b/core/Main.cc deleted file mode 100644 index 3aece05..0000000 --- a/core/Main.cc +++ /dev/null @@ -1,233 +0,0 @@ -/*****************************************************************************************[Main.cc] - Glucose -- Copyright (c) 2009, Gilles Audemard, Laurent Simon - CRIL - Univ. Artois, France - LRI - Univ. Paris Sud, France - -Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of -Glucose are exactly the same as Minisat on which it is based on. (see below). - ---------------- - -Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson -Copyright (c) 2007-2010, Niklas Sorensson - -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and -associated documentation files (the "Software"), to deal in the Software without restriction, -including without limitation the rights to use, copy, modify, merge, publish, distribute, -sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in all copies or -substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT -NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, -DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT -OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -**************************************************************************************************/ - -#include - -#include -#include - -#include "utils/System.h" -#include "utils/ParseUtils.h" -#include "utils/Options.h" -#include "core/Dimacs.h" -#include "core/Solver.h" - -using namespace Glucose; - -//================================================================================================= - - -void printStats(Solver& solver) -{ - double cpu_time = cpuTime(); - double mem_used = 0;//memUsedPeak(); - printf("c restarts : %"PRIu64" (%"PRIu64" conflicts in avg)\n", solver.starts,(solver.starts>0 ?solver.conflicts/solver.starts : 0)); - printf("c blocked restarts : %"PRIu64" (multiple: %"PRIu64") \n", solver.nbstopsrestarts,solver.nbstopsrestartssame); - printf("c last block at restart : %"PRIu64"\n",solver.lastblockatrestart); - printf("c nb ReduceDB : %lld\n", solver.nbReduceDB); - printf("c nb removed Clauses : %lld\n",solver.nbRemovedClauses); - printf("c nb learnts DL2 : %lld\n", solver.nbDL2); - printf("c nb learnts size 2 : %lld\n", solver.nbBin); - printf("c nb learnts size 1 : %lld\n", solver.nbUn); - - printf("c conflicts : %-12"PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time); - 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); - printf("c propagations : %-12"PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time); - printf("c conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals); - printf("c nb reduced Clauses : %lld\n",solver.nbReducedClauses); - - if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used); - printf("c CPU time : %g s\n", cpu_time); -} - - -static Solver* solver; -// Terminate by notifying the solver and back out gracefully. This is mainly to have a test-case -// for this feature of the Solver as it may take longer than an immediate call to '_exit()'. -static void SIGINT_interrupt(int signum) { solver->interrupt(); } - -// Note that '_exit()' rather than 'exit()' has to be used. The reason is that 'exit()' calls -// destructors and may cause deadlocks if a malloc/free function happens to be running (these -// functions are guarded by locks for multithreaded use). -static void SIGINT_exit(int signum) { - printf("\n"); printf("*** INTERRUPTED ***\n"); - if (solver->verbosity > 0){ - printStats(*solver); - printf("\n"); printf("*** INTERRUPTED ***\n"); } - _exit(1); } - - -//================================================================================================= -// Main: - - -int main(int argc, char** argv) -{ - printf("c\nc This is glucose 3.0 -- based on MiniSAT (Many thanks to MiniSAT team)\nc\n"); - try { - setUsageHelp("c USAGE: %s [options] \n\n where input may be either in plain or gzipped DIMACS.\n"); - // printf("This is MiniSat 2.0 beta\n"); - -#if defined(__linux__) - fpu_control_t oldcw, newcw; - _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw); - printf("c WARNING: for repeatability, setting FPU to use double precision\n"); -#endif - // Extra options: - // - IntOption verb ("MAIN", "verb", "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2)); - BoolOption mod ("MAIN", "model", "show model.", false); - IntOption vv ("MAIN", "vv", "Verbosity every vv conflicts", 10000, IntRange(1,INT32_MAX)); - IntOption cpu_lim("MAIN", "cpu-lim","Limit on CPU time allowed in seconds.\n", INT32_MAX, IntRange(0, INT32_MAX)); - IntOption mem_lim("MAIN", "mem-lim","Limit on memory usage in megabytes.\n", INT32_MAX, IntRange(0, INT32_MAX)); - - - parseOptions(argc, argv, true); - - Solver S; - double initial_time = cpuTime(); - - S.verbosity = verb; - S.verbEveryConflicts = vv; - S.showModel = mod; - solver = &S; - // Use signal handlers that forcibly quit until the solver will be able to respond to - // interrupts: - // signal(SIGINT, SIGINT_exit); - //signal(SIGXCPU,SIGINT_exit); - - // Set limit on CPU-time: - if (cpu_lim != INT32_MAX){ - rlimit rl; - getrlimit(RLIMIT_CPU, &rl); - if (rl.rlim_max == RLIM_INFINITY || (rlim_t)cpu_lim < rl.rlim_max){ - rl.rlim_cur = cpu_lim; - if (setrlimit(RLIMIT_CPU, &rl) == -1) - printf("c WARNING! Could not set resource limit: CPU-time.\n"); - } } - - // Set limit on virtual memory: - if (mem_lim != INT32_MAX){ - rlim_t new_mem_lim = (rlim_t)mem_lim * 1024*1024; - rlimit rl; - getrlimit(RLIMIT_AS, &rl); - if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){ - rl.rlim_cur = new_mem_lim; - if (setrlimit(RLIMIT_AS, &rl) == -1) - printf("c WARNING! Could not set resource limit: Virtual memory.\n"); - } } - - if (argc == 1) - printf("c Reading from standard input... Use '--help' for help.\n"); - - gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb"); - if (in == NULL) - printf("c ERROR! Could not open file: %s\n", argc == 1 ? "" : argv[1]), exit(1); - - if (S.verbosity > 0){ - printf("c ========================================[ Problem Statistics ]===========================================\n"); - printf("c | |\n"); } - - parse_DIMACS(in, S); - gzclose(in); - - - - FILE* res = (argc >= 3) ? fopen(argv[argc-1], "wb") : NULL; - - if (S.verbosity > 0){ - printf("c | Number of variables: %12d |\n", S.nVars()); - printf("c | Number of clauses: %12d |\n", S.nClauses()); } - - double parsed_time = cpuTime(); - if (S.verbosity > 0){ - printf("c | Parse time: %12.2f s |\n", parsed_time - initial_time); - printf("c | |\n"); } - - // Change to signal-handlers that will only notify the solver and allow it to terminate - // voluntarily: - //signal(SIGINT, SIGINT_interrupt); - //signal(SIGXCPU,SIGINT_interrupt); - - if (!S.simplify()){ - if (S.certifiedOutput != NULL) fprintf(S.certifiedOutput, "0\n"), fclose(S.certifiedOutput); - if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res); - if (S.verbosity > 0){ - printf("c =========================================================================================================\n"); - printf("Solved by unit propagation\n"); - printStats(S); - printf("\n"); } - printf("s UNSATISFIABLE\n"); - exit(20); - } - - vec dummy; - lbool ret = S.solveLimited(dummy); - if (S.verbosity > 0){ - printStats(S); - printf("\n"); } - - //-------------- Result is put in a external file - if (res != NULL){ - if (ret == l_True){ - fprintf(res, "SAT\n"); - for (int i = 0; i < S.nVars(); i++) - if (S.model[i] != l_Undef) - fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1); - fprintf(res, " 0\n"); - }else if (ret == l_False) - fprintf(res, "UNSAT\n"); - else - fprintf(res, "INDET\n"); - fclose(res); - - //-------------- Want certified output - } else { - printf(ret == l_True ? "s SATISFIABLE\n" : ret == l_False ? "s UNSATISFIABLE\n" : "s INDETERMINATE\n"); - if(S.showModel && ret==l_True) { - printf("v "); - for (int i = 0; i < S.nVars(); i++) - if (S.model[i] != l_Undef) - printf("%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1); - printf(" 0\n"); - } - } - - -#ifdef NDEBUG - exit(ret == l_True ? 10 : ret == l_False ? 20 : 0); // (faster than "return", which will invoke the destructor for 'Solver') -#else - return (ret == l_True ? 10 : ret == l_False ? 20 : 0); -#endif - } catch (OutOfMemoryException&){ - printf("c ===================================================================================================\n"); - printf("INDETERMINATE\n"); - exit(0); - } -} diff --git a/core/Solver.cc b/core/Solver.cc index 38f60a4..81bf372 100644 --- a/core/Solver.cc +++ b/core/Solver.cc @@ -9,19 +9,19 @@ Labri - Univ. Bordeaux, France Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of -Glucose (sources until 2013, Glucose 3.0, single core) are exactly the same as Minisat on which it +Glucose (sources until 2013, Glucose 3.0, single core) are exactly the same as Minisat on which it is based on. (see below). Glucose-Syrup sources are based on another copyright. Permissions and copyrights for the parallel version of Glucose-Syrup (the "Software") are granted, free of charge, to deal with the Software without restriction, including the rights to use, copy, modify, merge, publish, distribute, -sublicence, and/or sell copies of the Software, and to permit persons to whom the Software is +sublicence, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: - The above and below copyrights notices and this permission notice shall be included in all copies or substantial portions of the Software; - The parallel version of Glucose (all files modified since Glucose 3.0 releases, 2013) cannot -be used in any competitive event (sat competitions/evaluations) without the express permission of +be used in any competitive event (sat competitions/evaluations) without the express permission of the authors (Gilles Audemard / Laurent Simon). This is also the case for any competitive event using Glucose Parallel as an embedded SAT engine (single core or not). @@ -91,7 +91,8 @@ static IntOption opt_chanseok_limit(_cred, "co", "Chanseok Oh: all learnt clause static IntOption opt_lb_size_minimzing_clause(_cm, "minSizeMinimizingClause", "The min size required to minimize clause", 30, IntRange(3, INT32_MAX)); static IntOption opt_lb_lbd_minimzing_clause(_cm, "minLBDMinimizingClause", "The min LBD required to minimize clause", 6, IntRange(3, INT32_MAX)); - +static BoolOption opt_lcm(_cm, "lcm", "Use inprocessing vivif (ijcai17 paper)", true); +static BoolOption opt_lcm_update_lbd(_cm, "lcm-update", "Updates LBD when doing LCM", false); static DoubleOption opt_var_decay(_cat, "var-decay", "The variable activity decay factor (starting point)", 0.8, DoubleRange(0, false, 1, false)); static DoubleOption opt_max_var_decay(_cat, "max-var-decay", "The variable activity decay factor", 0.95, DoubleRange(0, false, 1, false)); @@ -138,6 +139,8 @@ verbosity(0) , coLBDBound (opt_chanseok_limit) , lbSizeMinimizingClause(opt_lb_size_minimzing_clause) , lbLBDMinimizingClause(opt_lb_lbd_minimzing_clause) +, useLCM(opt_lcm) +, LCMUpdateLBD (opt_lcm_update_lbd) , var_decay(opt_var_decay) , max_var_decay(opt_max_var_decay) , clause_decay(opt_clause_decay) @@ -192,6 +195,8 @@ verbosity(0) , totalTime4Unsat(0.) , nbSatCalls(0) , nbUnsatCalls(0) + // simplify +, performLCM(1) { MYFLAG = 0; // Initialize only first time. Useful for incremental solving (not in // version), useless otherwise @@ -222,6 +227,8 @@ Solver::Solver(const Solver &s) : , coLBDBound (opt_chanseok_limit) , lbSizeMinimizingClause(s.lbSizeMinimizingClause) , lbLBDMinimizingClause(s.lbLBDMinimizingClause) +, useLCM(s.useLCM) +, LCMUpdateLBD (s.LCMUpdateLBD) , var_decay(s.var_decay) , max_var_decay(s.max_var_decay) , clause_decay(s.clause_decay) @@ -277,6 +284,7 @@ Solver::Solver(const Solver &s) : , totalTime4Unsat(s.totalTime4Unsat) , nbSatCalls(s.nbSatCalls) , nbUnsatCalls(s.nbUnsatCalls) +, performLCM(s.performLCM) { // Copy clauses. s.ca.copyTo(ca); @@ -305,11 +313,14 @@ Solver::Solver(const Solver &s) : s.clauses.memCopyTo(clauses); s.learnts.memCopyTo(learnts); s.permanentLearnts.memCopyTo(permanentLearnts); + s.permanentLearntsReduced.memCopyTo(permanentLearntsReduced); s.lbdQueue.copyTo(lbdQueue); s.trailQueue.copyTo(trailQueue); s.forceUNSAT.copyTo(forceUNSAT); s.stats.copyTo(stats); + + } @@ -388,6 +399,8 @@ Var Solver::newVar(bool sign, bool dvar) { decision.push(); trail.capacity(v + 1); setDecisionVar(v, dvar); + + return v; } @@ -421,27 +434,8 @@ bool Solver::addClause_(vec &ps) { ps.shrink(i - j); if(flag && (certifiedUNSAT)) { - if(vbyte) { - write_char('a'); - for(i = j = 0, p = lit_Undef; i < ps.size(); i++) - write_lit(2 * (var(ps[i]) + 1) + sign(ps[i])); - write_lit(0); - - write_char('d'); - for(i = j = 0, p = lit_Undef; i < oc.size(); i++) - write_lit(2 * (var(oc[i]) + 1) + sign(oc[i])); - write_lit(0); - } - else { - for(i = j = 0, p = lit_Undef; i < ps.size(); i++) - fprintf(certifiedOutput, "%i ", (var(ps[i]) + 1) * (-2 * sign(ps[i]) + 1)); - fprintf(certifiedOutput, "0\n"); - - fprintf(certifiedOutput, "d "); - for(i = j = 0, p = lit_Undef; i < oc.size(); i++) - fprintf(certifiedOutput, "%i ", (var(oc[i]) + 1) * (-2 * sign(oc[i]) + 1)); - fprintf(certifiedOutput, "0\n"); - } + addToDrat(ps,true); + addToDrat(oc, false); } @@ -454,6 +448,7 @@ bool Solver::addClause_(vec &ps) { CRef cr = ca.alloc(ps, false); clauses.push(cr); attachClause(cr); + } return true; @@ -531,18 +526,7 @@ void Solver::removeClause(CRef cr, bool inPurgatory) { Clause &c = ca[cr]; if(certifiedUNSAT) { - if(vbyte) { - write_char('d'); - for(int i = 0; i < c.size(); i++) - write_lit(2 * (var(c[i]) + 1) + sign(c[i])); - write_lit(0); - } - else { - fprintf(certifiedOutput, "d "); - for(int i = 0; i < c.size(); i++) - fprintf(certifiedOutput, "%i ", (var(c[i]) + 1) * (-2 * sign(c[i]) + 1)); - fprintf(certifiedOutput, "0\n"); - } + addToDrat(c, false); } if(inPurgatory) @@ -570,43 +554,6 @@ bool Solver::satisfied(const Clause &c) const { } -/************************************************************ - * Compute LBD functions - *************************************************************/ - -template inline unsigned int Solver::computeLBD(const T &lits, int end) { - int nblevels = 0; - MYFLAG++; -#ifdef INCREMENTAL - if(incremental) { // ----------------- INCREMENTAL MODE - if(end==-1) end = lits.size(); - int nbDone = 0; - for(int i=0;i=end) break; - if(isSelector(var(lits[i]))) continue; - nbDone++; - int l = level(var(lits[i])); - if (permDiff[l] != MYFLAG) { - permDiff[l] = MYFLAG; - nblevels++; - } - } - } else { // -------- DEFAULT MODE. NOT A LOT OF DIFFERENCES... BUT EASIER TO READ -#endif - for(int i = 0; i < lits.size(); i++) { - int l = level(var(lits[i])); - if(permDiff[l] != MYFLAG) { - permDiff[l] = MYFLAG; - nblevels++; - } - } -#ifdef INCREMENTAL - } -#endif - return nblevels; -} - - /****************************************************************** * Minimisation with binary reolution @@ -718,19 +665,19 @@ Lit Solver::pickBranchLit() { /*_________________________________________________________________________________________________ | | analyze : (confl : Clause*) (out_learnt : vec&) (out_btlevel : int&) -> [void] -| +| | Description: | Analyze conflict and produce a reason clause. -| +| | Pre-conditions: | * 'out_learnt' is assumed to be cleared. | * Current decision level must be greater than root level. -| +| | Post-conditions: | * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'. -| * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the +| * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the | rest of literals. There may be others from the same level though. -| +| |________________________________________________________________________________________________@*/ void Solver::analyze(CRef confl, vec &out_learnt, vec &selectors, int &out_btlevel, unsigned int &lbd, unsigned int &szWithoutSelectors) { int pathC = 0; @@ -963,7 +910,7 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels) { /*_________________________________________________________________________________________________ | | analyzeFinal : (p : Lit) -> [void] -| +| | Description: | Specialized analysis procedure to express the final conflict in terms of assumptions. | Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and @@ -1019,11 +966,11 @@ void Solver::bumpForceUNSAT(Lit q) { /*_________________________________________________________________________________________________ | | propagate : [void] -> [Clause*] -| +| | Description: | Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned, | otherwise CRef_Undef. -| +| | Post-conditions: | * the propagation queue is empty, even if there was a conflict. |________________________________________________________________________________________________@*/ @@ -1155,11 +1102,11 @@ CRef Solver::propagate() { /*_________________________________________________________________________________________________ | | propagateUnaryWatches : [Lit] -> [Clause*] -| +| | Description: -| Propagates unary watches of Lit p, return a conflict +| Propagates unary watches of Lit p, return a conflict | otherwise CRef_Undef -| +| |________________________________________________________________________________________________@*/ CRef Solver::propagateUnaryWatches(Lit p) { @@ -1240,7 +1187,7 @@ CRef Solver::propagateUnaryWatches(Lit p) { /*_________________________________________________________________________________________________ | | reduceDB : () -> [void] -| +| | Description: | Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked | clauses are clauses that are reason to some assignment. Binary clauses are never removed. @@ -1251,6 +1198,15 @@ void Solver::reduceDB() { int i, j; stats[nbReduceDB]++; + + if (!chanseokStrategy) { // We will use the LBD, but keep 10% of the best active clauses + sort(learnts, reduceDBAct_lt(ca)); + for(int i=learnts.size()*90/100;i 2 && c.size() > 2 && c.canBeDel() && !locked(c) && (i < limit)) { + //mostActiveClauses.push(learnts[i]); removeClause(learnts[i]); stats[nbRemovedClauses]++; } @@ -1280,6 +1237,8 @@ void Solver::reduceDB() { } } learnts.shrink(i - j); + + checkGarbage(); } @@ -1291,10 +1250,13 @@ void Solver::removeSatisfied(vec &cs) { Clause &c = ca[cs[i]]; - if(satisfied(c)) if(c.getOneWatched()) + if(satisfied(c)) + if(c.getOneWatched()) removeClause(cs[i], true); - else - removeClause(cs[i]); + else { + //// simplify + removeClause(cs[i]); + } else cs[j++] = cs[i]; } @@ -1315,7 +1277,7 @@ void Solver::rebuildOrderHeap() { /*_________________________________________________________________________________________________ | | simplify : [void] -> [bool] -| +| | Description: | Simplify the clause database according to the current top-level assigment. Currently, the only | thing done here is the removal of satisfied clauses, but more things can be put here. @@ -1338,6 +1300,7 @@ bool Solver::simplify() { // Remove satisfied clauses: removeSatisfied(learnts); removeSatisfied(permanentLearnts); + removeSatisfied(permanentLearntsReduced); removeSatisfied(unaryWatchedClauses); if(remove_satisfied) // Can be turned off. removeSatisfied(clauses); @@ -1355,11 +1318,12 @@ void Solver::adaptSolver() { bool adjusted = false; bool reinit = false; printf("c\nc Try to adapt solver strategies\nc \n"); - /* printf("c Adjusting solver for the SAT Race 2015 (alpha feature)\n"); - printf("c key successive Conflicts : %" PRIu64"\n",stats[noDecisionConflict]); + printf("c Adjusting solver for the SAT Race 2015 (alpha feature)\n"); + /*printf("c key successive Conflicts : %" PRIu64"\n",stats[noDecisionConflict]); printf("c nb unary clauses learnt : %" PRIu64"\n",stats[nbUn]); - printf("c key avg dec per conflicts : %.2f\n", (float)decisions / (float)conflicts);*/ - float decpc = (float) decisions / (float) conflicts; + printf("c key avg dec per conflicts : %.2f\n", (float)decisions / (float)conflicts); + printf("c avg learnt clauses : %" PRIu64"\n", stats[sumSizes]/conflicts); + */float decpc = (float) decisions / (float) conflicts; if(decpc <= 1.2) { chanseokStrategy = true; coLBDBound = 4; @@ -1433,13 +1397,13 @@ void Solver::adaptSolver() { learnts.shrink(learnts.size()); checkGarbage(); /* - order_heap.clear(); - for(int i=0;i [lbool] -| +| | Description: -| Search for a model the specified number of conflicts. +| Search for a model the specified number of conflicts. | NOTE! Use negative value for 'nof_conflicts' indicate infinity. -| +| | Output: | 'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If | all variables are decision variables, this means that the clause set is satisfiable. 'l_False' @@ -1470,6 +1434,20 @@ lbool Solver::search(int nof_conflicts) { bool aDecisionWasMade = false; starts++; + + // simplify + if (useLCM && performLCM){ + //printf("###simplifyAll: %lld\n", conflicts); + sort(learnts, reduceDB_lt(ca)); + //printf("nbClauses : %d, nbLearnts : %d\n", clauses.size(), learnts.size()); + if (!simplifyAll()) + { + return l_False; + } + performLCM = 0; + } + + for(; ;) { if(decisionLevel() == 0) { // We import clauses FIXME: ensure that we will import clauses enventually (restart after some point) parallelImportUnaryClauses(); @@ -1532,25 +1510,15 @@ lbool Solver::search(int nof_conflicts) { analyze(confl, learnt_clause, selectors, backtrack_level, nblevels, szWithoutSelectors); + stats[sumSizes]+= learnt_clause.size(); lbdQueue.push(nblevels); sumLBD += nblevels; cancelUntil(backtrack_level); - if(certifiedUNSAT) { - if(vbyte) { - write_char('a'); - for(int i = 0; i < learnt_clause.size(); i++) - write_lit(2 * (var(learnt_clause[i]) + 1) + sign(learnt_clause[i])); - write_lit(0); - } - else { - for(int i = 0; i < learnt_clause.size(); i++) - fprintf(certifiedOutput, "%i ", (var(learnt_clause[i]) + 1) * - (-2 * sign(learnt_clause[i]) + 1)); - fprintf(certifiedOutput, "0\n"); - } - } + if(certifiedUNSAT) + addToDrat(learnt_clause, true); + if(learnt_clause.size() == 1) { @@ -1577,6 +1545,8 @@ lbool Solver::search(int nof_conflicts) { if(ca[cr].size() == 2) stats[nbBin]++; // stats attachClause(cr); lastLearntClause = cr; // Use in multithread (to hard to put inside ParallelSolver) + + parallelExportClauseDuringSearch(ca[cr]); uncheckedEnqueue(learnt_clause[0], cr); @@ -1618,6 +1588,7 @@ lbool Solver::search(int nof_conflicts) { if(learnts.size() > 0) { curRestart = (conflicts / nbclausesbeforereduce) + 1; reduceDB(); + performLCM = 1; if(!panicModeIsEnabled()) nbclausesbeforereduce += incReduceDB; } @@ -1843,7 +1814,7 @@ lbool Solver::solve_(bool do_simp, bool turn_off_simp) // Parameters are useless //================================================================================================= // Writing CNF to DIMACS: -// +// // FIXME: this needs to be rewritten completely. static Var mapVar(Var x, vec &map, Var &max) { @@ -1958,6 +1929,9 @@ void Solver::relocAll(ClauseAllocator &to) { for(int i = 0; i < permanentLearnts.size(); i++) ca.reloc(permanentLearnts[i], to); + for(int i = 0; i < permanentLearntsReduced.size(); i++) + ca.reloc(permanentLearntsReduced[i], to); + // All original: // for(int i = 0; i < clauses.size(); i++) @@ -1999,11 +1973,11 @@ bool Solver::parallelImportClauses() { } -void Solver::parallelExportUnaryClause(Lit p) { +void Solver::parallelExportUnaryClause(Lit) { } -void Solver::parallelExportClauseDuringSearch(Clause &c) { +void Solver::parallelExportClauseDuringSearch(Clause &) { } @@ -2013,5 +1987,5 @@ bool Solver::parallelJobIsFinished() { } -void Solver::parallelImportClauseDuringConflictAnalysis(Clause &c, CRef confl) { +void Solver::parallelImportClauseDuringConflictAnalysis(Clause &, CRef ) { } diff --git a/core/Solver.h b/core/Solver.h index 54335ff..9adc272 100644 --- a/core/Solver.h +++ b/core/Solver.h @@ -62,11 +62,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA namespace Glucose { // Core stats - + enum CoreStats { sumResSeen, sumRes, - sumTrail, + sumTrail, nbPromoted, originalClausesSeen, sumDecisionLevels, @@ -87,10 +87,13 @@ enum CoreStats { learnts_literals, max_literals, tot_literals, - noDecisionConflict + noDecisionConflict, + lcmtested, + lcmreduced, + sumSizes } ; -#define coreStatsSize 24 +#define coreStatsSize 27 //================================================================================================= // Solver -- the main class: @@ -104,24 +107,24 @@ class Solver : public Clone { // Solver(); Solver(const Solver &s); - + virtual ~Solver(); - + /** * Clone function */ virtual Clone* clone() const { return new Solver(*this); - } + } // Problem specification: // virtual Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode. - bool addClause (const vec& ps); // Add a clause to the solver. + bool addClause (const vec& ps); // Add a clause to the solver. bool addEmptyClause(); // Add the empty clause, making the solver contradictory. - bool addClause (Lit p); // Add a unit clause to the solver. - bool addClause (Lit p, Lit q); // Add a binary clause to the solver. - bool addClause (Lit p, Lit q, Lit r); // Add a ternary clause to the solver. + bool addClause (Lit p); // Add a unit clause to the solver. + bool addClause (Lit p, Lit q); // Add a binary clause to the solver. + bool addClause (Lit p, Lit q, Lit r); // Add a ternary clause to the solver. virtual bool addClause_( vec& ps); // Add a clause to the solver without making superflous internal copy. Will // change the passed vector 'ps'. // Solving: @@ -143,14 +146,14 @@ class Solver : public Clone { void toDimacs (const char* file, Lit p); void toDimacs (const char* file, Lit p, Lit q); void toDimacs (const char* file, Lit p, Lit q, Lit r); - + // Display clauses and literals void printLit(Lit l); void printClause(CRef c); void printInitialClause(CRef c); - + // Variable mode: - // + // void setPolarity (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'. void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic. @@ -198,7 +201,7 @@ class Solver : public Clone { int verbosity; int verbEveryConflicts; int showModel; - + // Constants For restarts double K; double R; @@ -215,6 +218,8 @@ class Solver : public Clone { // Constant for reducing clause int lbSizeMinimizingClause; unsigned int lbLBDMinimizingClause; + bool useLCM; // See ijcai17 (Chu Min Li paper, related to vivif). + bool LCMUpdateLBD; // Updates the LBD when shrinking/replacing a clause with the vivification // Constant for heuristic double var_decay; @@ -228,7 +233,7 @@ class Solver : public Clone { bool rnd_init_act; // Initialize variable activities with a small random value. bool randomizeFirstDescent; // the first decisions (until first cnflict) are made randomly // Useful for syrup! - + // Constant for Memory managment double garbage_frac; // The fraction of wasted memory allowed before a garbage collection is triggered. @@ -240,17 +245,17 @@ class Solver : public Clone { void write_char (unsigned char c); void write_lit (int n); + template void addToDrat(T & lits, bool add); - - // Panic mode. + // Panic mode. // Save memory uint32_t panicModeLastRemoved, panicModeLastRemovedShared; - + bool useUnaryWatched; // Enable unary watched literals bool promoteOneWatchedClause; // One watched clauses are promotted to two watched clauses if found empty - + // Functions useful for multithread solving - // Useless in the sequential case + // Useless in the sequential case // Overide in ParallelSolver virtual void parallelImportClauseDuringConflictAnalysis(Clause &c,CRef confl); virtual bool parallelImportClauses(); // true if the empty clause was received @@ -259,13 +264,13 @@ class Solver : public Clone { virtual void parallelExportClauseDuringSearch(Clause &c); virtual bool parallelJobIsFinished(); virtual bool panicModeIsEnabled(); - - + + double luby(double y, int x); - - // Statistics + + // Statistics vec stats; - + // Important stats completely related to search. Keep here uint64_t solves,starts,decisions,propagations,conflicts,conflictsRestarts; @@ -331,7 +336,9 @@ class Solver : public Clone { vec clauses; // List of problem clauses. vec learnts; // List of learnt clauses. vec permanentLearnts; // The list of learnts clauses kept permanently + vec permanentLearntsReduced; // The list of learnts clauses kept permanently that have been reduced by LCM vec unaryWatchedClauses; // List of imported clauses (after the purgatory) // TODO put inside ParallelSolver + vec mostActiveClauses; // Used to keep most active clauses (instead of removing them) vec assigns; // The current assignments. vec polarity; // The preferred polarity of each variable. @@ -351,15 +358,15 @@ class Solver : public Clone { double progress_estimate;// Set by 'search()'. bool remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'. vec permDiff; // permDiff[var] contains the current conflict number... Used to count the number of LBD - + // UPDATEVARACTIVITY trick (see competition'09 companion paper) - vec lastDecisionLevel; + vec lastDecisionLevel; ClauseAllocator ca; int nbclausesbeforereduce; // To know when it is time to reduce clause database - + // Used for restart strategies bqueue trailQueue,lbdQueue; // Bounded queues for restarts. float sumLBD; // used to compute the global average of LBD. Restarts... @@ -462,6 +469,35 @@ class Solver : public Clone { // Returns a random integer 0 <= x < size. Seed must never be 0. static inline int irand(double& seed, int size) { return (int)(drand(seed) * size); } + + + // simplify + // +public: + bool simplifyAll(); + void simplifyLearnt(Clause& c); + int trailRecord; + void litsEnqueue(int cutP, Clause& c); + void cancelUntilTrailRecord(); + void simpleUncheckEnqueue(Lit p, CRef from = CRef_Undef); + CRef simplePropagate(); + CRef simplePropagateUnaryWatches(Lit p); + + vec simp_learnt_clause; + vec simp_reason_clause; + void simpleAnalyze(CRef confl, vec& out_learnt, vec& reason_clause, bool True_confl); + // sort learnt clause literal by litValue + + // in redundant + bool removed(CRef cr); + int performLCM; + + //// test + vec valueDup; + void compareValue(); + void wholeCompareValue(); + + }; @@ -507,12 +543,12 @@ inline bool Solver::addEmptyClause () { add_tmp.clear( inline bool Solver::addClause (Lit p) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); } inline bool Solver::addClause (Lit p, Lit q) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); } inline bool Solver::addClause (Lit p, Lit q, Lit r) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); } - inline bool Solver::locked (const Clause& c) const { - if(c.size()>2) - return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; - return + inline bool Solver::locked (const Clause& c) const { + if(c.size()>2) + return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; + return (value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c) - || + || (value(c[1]) == l_True && reason(var(c[1])) != CRef_Undef && ca.lea(reason(var(c[1]))) == &c); } inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } @@ -527,12 +563,12 @@ inline int Solver::nAssigns () const { return trail.size(); } inline int Solver::nClauses () const { return clauses.size(); } inline int Solver::nLearnts () const { return learnts.size(); } inline int Solver::nVars () const { return vardata.size(); } -inline int Solver::nFreeVars () { +inline int Solver::nFreeVars () { int a = stats[dec_vars]; return (int)(a) - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); } inline void Solver::setPolarity (Var v, bool b) { polarity[v] = b; } -inline void Solver::setDecisionVar(Var v, bool b) -{ +inline void Solver::setDecisionVar(Var v, bool b) +{ if ( b && !decision[v]) stats[dec_vars]++; else if (!b && decision[v]) stats[dec_vars]--; @@ -566,6 +602,43 @@ inline void Solver::toDimacs (const char* file, Lit p, Lit q){ vec inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ vec as; as.push(p); as.push(q); as.push(r); toDimacs(file, as); } +/************************************************************ + * Compute LBD functions + *************************************************************/ + +template inline unsigned int Solver::computeLBD(const T &lits, int end) { + int nblevels = 0; + MYFLAG++; +#ifdef INCREMENTAL + if(incremental) { // ----------------- INCREMENTAL MODE + if(end==-1) end = lits.size(); + int nbDone = 0; + for(int i=0;i=end) break; + if(isSelector(var(lits[i]))) continue; + nbDone++; + int l = level(var(lits[i])); + if (permDiff[l] != MYFLAG) { + permDiff[l] = MYFLAG; + nblevels++; + } + } + } else { // -------- DEFAULT MODE. NOT A LOT OF DIFFERENCES... BUT EASIER TO READ +#endif + for(int i = 0; i < lits.size(); i++) { + int l = level(var(lits[i])); + if(permDiff[l] != MYFLAG) { + permDiff[l] = MYFLAG; + nblevels++; + } + } +#ifdef INCREMENTAL + } +#endif + return nblevels; +} + + //================================================================================================= // Debug etc: @@ -597,6 +670,28 @@ inline void Solver::printInitialClause(CRef cr) } } +template inline void Solver::addToDrat(T &lits, bool add) { + if(vbyte) { + if(add) + write_char('a'); + else + write_char('d'); + for(int i = 0; i < lits.size(); i++) + write_lit(2 * (var(lits[i]) + 1) + sign(lits[i])); + write_lit(0); + } + else { + if(!add) + fprintf(certifiedOutput, "d "); + + for(int i = 0; i < lits.size(); i++) + fprintf(certifiedOutput, "%i ", (var(lits[i]) + 1) * (-2 * sign(lits[i]) + 1)); + fprintf(certifiedOutput, "0\n"); + } +} + + + //================================================================================================= struct reduceDBAct_lt { ClauseAllocator& ca; @@ -639,7 +734,7 @@ struct reduceDB_lt { return ca[x].activity() < ca[y].activity(); //return x->size() < y->size(); - //return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); } + //return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); } } }; diff --git a/core/SolverTypes.h b/core/SolverTypes.h index 422ec78..3eb52b7 100644 --- a/core/SolverTypes.h +++ b/core/SolverTypes.h @@ -152,7 +152,7 @@ inline lbool toLbool(int v) { return lbool((uint8_t)v); } class Clause; typedef RegionAllocator::Ref CRef; -#define BITS_LBD 20 +#define BITS_LBD 19 #ifdef INCREMENTAL #define BITS_SIZEWITHOUTSEL 19 #endif @@ -167,6 +167,8 @@ class Clause { unsigned reloced : 1; unsigned exported : 2; // Values to keep track of the clause status for exportations unsigned oneWatched : 1; + //simplify + unsigned simplified : 1; unsigned lbd : BITS_LBD; unsigned size : BITS_REALSIZE; @@ -183,7 +185,7 @@ class Clause { // NOTE: This constructor cannot be used directly (doesn't allocate enough memory). template Clause(const V& ps, int _extra_size, bool learnt) { - assert(_extra_size < (1<<2)); + assert(_extra_size < 3); header.mark = 0; header.learnt = learnt; header.extra_size = _extra_size; @@ -193,7 +195,9 @@ class Clause { header.canbedel = 1; header.exported = 0; header.oneWatched = 0; - header.seen = 0; + header.simplified = 0; + + header.seen = 0; for (int i = 0; i < ps.size(); i++) data[i].lit = ps[i]; @@ -221,7 +225,7 @@ class Clause { if (header.extra_size > 0) { data[header.size-i] = data[header.size]; if (header.extra_size > 1) { // Special case for imported clauses - data[header.size-i-1] = data[header.size-1]; + data[header.size-i+1] = data[header.size+1]; } } header.size -= i; } @@ -264,7 +268,13 @@ class Clause { unsigned int getExported() {return header.exported;} void setOneWatched(bool b) {header.oneWatched = b;} bool getOneWatched() {return header.oneWatched;} -#ifdef INCREMNENTAL + + // simplify + // + void setSimplified(bool b) { header.simplified = b; } + bool simplified() { return header.simplified; } + +#ifdef INCREMENTAL void setSizeWithoutSelectors (unsigned int n) {header.szWithoutSelectors = n; } unsigned int sizeWithoutSelectors () const { return header.szWithoutSelectors; } #endif @@ -298,7 +308,7 @@ class Clause { assert(sizeof(float) == sizeof(uint32_t)); bool use_extra = learnt | extra_clause_field; - int extra_size = imported?3:(use_extra?1:0); + int extra_size = imported?2:(use_extra?1:0); CRef cid = RegionAllocator::alloc(clauseWord32Size(ps.size(), extra_size)); new (lea(cid)) Clause(ps, extra_size, learnt); @@ -335,6 +345,10 @@ class Clause { to[cr].setLBD(c.lbd()); to[cr].setExported(c.getExported()); to[cr].setOneWatched(c.getOneWatched()); + // simplify + // + to[cr].setSimplified(c.simplified()); + #ifdef INCREMENTAL to[cr].setSizeWithoutSelectors(c.sizeWithoutSelectors()); #endif diff --git a/core/lcm.cc b/core/lcm.cc new file mode 100644 index 0000000..67ab9d9 --- /dev/null +++ b/core/lcm.cc @@ -0,0 +1,535 @@ +#include "Solver.h" +#include "mtl/Sort.h" +using namespace Glucose; + + + +// simplify All +// +CRef Solver::simplePropagate() +{ + CRef confl = CRef_Undef; + int num_props = 0; + watches.cleanAll(); + watchesBin.cleanAll(); + while (qhead < trail.size()){ + Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate. + vec& ws = watches[p]; + Watcher *i, *j, *end; + num_props++; + + // First, Propagate binary clauses + vec& wbin = watchesBin[p]; + + for (int k = 0; kblocker; + if (value(blocker) == l_True){ + *j++ = *i++; continue; + } + + // Make sure the false literal is data[1]: + CRef cr = i->cref; + Clause& c = ca[cr]; + Lit false_lit = ~p; + if (c[0] == false_lit) + c[0] = c[1], c[1] = false_lit; + assert(c[1] == false_lit); + // i++; + + // If 0th watch is true, then clause is already satisfied. + // However, 0th watch is not the blocker, make it blocker using a new watcher w + // why not simply do i->blocker=first in this case? + Lit first = c[0]; + // Watcher w = Watcher(cr, first); + if (first != blocker && value(first) == l_True){ + i->blocker = first; + *j++ = *i++; continue; + } + + // Look for new watch: + if (incremental){ // ----------------- INCREMENTAL MODE + int choosenPos = -1; + for (int k = 2; k < c.size(); k++){ + if (value(c[k]) != l_False){ + if (decisionLevel()>assumptions.size()){ + choosenPos = k; + break; + } + else{ + choosenPos = k; + + if (value(c[k]) == l_True || !isSelector(var(c[k]))) { + break; + } + } + + } + } + if (choosenPos != -1){ + // watcher i is abandonned using i++, because cr watches now ~c[k] instead of p + // the blocker is first in the watcher. However, + // the blocker in the corresponding watcher in ~first is not c[1] + Watcher w = Watcher(cr, first); i++; + c[1] = c[choosenPos]; c[choosenPos] = false_lit; + watches[~c[1]].push(w); + goto NextClause; + } + } + else{ // ----------------- DEFAULT MODE (NOT INCREMENTAL) + for (int k = 2; k < c.size(); k++){ + + if (value(c[k]) != l_False){ + // watcher i is abandonned using i++, because cr watches now ~c[k] instead of p + // the blocker is first in the watcher. However, + // the blocker in the corresponding watcher in ~first is not c[1] + Watcher w = Watcher(cr, first); i++; + c[1] = c[k]; c[k] = false_lit; + watches[~c[1]].push(w); + goto NextClause; + } + } + } + + // Did not find watch -- clause is unit under assignment: + i->blocker = first; + *j++ = *i++; + if (value(first) == l_False){ + confl = cr; + qhead = trail.size(); + // Copy the remaining watches: + while (i < end) + *j++ = *i++; + } + else{ + simpleUncheckEnqueue(first, cr); + } + NextClause:; + } + ws.shrink(i - j); + + // unaryWatches "propagation" + if(useUnaryWatched && confl == CRef_Undef) { + confl = simplePropagateUnaryWatches(p); + + } + } + + + return confl; +} + +CRef Solver::simplePropagateUnaryWatches(Lit p) { + CRef confl = CRef_Undef; + Watcher *i, *j, *end; + vec &ws = unaryWatches[p]; + for(i = j = (Watcher *) ws, end = i + ws.size(); i != end;) { + // Try to avoid inspecting the clause: + Lit blocker = i->blocker; + if(value(blocker) == l_True) { + *j++ = *i++; + continue; + } + + // Make sure the false literal is data[1]: + CRef cr = i->cref; + Clause &c = ca[cr]; + assert(c.getOneWatched()); + Lit false_lit = ~p; + assert(c[0] == false_lit); // this is unary watch... No other choice if "propagated" + //if (c[0] == false_lit) + //c[0] = c[1], c[1] = false_lit; + //assert(c[1] == false_lit); + i++; + Watcher w = Watcher(cr, c[0]); + for(int k = 1; k < c.size(); k++) { + if(value(c[k]) != l_False) { + c[0] = c[k]; + c[k] = false_lit; + unaryWatches[~c[0]].push(w); + goto NextClauseUnary; + } + } + + // Did not find watch -- clause is empty under assignment: + *j++ = w; + + confl = cr; + qhead = trail.size(); + // Copy the remaining watches: + while(i < end) + *j++ = *i++; + + NextClauseUnary:; + } + ws.shrink(i - j); + + return confl; +} + + +void Solver::simpleUncheckEnqueue(Lit p, CRef from){ + assert(value(p) == l_Undef); + assigns[var(p)] = lbool(!sign(p)); // this makes a lbool object whose value is sign(p) + vardata[var(p)].reason = from; + trail.push_(p); +} + +void Solver::cancelUntilTrailRecord() +{ + for (int c = trail.size() - 1; c >= trailRecord; c--) + { + Var x = var(trail[c]); + assigns[x] = l_Undef; + + } + qhead = trailRecord; + trail.shrink(trail.size() - trailRecord); + +} + +void Solver::litsEnqueue(int cutP, Clause& c) +{ + for (int i = cutP; i < c.size(); i++) + { + simpleUncheckEnqueue(~c[i]); + } +} + +bool Solver::removed(CRef cr) { + return ca[cr].mark() == 1; +} + +void Solver::simpleAnalyze(CRef confl, vec& out_learnt, vec& reason_clause, bool True_confl) +{ + int pathC = 0; + Lit p = lit_Undef; + int index = trail.size() - 1; + + do{ + if (confl != CRef_Undef){ + reason_clause.push(confl); + Clause& c = ca[confl]; + // Special case for binary clauses + // The first one has to be SAT + if (p != lit_Undef && c.size() == 2 && value(c[0]) == l_False) { + + assert(value(c[1]) == l_True); + Lit tmp = c[0]; + c[0] = c[1], c[1] = tmp; + } + // if True_confl==true, then choose p begin with the 1th index of c; + for (int j = (p == lit_Undef && True_confl == false) ? 0 : 1; j < c.size(); j++){ + Lit q = c[j]; + if (!seen[var(q)]){ + seen[var(q)] = 1; + pathC++; + } + } + } + else if (confl == CRef_Undef){ + out_learnt.push(~p); + } + // if not break, while() will come to the index of trail blow 0, and fatal error occur; + if (pathC == 0) break; + // Select next clause to look at: + while (!seen[var(trail[index--])]); + // if the reason cr from the 0-level assigned var, we must break avoid move forth further; + // but attention that maybe seen[x]=1 and never be clear. However makes no matter; + if (trailRecord > index + 1) break; + p = trail[index + 1]; + confl = reason(var(p)); + seen[var(p)] = 0; + pathC--; + + } while (pathC >= 0); +} + +void Solver::simplifyLearnt(Clause& c) +{ + stats[lcmtested]++; + + trailRecord = trail.size();// record the start pointer + + vec falseLit; + + falseLit.clear(); + + bool True_confl = false; + int beforeSize, afterSize; + beforeSize = c.size(); + int i, j; + CRef confl; + + for (i = 0, j = 0; i < c.size(); i++){ + if (value(c[i]) == l_Undef){ + //printf("///@@@ uncheckedEnqueue:index = %d. l_Undef\n", i); + simpleUncheckEnqueue(~c[i]); + c[j++] = c[i]; + confl = simplePropagate(); + if (confl != CRef_Undef){ + break; + } + } + else{ + if (value(c[i]) == l_True){ + //printf("///@@@ uncheckedEnqueue:index = %d. l_True\n", i); + c[j++] = c[i]; + True_confl = true; + confl = reason(var(c[i])); + break; + } + else{ + falseLit.push(c[i]); + //printf("///@@@ uncheckedEnqueue:index = %d. l_False\n", i); + } + } + } + c.shrink(c.size() - j); + if (LCMUpdateLBD && c.lbd() > c.size()) c.setLBD(c.size()); + afterSize = c.size(); + + if (confl != CRef_Undef || True_confl == true){ + simp_learnt_clause.clear(); + simp_reason_clause.clear(); + if (True_confl == true){ + simp_learnt_clause.push(c.last()); + } + simpleAnalyze(confl, simp_learnt_clause, simp_reason_clause, True_confl); + + if (simp_learnt_clause.size() < c.size()){ + for (i = 0; i < simp_learnt_clause.size(); i++){ + c[i] = simp_learnt_clause[i]; + } + c.shrink(c.size() - i); + if (LCMUpdateLBD) { + int nblevels = computeLBD(simp_learnt_clause); + if (nblevels < c.lbd()) + c.setLBD(nblevels); + } + } + } + + cancelUntilTrailRecord(); + +} + +bool Solver::simplifyAll() +{ + int nbGoodReduce = 0; + int beforeSize, afterSize; + int nbSize1 = 0, nbSize2 = 0; + + if (!ok || propagate() != CRef_Undef) + return ok = false; + + removeSatisfied(clauses); + + int ci, cj, li, lj; + bool sat, false_lit; + unsigned int nblevels; + vec ori_c; + + if (0 && chanseokStrategy && permanentLearnts.size() > 0) { + for (ci = 0, cj = 0; ci < permanentLearnts.size(); ci++){ + CRef cr = permanentLearnts[ci]; + Clause& c = ca[cr]; + + if (!removed(cr)){ + sat = false_lit = false; + for (int i = 0; i < c.size(); i++){ + if (value(c[i]) == l_True){ + sat = true; + break; + } + else if (value(c[i]) == l_False){ + false_lit = true; + } + } + if (sat){ + removeClause(cr); + } + else{ + detachClause(cr, true); + + if (false_lit){ + for (li = lj = 0; li < c.size(); li++){ + if (value(c[li]) != l_False){ + c[lj++] = c[li]; + } + } + c.shrink(li - lj); + if(certifiedUNSAT) + addToDrat(c, true); + } + //// + if (c.simplified() || c.lbd() > 3) { + attachClause(cr); + permanentLearntsReduced.push(cr); //[cj++] = permanentLearnts[ci]; + // permanentLearnts[cj++] = permanentLearnts[ci]; + continue; + } + + beforeSize = c.size(); + assert(c.size() > 1); + // simplify a learnt clause c + simplifyLearnt(c); + assert(c.size() > 0); + afterSize = c.size(); + + if (beforeSize > afterSize){ + if (afterSize <= 3) { + nbGoodReduce++; + if (afterSize > 1) parallelExportClauseDuringSearch(c); + if (afterSize == 2){ + nbSize2++; + } + } + if(certifiedOutput) + addToDrat(c, true); + stats[lcmreduced]++; + } + + if (c.size() == 1){ + nbSize1++; + // when unit clause occur, enqueue and propagate + uncheckedEnqueue(c[0]); + parallelExportUnaryClause(c[0]); + if (propagate() != CRef_Undef) + { + ok = false; + return false; + } + // delete the clause memory in logic + c.mark(1); + ca.free(cr); + } + else{ + attachClause(cr); + permanentLearntsReduced.push(cr); //[cj++] = permanentLearnts[ci]; + //permanentLearnts[cj++] = permanentLearnts[ci]; + // TODO + /*nblevels = computeLBD(c); + if (nblevels < c.lbd()){ + c.setLBD(nblevels); + }*/ + + c.setSimplified(true); + } + } + } + } + permanentLearnts.shrink(ci - cj); + } + + if (!chanseokStrategy) { + sort(learnts, reduceDB_lt(ca)); + + for (ci = 0, cj = 0; ci < learnts.size(); ci++){ + CRef cr = learnts[ci]; + Clause& c = ca[cr]; + + if (!removed(cr)){ + sat = false_lit = false; + for (int i = 0; i < c.size(); i++){ + if (value(c[i]) == l_True){ + sat = true; + break; + } + else if (value(c[i]) == l_False){ + false_lit = true; + } + } + if (sat){ + removeClause(cr); + } + else{ + detachClause(cr, true); + + if (false_lit){ + for (li = lj = 0; li < c.size(); li++){ + if (value(c[li]) != l_False){ + c[lj++] = c[li]; + } + } + c.shrink(li - lj); + if(certifiedUNSAT) + addToDrat(c, true); + } + //// + if (ci < learnts.size() / 2 || c.simplified()) { + attachClause(cr); + learnts[cj++] = learnts[ci]; + continue; + } + + beforeSize = c.size(); + assert(c.size() > 1); + // simplify a learnt clause c + simplifyLearnt(c); + assert(c.size() > 0); + afterSize = c.size(); + + if (beforeSize > afterSize){ + if (afterSize <= 3) { + nbGoodReduce++; + if (afterSize > 1) parallelExportClauseDuringSearch(c); + if (afterSize == 2){ + nbSize2++; + } + } + if(certifiedOutput) + addToDrat(c, true); + stats[lcmreduced]++; + } + + if (c.size() == 1){ + nbSize1++; + // when unit clause occur, enqueue and propagate + uncheckedEnqueue(c[0]); + parallelExportUnaryClause(c[0]); + if (propagate() != CRef_Undef) + { + ok = false; + return false; + } + // delete the clause memory in logic + c.mark(1); + ca.free(cr); + } + else{ + attachClause(cr); + learnts[cj++] = learnts[ci]; + // TODO + /*nblevels = computeLBD(c); + if (nblevels < c.lbd()){ + c.setLBD(nblevels); + }*/ + + c.setSimplified(true); + } + } + } + } + learnts.shrink(ci - cj); + } + + checkGarbage(); + + return true; +} + + + diff --git a/parallel/Main.cc b/parallel/Main.cc index ecc60cf..7f224a8 100644 --- a/parallel/Main.cc +++ b/parallel/Main.cc @@ -92,7 +92,7 @@ static void SIGINT_exit(int signum) { int main(int argc, char** argv) { double realTimeStart = realTime(); - printf("c\nc This is glucose-syrup 4.1 (glucose in many threads) -- based on MiniSAT (Many thanks to MiniSAT team)\nc\n"); + printf("c\nc This is glucose-syrup 4.2.1 (glucose in many threads) -- based on MiniSAT (Many thanks to MiniSAT team)\nc\n"); try { setUsageHelp("c USAGE: %s [options] \n\n where input may be either in plain or gzipped DIMACS.\n"); // printf("This is MiniSat 2.0 beta\n"); diff --git a/simp/Main.cc b/simp/Main.cc index fe05a59..c2327df 100644 --- a/simp/Main.cc +++ b/simp/Main.cc @@ -74,6 +74,7 @@ void printStats(Solver& solver) printf("c last block at restart : %" PRIu64"\n",solver.stats[lastblockatrestart]); printf("c nb ReduceDB : %" PRIu64"\n", solver.stats[nbReduceDB]); printf("c nb removed Clauses : %" PRIu64"\n",solver.stats[nbRemovedClauses]); + printf("c average learnt size : %" PRIu64"\n", solver.conflicts == 0 ? 0 : solver.stats[sumSizes]/solver.conflicts); printf("c nb learnts DL2 : %" PRIu64"\n", solver.stats[nbDL2]); printf("c nb learnts size 2 : %" PRIu64"\n", solver.stats[nbBin]); printf("c nb learnts size 1 : %" PRIu64"\n", solver.stats[nbUn]); @@ -86,7 +87,7 @@ void printStats(Solver& solver) // printf("c conflict literals : %-12" PRIu64" (%4.2f %% deleted)\n", solver.stats[tot_literals], (solver.stats[max_literals] - solver.stats[tot_literals])*100 / (double)solver.stats[max_literals]); // printf("c Average resolutions : %-12" PRIu64" (%.0f seen ones)\n",solver.stats[sumRes]/solver.conflicts,((double)solver.stats[sumResSeen])/solver.conflicts); printf("c nb reduced Clauses : %" PRIu64"\n",solver.stats[nbReducedClauses]); - + printf("c LCM : %" PRIu64" / %" PRIu64" \n", solver.stats[lcmreduced],solver.stats[lcmtested]); if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used); printf("c CPU time : %g s\n", cpu_time); } @@ -115,7 +116,7 @@ static void SIGINT_exit(int signum) { int main(int argc, char** argv) { try { - printf("c\nc This is glucose 4.1 -- based on MiniSAT (Many thanks to MiniSAT team)\nc\n"); + printf("c\nc This is glucose 4.2.1 -- based on MiniSAT (Many thanks to MiniSAT team)\nc\n"); setUsageHelp("c USAGE: %s [options] \n\n where input may be either in plain or gzipped DIMACS.\n"); diff --git a/simp/SimpSolver.cc b/simp/SimpSolver.cc index 7c36bd0..6e2f6ab 100644 --- a/simp/SimpSolver.cc +++ b/simp/SimpSolver.cc @@ -219,19 +219,8 @@ bool SimpSolver::addClause_(vec& ps) if (!Solver::addClause_(ps)) return false; - if(!parsing && certifiedUNSAT) { - if (vbyte) { - write_char('a'); - for (int i = 0; i < ps.size(); i++) - write_lit(2*(var(ps[i])+1) + sign(ps[i])); - write_lit(0); - } - else { - for (int i = 0; i < ps.size(); i++) - fprintf(certifiedOutput, "%i " , (var(ps[i]) + 1) * (-2 * sign(ps[i]) + 1) ); - fprintf(certifiedOutput, "0\n"); - } - } + if(!parsing && certifiedUNSAT) + addToDrat(ps, true); if (use_simplification && clauses.size() == nclauses + 1){ CRef cr = clauses.last(); @@ -302,20 +291,8 @@ bool SimpSolver::strengthenClause(CRef cr, Lit l) removeClause(cr); c.strengthen(l); }else{ - if (certifiedUNSAT) { - if (vbyte) { - write_char('d'); - for (int i = 0; i < c.size(); i++) - write_lit(2*(var(c[i])+1) + sign(c[i])); - write_lit(0); - } - else { - fprintf(certifiedOutput, "d "); - for (int i = 0; i < c.size(); i++) - fprintf(certifiedOutput, "%i " , (var(c[i]) + 1) * (-2 * sign(c[i]) + 1) ); - fprintf(certifiedOutput, "0\n"); - } - } + if (certifiedUNSAT) + addToDrat(c, false); detachClause(cr, true); c.strengthen(l);