From 27cf1a55a2a89c7e2143619b24a93c15af782002 Mon Sep 17 00:00:00 2001 From: audemard Date: Tue, 9 May 2023 11:55:07 +0200 Subject: [PATCH] Glucose 4.0 --- CHANGELOG | 27 + README.md | 30 +- core/BoundedQueue.h | 56 +- core/Constants.h | 46 +- core/Makefile | 7 +- core/Solver.cc | 1513 ++++++++++++++++++------------- core/Solver.h | 181 +++- core/SolverTypes.h | 145 ++- mtl/Alloc.h | 11 + mtl/Clone.h | 13 + mtl/Heap.h | 2 + mtl/Queue.h | 11 + mtl/Vec.h | 7 + mtl/template.mk | 4 +- parallel/ClausesBuffer.cc | 235 +++++ parallel/ClausesBuffer.h | 114 +++ parallel/Main.cc | 254 ++++++ parallel/Makefile | 4 + parallel/MultiSolvers.cc | 543 +++++++++++ parallel/MultiSolvers.h | 182 ++++ parallel/ParallelSolver.cc | 490 ++++++++++ parallel/ParallelSolver.h | 144 +++ parallel/SharedCompanion.cc | 167 ++++ parallel/SharedCompanion.h | 122 +++ parallel/SolverCompanion.cc | 87 ++ parallel/SolverCompanion.h | 79 ++ parallel/SolverConfiguration.cc | 131 +++ parallel/SolverConfiguration.h | 68 ++ simp/Main.cc | 109 ++- simp/SimpSolver.cc | 105 ++- simp/SimpSolver.h | 61 +- utils/Options.h | 6 +- utils/System.h | 7 + 33 files changed, 4186 insertions(+), 775 deletions(-) create mode 100644 CHANGELOG create mode 100644 mtl/Clone.h create mode 100644 parallel/ClausesBuffer.cc create mode 100644 parallel/ClausesBuffer.h create mode 100644 parallel/Main.cc create mode 100644 parallel/Makefile create mode 100644 parallel/MultiSolvers.cc create mode 100644 parallel/MultiSolvers.h create mode 100644 parallel/ParallelSolver.cc create mode 100644 parallel/ParallelSolver.h create mode 100644 parallel/SharedCompanion.cc create mode 100644 parallel/SharedCompanion.h create mode 100644 parallel/SolverCompanion.cc create mode 100644 parallel/SolverCompanion.h create mode 100644 parallel/SolverConfiguration.cc create mode 100644 parallel/SolverConfiguration.h diff --git a/CHANGELOG b/CHANGELOG new file mode 100644 index 0000000..aa5b70f --- /dev/null +++ b/CHANGELOG @@ -0,0 +1,27 @@ +Version 4.0 + - Add a Multithread version, called syrup (many glucose ;-) + See SAT14 paper: Lazy Clause Exchange Policy for parallel SAT solvers. + + - Can work independently in sequential or with many cores + +Version 3.0 (2013) + - Add incremental features. + See SAT13 paper: Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction + + - Add certified UNSAT proof. + +Version 2.3 (2012) + - Add new restart strategy + See CP12 paper: Refining Restarts Strategies For SAT and UNSAT + + - Add additionnal features to speed the search + +Version 2.0 (2011) + - Add additionnal features (freeze potential good clauses for one turn) + + - Based on Minisat 2.2 + +Version 1.0 (2009) + - Based on Minisat 2.0 + First release of glucose. + See ijcai 2009 paper: Predicting Learnt Clauses Quality in Modern SAT Solver \ No newline at end of file diff --git a/README.md b/README.md index 77c5e83..89434b3 100644 --- a/README.md +++ b/README.md @@ -1,13 +1,33 @@ # Glucose SAT solver -This is the release 3.0 of the glucose SAT solver. +This is the release 4.0 of the glucose SAT solver. It is based on [Minisat 2.2](http://minisat.se/MiniSat.html) -For compiling: - - ```cd simp``` -- ```make``` +**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. +Very good performances on industrial (non crypto) problems. -For running: ```simp/glucose BENCHNAME``` +**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: + Glucose sequential (with/without Satelite, decided by command line arguments) + Glucose sequential, incremental mode + Glucose sequential, certified unsat proof logging + Glucose parallel with satelite ( not yet a parallel certified unsat / parallel incremental) + +Choose your directory (simp or parallel) and type ‘make’. + +## 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. + - "_Glucose: a solver that predicts learnt clauses quality_". Gilles Audemard, Laurent Simon, SAT Competition, 2009. + - "_Refining restarts strategies for SAT and UNSAT formulae_". Gilles Audemard and Laurent Simon, in Proceedings of the 22nd International Conference on Principles and Practice of Constraint Programming (CP-12), 2012. + - "_GLUCOSE 2.1: Aggressive – but Reactive – Clause Database Management, Dynamic Restarts_". In Pragmatics of SAT (Workshop of SAT'12), Gilles Audemard and Laurent Simon, Juin 2012. + - "_Improving Glucose for Incremental SAT Solving with Assumption: Application to MUS Extraction_". Gilles Audemard, Jean-Marie Lagniez, Laurent Simon, in Proceedings of SAT 2013, 2013. + - "_Lazy Clause Exchange Policy for parallel SAT solvers_". Gilles Audemard, Laurent Simon, in 17th International Conference on Theory and Applications of Satisfiability Testing (SAT'14), 2014. + - "_Glucose in the SAT 2014 Competition_". G Audemard, L Simon, SAT Competition, 2014. diff --git a/core/BoundedQueue.h b/core/BoundedQueue.h index b17354f..5269c9b 100644 --- a/core/BoundedQueue.h +++ b/core/BoundedQueue.h @@ -1,23 +1,51 @@ -/***********************************************************************************[BoundedQueue.h] - Glucose -- Copyright (c) 2009, Gilles Audemard, Laurent Simon - CRIL - Univ. Artois, France - LRI - Univ. Paris Sud, France - +/***************************************************************************************[BoundedQueue.h] + Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + LRI - Univ. Paris Sud, France (2009-2013) + Labri - Univ. Bordeaux, France + + Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + 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 +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 +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 +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). + + +--------------- Original Minisat Copyrights + +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. -**************************************************************************************************/ + **************************************************************************************************/ #ifndef BoundedQueue_h @@ -102,7 +130,17 @@ class bqueue { void clear(bool dealloc = false) { elems.clear(dealloc); first = 0; maxsize=0; queuesize=0;sumofqueue=0;} - + void copyTo(bqueue &dest) const { + dest.last = last; + dest.sumofqueue = sumofqueue; + dest.maxsize = maxsize; + dest.queuesize = queuesize; + dest.expComputed = expComputed; + dest.exp = exp; + dest.value = value; + dest.first = first; + elems.copyTo(dest.elems); + } }; } //================================================================================================= diff --git a/core/Constants.h b/core/Constants.h index 4cccad2..259f1b3 100644 --- a/core/Constants.h +++ b/core/Constants.h @@ -1,33 +1,59 @@ -/************************************************************************************[Constants.h] - Glucose -- Copyright (c) 2009, Gilles Audemard, Laurent Simon - CRIL - Univ. Artois, France - LRI - Univ. Paris Sud, France - +/***************************************************************************************[Constants.h] + Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + LRI - Univ. Paris Sud, France (2009-2013) + Labri - Univ. Bordeaux, France + + Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + 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 +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 +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 +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). + + +--------------- Original Minisat Copyrights + +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. -**************************************************************************************************/ + **************************************************************************************************/ #define DYNAMICNBLEVEL #define CONSTANTREMOVECLAUSE -#define UPDATEVARACTIVITY // Constants for clauses reductions #define RATIOREMOVECLAUSES 2 - // Constants for restarts #define LOWER_BOUND_FOR_BLOCKING_RESTART 10000 diff --git a/core/Makefile b/core/Makefile index 0a9f1f5..14c4e9c 100644 --- a/core/Makefile +++ b/core/Makefile @@ -1,4 +1,3 @@ -EXEC = glucose -DEPDIR = mtl utils -MROOT = $(PWD)/.. -include $(MROOT)/mtl/template.mk +PHONY: + @echo "** Careful ** Since 4.0 you have to use the simp or parallel directory only for typing make" + diff --git a/core/Solver.cc b/core/Solver.cc index e3c474a..8346438 100644 --- a/core/Solver.cc +++ b/core/Solver.cc @@ -1,12 +1,32 @@ /***************************************************************************************[Solver.cc] - Glucose -- Copyright (c) 2013, Gilles Audemard, Laurent Simon - CRIL - Univ. Artois, France - LRI - Univ. Paris Sud, France - + Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + LRI - Univ. Paris Sud, France (2009-2013) + Labri - Univ. Bordeaux, France + + Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + Labri - Univ. Bordeaux, 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). +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 +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 +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). + + +--------------- Original Minisat Copyrights Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson Copyright (c) 2007-2010, Niklas Sorensson @@ -25,14 +45,14 @@ NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPO 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 "utils/System.h" #include "mtl/Sort.h" #include "core/Solver.h" #include "core/Constants.h" -#include "utils/System.h" using namespace Glucose; @@ -43,127 +63,224 @@ static const char* _cat = "CORE"; static const char* _cr = "CORE -- RESTART"; static const char* _cred = "CORE -- REDUCE"; static const char* _cm = "CORE -- MINIMIZE"; -static const char* _certified = "CORE -- CERTIFIED UNSAT"; -static BoolOption opt_incremental (_cat,"incremental", "Use incremental SAT solving",false); -static DoubleOption opt_K (_cr, "K", "The constant used to force restart", 0.8, DoubleRange(0, false, 1, false)); -static DoubleOption opt_R (_cr, "R", "The constant used to block restart", 1.4, DoubleRange(1, false, 5, false)); -static IntOption opt_size_lbd_queue (_cr, "szLBDQueue", "The size of moving average for LBD (restarts)", 50, IntRange(10, INT32_MAX)); -static IntOption opt_size_trail_queue (_cr, "szTrailQueue", "The size of moving average for trail (block restarts)", 5000, IntRange(10, INT32_MAX)); +static DoubleOption opt_K(_cr, "K", "The constant used to force restart", 0.8, DoubleRange(0, false, 1, false)); +static DoubleOption opt_R(_cr, "R", "The constant used to block restart", 1.4, DoubleRange(1, false, 5, false)); +static IntOption opt_size_lbd_queue(_cr, "szLBDQueue", "The size of moving average for LBD (restarts)", 50, IntRange(10, INT32_MAX)); +static IntOption opt_size_trail_queue(_cr, "szTrailQueue", "The size of moving average for trail (block restarts)", 5000, IntRange(10, INT32_MAX)); -static IntOption opt_first_reduce_db (_cred, "firstReduceDB", "The number of conflicts before the first reduce DB", 2000, IntRange(0, INT32_MAX)); -static IntOption opt_inc_reduce_db (_cred, "incReduceDB", "Increment for reduce DB", 300, IntRange(0, INT32_MAX)); -static IntOption opt_spec_inc_reduce_db (_cred, "specialIncReduceDB", "Special increment for reduce DB", 1000, IntRange(0, INT32_MAX)); -static IntOption opt_lb_lbd_frozen_clause (_cred, "minLBDFrozenClause", "Protect clauses if their LBD decrease and is lower than (for one turn)", 30, IntRange(0, INT32_MAX)); +static IntOption opt_first_reduce_db(_cred, "firstReduceDB", "The number of conflicts before the first reduce DB", 2000, IntRange(0, INT32_MAX)); +static IntOption opt_inc_reduce_db(_cred, "incReduceDB", "Increment for reduce DB", 300, IntRange(0, INT32_MAX)); +static IntOption opt_spec_inc_reduce_db(_cred, "specialIncReduceDB", "Special increment for reduce DB", 1000, IntRange(0, INT32_MAX)); +static IntOption opt_lb_lbd_frozen_clause(_cred, "minLBDFrozenClause", "Protect clauses if their LBD decrease and is lower than (for one turn)", 30, IntRange(0, INT32_MAX)); -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 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 DoubleOption opt_var_decay (_cat, "var-decay", "The variable activity decay factor", 0.8, DoubleRange(0, false, 1, false)); -static DoubleOption opt_clause_decay (_cat, "cla-decay", "The clause activity decay factor", 0.999, DoubleRange(0, false, 1, false)); -static DoubleOption opt_random_var_freq (_cat, "rnd-freq", "The frequency with which the decision heuristic tries to choose a random variable", 0, DoubleRange(0, true, 1, true)); -static DoubleOption opt_random_seed (_cat, "rnd-seed", "Used by the random variable selection", 91648253, DoubleRange(0, false, HUGE_VAL, false)); -static IntOption opt_ccmin_mode (_cat, "ccmin-mode", "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 2, IntRange(0, 2)); -static IntOption opt_phase_saving (_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2)); -static BoolOption opt_rnd_init_act (_cat, "rnd-init", "Randomize the initial activity", false); -/* -static IntOption opt_restart_first (_cat, "rfirst", "The base restart interval", 100, IntRange(1, INT32_MAX)); -static DoubleOption opt_restart_inc (_cat, "rinc", "Restart interval increase factor", 2, DoubleRange(1, false, HUGE_VAL, false)); -*/ -static DoubleOption opt_garbage_frac (_cat, "gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered", 0.20, DoubleRange(0, false, HUGE_VAL, false)); - - - BoolOption opt_certified (_certified, "certified", "Certified UNSAT using DRUP format", false); - StringOption opt_certified_file (_certified, "certified-output", "Certified UNSAT output file", "NULL"); +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)); +static DoubleOption opt_clause_decay(_cat, "cla-decay", "The clause activity decay factor", 0.999, DoubleRange(0, false, 1, false)); +static DoubleOption opt_random_var_freq(_cat, "rnd-freq", "The frequency with which the decision heuristic tries to choose a random variable", 0, DoubleRange(0, true, 1, true)); +static DoubleOption opt_random_seed(_cat, "rnd-seed", "Used by the random variable selection", 91648253, DoubleRange(0, false, HUGE_VAL, false)); +static IntOption opt_ccmin_mode(_cat, "ccmin-mode", "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 2, IntRange(0, 2)); +static IntOption opt_phase_saving(_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2)); +static BoolOption opt_rnd_init_act(_cat, "rnd-init", "Randomize the initial activity", false); +static DoubleOption opt_garbage_frac(_cat, "gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered", 0.20, DoubleRange(0, false, HUGE_VAL, false)); //================================================================================================= // Constructor/Destructor: - Solver::Solver() : - // Parameters (user settable): - // - verbosity (0) - , showModel (0) - , K (opt_K) - , R (opt_R) - , sizeLBDQueue (opt_size_lbd_queue) - , sizeTrailQueue (opt_size_trail_queue) - , firstReduceDB (opt_first_reduce_db) - , incReduceDB (opt_inc_reduce_db) - , specialIncReduceDB (opt_spec_inc_reduce_db) - , lbLBDFrozenClause (opt_lb_lbd_frozen_clause) - , lbSizeMinimizingClause (opt_lb_size_minimzing_clause) - , lbLBDMinimizingClause (opt_lb_lbd_minimzing_clause) - , var_decay (opt_var_decay) - , clause_decay (opt_clause_decay) - , random_var_freq (opt_random_var_freq) - , random_seed (opt_random_seed) - , ccmin_mode (opt_ccmin_mode) - , phase_saving (opt_phase_saving) - , rnd_pol (false) - , rnd_init_act (opt_rnd_init_act) - , garbage_frac (opt_garbage_frac) - , certifiedOutput (NULL) - , certifiedUNSAT (opt_certified) - // Statistics: (formerly in 'SolverStats') - // - , nbRemovedClauses(0),nbReducedClauses(0), nbDL2(0),nbBin(0),nbUn(0) , nbReduceDB(0) - , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0),conflicts(0),conflictsRestarts(0),nbstopsrestarts(0),nbstopsrestartssame(0),lastblockatrestart(0) - , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) - , curRestart(1) - - , ok (true) - , cla_inc (1) - , var_inc (1) - , watches (WatcherDeleted(ca)) - , watchesBin (WatcherDeleted(ca)) - , qhead (0) - , simpDB_assigns (-1) - , simpDB_props (0) - , order_heap (VarOrderLt(activity)) - , progress_estimate (0) - , remove_satisfied (true) - - // Resource constraints: - // - , conflict_budget (-1) - , propagation_budget (-1) - , asynch_interrupt (false) - , incremental(opt_incremental) - , nbVarsInitialFormula(INT32_MAX) +// Parameters (user settable): +// +verbosity(0) +, showModel(0) +, K(opt_K) +, R(opt_R) +, sizeLBDQueue(opt_size_lbd_queue) +, sizeTrailQueue(opt_size_trail_queue) +, firstReduceDB(opt_first_reduce_db) +, incReduceDB(opt_inc_reduce_db) +, specialIncReduceDB(opt_spec_inc_reduce_db) +, lbLBDFrozenClause(opt_lb_lbd_frozen_clause) +, lbSizeMinimizingClause(opt_lb_size_minimzing_clause) +, lbLBDMinimizingClause(opt_lb_lbd_minimzing_clause) +, var_decay(opt_var_decay) +, max_var_decay(opt_max_var_decay) +, clause_decay(opt_clause_decay) +, random_var_freq(opt_random_var_freq) +, random_seed(opt_random_seed) +, ccmin_mode(opt_ccmin_mode) +, phase_saving(opt_phase_saving) +, rnd_pol(false) +, rnd_init_act(opt_rnd_init_act) +, garbage_frac(opt_garbage_frac) +, certifiedOutput(NULL) +, certifiedUNSAT(false) // Not in the first parallel version +, panicModeLastRemoved(0), panicModeLastRemovedShared(0) +, useUnaryWatched(false) +, promoteOneWatchedClause(true) +// Statistics: (formerly in 'SolverStats') +// +, nbPromoted(0) +, originalClausesSeen(0) +, sumDecisionLevels(0) +, nbRemovedClauses(0), nbRemovedUnaryWatchedClauses(0), nbReducedClauses(0), nbDL2(0), nbBin(0), nbUn(0), nbReduceDB(0) +, solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0), conflictsRestarts(0) +, nbstopsrestarts(0), nbstopsrestartssame(0), lastblockatrestart(0) +, dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) +, curRestart(1) + +, ok(true) +, cla_inc(1) +, var_inc(1) +, watches(WatcherDeleted(ca)) +, watchesBin(WatcherDeleted(ca)) +, unaryWatches(WatcherDeleted(ca)) +, qhead(0) +, simpDB_assigns(-1) +, simpDB_props(0) +, order_heap(VarOrderLt(activity)) +, progress_estimate(0) +, remove_satisfied(true) +, reduceOnSize(false) // +, reduceOnSizeSize(12) // Constant to use on size reductions +,lastLearntClause(CRef_Undef) +// Resource constraints: +// +, conflict_budget(-1) +, propagation_budget(-1) +, asynch_interrupt(false) +, incremental(false) +, nbVarsInitialFormula(INT32_MAX) +, totalTime4Sat(0.) +, totalTime4Unsat(0.) +, nbSatCalls(0) +, nbUnsatCalls(0) { - MYFLAG=0; - // Initialize only first time. Useful for incremental solving, useless otherwise - lbdQueue.initSize(sizeLBDQueue); - trailQueue.initSize(sizeTrailQueue); - sumLBD = 0; - nbclausesbeforereduce = firstReduceDB; - totalTime4Sat=0;totalTime4Unsat=0; - nbSatCalls=0;nbUnsatCalls=0; - - - if(certifiedUNSAT) { - if(!strcmp(opt_certified_file,"NULL")) { - certifiedOutput = fopen("/dev/stdout", "wb"); - } else { - certifiedOutput = fopen(opt_certified_file, "wb"); - } - // fprintf(certifiedOutput,"o proof DRUP\n"); - } + MYFLAG = 0; + // Initialize only first time. Useful for incremental solving (not in // version), useless otherwise + // Kept here for simplicity + lbdQueue.initSize(sizeLBDQueue); + trailQueue.initSize(sizeTrailQueue); + sumLBD = 0; + nbclausesbeforereduce = firstReduceDB; } - -Solver::~Solver() +//------------------------------------------------------- +// Special constructor used for cloning solvers +//------------------------------------------------------- + +Solver::Solver(const Solver &s) : + verbosity(s.verbosity) +, showModel(s.showModel) +, K(s.K) +, R(s.R) +, sizeLBDQueue(s.sizeLBDQueue) +, sizeTrailQueue(s.sizeTrailQueue) +, firstReduceDB(s.firstReduceDB) +, incReduceDB(s.incReduceDB) +, specialIncReduceDB(s.specialIncReduceDB) +, lbLBDFrozenClause(s.lbLBDFrozenClause) +, lbSizeMinimizingClause(s.lbSizeMinimizingClause) +, lbLBDMinimizingClause(s.lbLBDMinimizingClause) +, var_decay(s.var_decay) +, max_var_decay(s.max_var_decay) +, clause_decay(s.clause_decay) +, random_var_freq(s.random_var_freq) +, random_seed(s.random_seed) +, ccmin_mode(s.ccmin_mode) +, phase_saving(s.phase_saving) +, rnd_pol(s.rnd_pol) +, rnd_init_act(s.rnd_init_act) +, garbage_frac(s.garbage_frac) +, certifiedOutput(NULL) +, certifiedUNSAT(false) // Not in the first parallel version +, panicModeLastRemoved(s.panicModeLastRemoved), panicModeLastRemovedShared(s.panicModeLastRemovedShared) +, useUnaryWatched(s.useUnaryWatched) +, promoteOneWatchedClause(s.promoteOneWatchedClause) +// Statistics: (formerly in 'SolverStats') +// +, nbPromoted(s.nbPromoted) +, originalClausesSeen(s.originalClausesSeen) +, sumDecisionLevels(s.sumDecisionLevels) +, nbRemovedClauses(s.nbRemovedClauses), nbRemovedUnaryWatchedClauses(s.nbRemovedUnaryWatchedClauses) +, nbReducedClauses(s.nbReducedClauses), nbDL2(s.nbDL2), nbBin(s.nbBin), nbUn(s.nbUn), nbReduceDB(s.nbReduceDB) +, solves(s.solves), starts(s.starts), decisions(s.decisions), rnd_decisions(s.rnd_decisions) +, propagations(s.propagations), conflicts(s.conflicts), conflictsRestarts(s.conflictsRestarts) +, nbstopsrestarts(s.nbstopsrestarts), nbstopsrestartssame(s.nbstopsrestartssame) +, lastblockatrestart(s.lastblockatrestart) +, dec_vars(s.dec_vars), clauses_literals(s.clauses_literals) +, learnts_literals(s.learnts_literals), max_literals(s.max_literals), tot_literals(s.tot_literals) +, curRestart(s.curRestart) + +, ok(true) +, cla_inc(s.cla_inc) +, var_inc(s.var_inc) +, watches(WatcherDeleted(ca)) +, watchesBin(WatcherDeleted(ca)) +, unaryWatches(WatcherDeleted(ca)) +, qhead(s.qhead) +, simpDB_assigns(s.simpDB_assigns) +, simpDB_props(s.simpDB_props) +, order_heap(VarOrderLt(activity)) +, progress_estimate(s.progress_estimate) +, remove_satisfied(s.remove_satisfied) +, reduceOnSize(s.reduceOnSize) // +, reduceOnSizeSize(s.reduceOnSizeSize) // Constant to use on size reductions +,lastLearntClause(CRef_Undef) +// Resource constraints: +// +, conflict_budget(s.conflict_budget) +, propagation_budget(s.propagation_budget) +, asynch_interrupt(s.asynch_interrupt) +, incremental(s.incremental) +, nbVarsInitialFormula(s.nbVarsInitialFormula) +, totalTime4Sat(s.totalTime4Sat) +, totalTime4Unsat(s.totalTime4Unsat) +, nbSatCalls(s.nbSatCalls) +, nbUnsatCalls(s.nbUnsatCalls) { + // Copy clauses. + s.ca.copyTo(ca); + ca.extra_clause_field = s.ca.extra_clause_field; + + // Initialize other variables + MYFLAG = 0; + // Initialize only first time. Useful for incremental solving (not in // version), useless otherwise + // Kept here for simplicity + sumLBD = s.sumLBD; + nbclausesbeforereduce = s.nbclausesbeforereduce; + + // Copy all search vectors + s.watches.copyTo(watches); + s.watchesBin.copyTo(watchesBin); + s.unaryWatches.copyTo(unaryWatches); + s.assigns.memCopyTo(assigns); + s.vardata.memCopyTo(vardata); + s.activity.memCopyTo(activity); + s.seen.memCopyTo(seen); + s.permDiff.memCopyTo(permDiff); + s.polarity.memCopyTo(polarity); + s.decision.memCopyTo(decision); + s.trail.memCopyTo(trail); + s.order_heap.copyTo(order_heap); + s.clauses.memCopyTo(clauses); + s.learnts.memCopyTo(learnts); + + s.lbdQueue.copyTo(lbdQueue); + s.trailQueue.copyTo(trailQueue); + } +Solver::~Solver() { +} /**************************************************************** Set the incremental mode @@ -181,6 +298,10 @@ void Solver::initNbInitialVars(int nb) { nbVarsInitialFormula = nb; } +bool Solver::isIncremental() { + return incremental; +} + //================================================================================================= // Minor methods: @@ -189,72 +310,73 @@ void Solver::initNbInitialVars(int nb) { // Creates a new SAT variable in the solver. If 'decision' is cleared, variable will not be // used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result). // -Var Solver::newVar(bool sign, bool dvar) -{ + +Var Solver::newVar(bool sign, bool dvar) { int v = nVars(); - watches .init(mkLit(v, false)); - watches .init(mkLit(v, true )); - watchesBin .init(mkLit(v, false)); - watchesBin .init(mkLit(v, true )); - assigns .push(l_Undef); - vardata .push(mkVarData(CRef_Undef, 0)); - //activity .push(0); + watches .init(mkLit(v, false)); + watches .init(mkLit(v, true)); + watchesBin .init(mkLit(v, false)); + watchesBin .init(mkLit(v, true)); + unaryWatches .init(mkLit(v, false)); + unaryWatches .init(mkLit(v, true)); + assigns .push(l_Undef); + vardata .push(mkVarData(CRef_Undef, 0)); activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0); - seen .push(0); - permDiff .push(0); + seen .push(0); + permDiff .push(0); polarity .push(sign); decision .push(); - trail .capacity(v+1); + trail .capacity(v + 1); setDecisionVar(v, dvar); return v; } +bool Solver::addClause_(vec& ps) { - -bool Solver::addClause_(vec& ps) -{ assert(decisionLevel() == 0); if (!ok) return false; // Check if clause is satisfied and remove false/duplicate literals: sort(ps); - vec oc; + vec oc; oc.clear(); - Lit p; int i, j, flag = 0; - if(certifiedUNSAT) { - for (i = j = 0, p = lit_Undef; i < ps.size(); i++) { - oc.push(ps[i]); - if (value(ps[i]) == l_True || ps[i] == ~p || value(ps[i]) == l_False) - flag = 1; - } + Lit p; + int i, j, flag = 0; + if (certifiedUNSAT) { + for (i = j = 0, p = lit_Undef; i < ps.size(); i++) { + oc.push(ps[i]); + if (value(ps[i]) == l_True || ps[i] == ~p || value(ps[i]) == l_False) + flag = 1; + } } for (i = j = 0, p = lit_Undef; i < ps.size(); i++) - if (value(ps[i]) == l_True || ps[i] == ~p) - return true; - else if (value(ps[i]) != l_False && ps[i] != p) - ps[j++] = p = ps[i]; + if (value(ps[i]) == l_True || ps[i] == ~p) + return true; + else if (value(ps[i]) != l_False && ps[i] != p) + ps[j++] = p = ps[i]; ps.shrink(i - j); - + if (flag && (certifiedUNSAT)) { - 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"); + 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"); } + if (ps.size() == 0) return ok = false; - else if (ps.size() == 1){ + else if (ps.size() == 1) { uncheckedEnqueue(ps[0]); return ok = (propagate() == CRef_Undef); - }else{ + } else { CRef cr = ca.alloc(ps, false); clauses.push(cr); attachClause(cr); @@ -263,79 +385,99 @@ bool Solver::addClause_(vec& ps) return true; } - void Solver::attachClause(CRef cr) { const Clause& c = ca[cr]; assert(c.size() > 1); - if(c.size()==2) { - watchesBin[~c[0]].push(Watcher(cr, c[1])); - watchesBin[~c[1]].push(Watcher(cr, c[0])); + if (c.size() == 2) { + watchesBin[~c[0]].push(Watcher(cr, c[1])); + watchesBin[~c[1]].push(Watcher(cr, c[0])); } else { - watches[~c[0]].push(Watcher(cr, c[1])); - watches[~c[1]].push(Watcher(cr, c[0])); + watches[~c[0]].push(Watcher(cr, c[1])); + watches[~c[1]].push(Watcher(cr, c[0])); } if (c.learnt()) learnts_literals += c.size(); - else clauses_literals += c.size(); } + else clauses_literals += c.size(); +} +void Solver::attachClausePurgatory(CRef cr) { + const Clause& c = ca[cr]; + assert(c.size() > 1); + unaryWatches[~c[0]].push(Watcher(cr, c[1])); +} void Solver::detachClause(CRef cr, bool strict) { const Clause& c = ca[cr]; - + assert(c.size() > 1); - if(c.size()==2) { - if (strict){ - remove(watchesBin[~c[0]], Watcher(cr, c[1])); - remove(watchesBin[~c[1]], Watcher(cr, c[0])); - }else{ - // Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause) - watchesBin.smudge(~c[0]); - watchesBin.smudge(~c[1]); - } + if (c.size() == 2) { + if (strict) { + remove(watchesBin[~c[0]], Watcher(cr, c[1])); + remove(watchesBin[~c[1]], Watcher(cr, c[0])); + } else { + // Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause) + watchesBin.smudge(~c[0]); + watchesBin.smudge(~c[1]); + } } else { - if (strict){ - remove(watches[~c[0]], Watcher(cr, c[1])); - remove(watches[~c[1]], Watcher(cr, c[0])); - }else{ - // Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause) - watches.smudge(~c[0]); - watches.smudge(~c[1]); - } + if (strict) { + remove(watches[~c[0]], Watcher(cr, c[1])); + remove(watches[~c[1]], Watcher(cr, c[0])); + } else { + // Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause) + watches.smudge(~c[0]); + watches.smudge(~c[1]); + } } if (c.learnt()) learnts_literals -= c.size(); - else clauses_literals -= c.size(); } - + else clauses_literals -= c.size(); +} -void Solver::removeClause(CRef cr) { - Clause& c = ca[cr]; +// The purgatory is the 1-Watched scheme for imported clauses - if (certifiedUNSAT) { - 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"); - } +void Solver::detachClausePurgatory(CRef cr, bool strict) { + const Clause& c = ca[cr]; - detachClause(cr); - // Don't leave pointers to free'd memory! - if (locked(c)) vardata[var(c[0])].reason = CRef_Undef; - c.mark(1); - ca.free(cr); + assert(c.size() > 1); + if (strict) + remove(unaryWatches[~c[0]], Watcher(cr, c[1])); + else + unaryWatches.smudge(~c[0]); } +void Solver::removeClause(CRef cr, bool inPurgatory) { -bool Solver::satisfied(const Clause& c) const { - if(incremental) // Check clauses with many selectors is too time consuming - return (value(c[0]) == l_True) || (value(c[1]) == l_True); + Clause& c = ca[cr]; + + if (certifiedUNSAT) { + 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"); + } - // Default mode. + if (inPurgatory) + detachClausePurgatory(cr); + else + detachClause(cr); + // Don't leave pointers to free'd memory! + if (locked(c)) vardata[var(c[0])].reason = CRef_Undef; + c.mark(1); + ca.free(cr); +} + +bool Solver::satisfied(const Clause& c) const { + if(incremental) + return (value(c[0]) == l_True) || (value(c[1]) == l_True); + + // Default mode for (int i = 0; i < c.size(); i++) if (value(c[i]) == l_True) return true; - return false; + return false; } /************************************************************ @@ -348,7 +490,7 @@ inline unsigned int Solver::computeLBD(const vec & lits,int end) { if(incremental) { // ----------------- INCREMENTAL MODE if(end==-1) end = lits.size(); - unsigned int nbDone = 0; + int nbDone = 0; for(int i=0;i=end) break; if(isSelector(var(lits[i]))) continue; @@ -369,7 +511,10 @@ inline unsigned int Solver::computeLBD(const vec & lits,int end) { } } - return nblevels; + if (!reduceOnSize) + return nblevels; + if (lits.size() < reduceOnSizeSize) return lits.size(); // See the XMinisat paper + return lits.size() + nblevels; } inline unsigned int Solver::computeLBD(const Clause &c) { @@ -377,7 +522,7 @@ inline unsigned int Solver::computeLBD(const Clause &c) { MYFLAG++; if(incremental) { // ----------------- INCREMENTAL MODE - int nbDone = 0; + unsigned int nbDone = 0; for(int i=0;i=c.sizeWithoutSelectors()) break; if(isSelector(var(c[i]))) continue; @@ -397,96 +542,103 @@ inline unsigned int Solver::computeLBD(const Clause &c) { } } } - return nblevels; -} + + if (!reduceOnSize) + return nblevels; + if (c.size() < reduceOnSizeSize) return c.size(); // See the XMinisat paper + return c.size() + nblevels; +} /****************************************************************** * Minimisation with binary reolution ******************************************************************/ void Solver::minimisationWithBinaryResolution(vec &out_learnt) { - - // Find the LBD measure - unsigned int lbd = computeLBD(out_learnt); - Lit p = ~out_learnt[0]; - - if(lbd<=lbLBDMinimizingClause){ - MYFLAG++; - - for(int i = 1;i& wbin = watchesBin[p]; - int nb = 0; - for(int k = 0;k0) { - nbReducedClauses++; - for(int i = 1;i& wbin = watchesBin[p]; + int nb = 0; + for (int k = 0; k < wbin.size(); k++) { + Lit imp = wbin[k].blocker; + if (permDiff[var(imp)] == MYFLAG && value(imp) == l_True) { + nb++; + permDiff[var(imp)] = MYFLAG - 1; + } + } + int l = out_learnt.size() - 1; + if (nb > 0) { + nbReducedClauses++; + for (int i = 1; i < out_learnt.size() - nb; i++) { + if (permDiff[var(out_learnt[i])] != MYFLAG) { + Lit p = out_learnt[l]; + out_learnt[l] = out_learnt[i]; + out_learnt[i] = p; + l--; + i--; + } + } + + out_learnt.shrink(nb); + + } } - } } // Revert to the state at given level (keeping all assignment at 'level' but not beyond). // + void Solver::cancelUntil(int level) { - if (decisionLevel() > level){ - for (int c = trail.size()-1; c >= trail_lim[level]; c--){ - Var x = var(trail[c]); + if (decisionLevel() > level) { + for (int c = trail.size() - 1; c >= trail_lim[level]; c--) { + Var x = var(trail[c]); assigns [x] = l_Undef; - if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last())) + if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last())) { polarity[x] = sign(trail[c]); - insertVarOrder(x); } + } + insertVarOrder(x); + } qhead = trail_lim[level]; trail.shrink(trail.size() - trail_lim[level]); trail_lim.shrink(trail_lim.size() - level); - } + } } //================================================================================================= // Major methods: - -Lit Solver::pickBranchLit() -{ +Lit Solver::pickBranchLit() { Var next = var_Undef; // Random decision: - if (drand(random_seed) < random_var_freq && !order_heap.empty()){ - next = order_heap[irand(random_seed,order_heap.size())]; + if (drand(random_seed) < random_var_freq && !order_heap.empty()) { + next = order_heap[irand(random_seed, order_heap.size())]; if (value(next) == l_Undef && decision[next]) - rnd_decisions++; } + rnd_decisions++; + } // Activity based decision: while (next == var_Undef || value(next) != l_Undef || !decision[next]) - if (order_heap.empty()){ + if (order_heap.empty()) { next = var_Undef; break; - }else + } else { next = order_heap.removeMin(); + } return next == var_Undef ? lit_Undef : mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : polarity[next]); } - /*_________________________________________________________________________________________________ | | analyze : (confl : Clause*) (out_learnt : vec&) (out_btlevel : int&) -> [void] @@ -504,91 +656,94 @@ Lit Solver::pickBranchLit() | 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) -{ +void Solver::analyze(CRef confl, vec& out_learnt,vec&selectors, int& out_btlevel,unsigned int &lbd,unsigned int &szWithoutSelectors) { int pathC = 0; - Lit p = lit_Undef; + Lit p = lit_Undef; + // Generate conflict clause: // - out_learnt.push(); // (leave room for the asserting literal) - int index = trail.size() - 1; - - do{ + out_learnt.push(); // (leave room for the asserting literal) + int index = trail.size() - 1; + do { assert(confl != CRef_Undef); // (otherwise should be UIP) 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; + } - // 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 (c.learnt()) + if (c.learnt()) { + parallelImportClauseDuringConflictAnalysis(c,confl); claBumpActivity(c); + } else { // original clause + if (!c.getSeen()) { + originalClausesSeen++; + c.setSeen(true); + } + } -#ifdef DYNAMICNBLEVEL - // DYNAMIC NBLEVEL trick (see competition'09 companion paper) - if(c.learnt() && c.lbd()>2) { - unsigned int nblevels = computeLBD(c); - if(nblevels+1 2) { + unsigned int nblevels = computeLBD(c); + if (nblevels + 1 < c.lbd()) { // improve the LBD + if (c.lbd() <= lbLBDFrozenClause) { + c.setCanBeDel(false); + } + // seems to be interesting : keep it for the next round + c.setLBD(nblevels); // Update it + } + } - for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){ + for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++) { Lit q = c[j]; - if (!seen[var(q)] && level(var(q)) > 0){ - if(!isSelector(var(q))) - varBumpActivity(var(q)); - seen[var(q)] = 1; - if (level(var(q)) >= decisionLevel()) { - pathC++; -#ifdef UPDATEVARACTIVITY - // UPDATEVARACTIVITY trick (see competition'09 companion paper) - if(!isSelector(var(q)) && (reason(var(q))!= CRef_Undef) && ca[reason(var(q))].learnt()) - lastDecisionLevel.push(q); -#endif - - } else { - if(isSelector(var(q))) { - assert(value(q) == l_False); - selectors.push(q); - } else - out_learnt.push(q); - } - } + if (!seen[var(q)]) { + if (level(var(q)) == 0) { + } else { // Here, the old case + if(!isSelector(var(q))) + varBumpActivity(var(q)); + seen[var(q)] = 1; + if (level(var(q)) >= decisionLevel()) { + pathC++; + // UPDATEVARACTIVITY trick (see competition'09 companion paper) + if (!isSelector(var(q)) && (reason(var(q)) != CRef_Undef) && ca[reason(var(q))].learnt()) + lastDecisionLevel.push(q); + } else { + if(isSelector(var(q))) { + assert(value(q) == l_False); + selectors.push(q); + } else + out_learnt.push(q); + } + } + } } - + // Select next clause to look at: while (!seen[var(trail[index--])]); - p = trail[index+1]; + p = trail[index + 1]; confl = reason(var(p)); seen[var(p)] = 0; pathC--; - }while (pathC > 0); + } while (pathC > 0); out_learnt[0] = ~p; // Simplify conflict clause: // int i, j; - for(int i = 0;i& out_learnt,vec&selectors, int& o for (i = j = 1; i < out_learnt.size(); i++) if (reason(var(out_learnt[i])) == CRef_Undef || !litRedundant(out_learnt[i], abstract_level)) out_learnt[j++] = out_learnt[i]; - - }else if (ccmin_mode == 1){ - for (i = j = 1; i < out_learnt.size(); i++){ + + } else if (ccmin_mode == 1) { + for (i = j = 1; i < out_learnt.size(); i++) { Var x = var(out_learnt[i]); if (reason(x) == CRef_Undef) out_learnt[j++] = out_learnt[i]; - else{ + else { Clause& c = ca[reason(var(out_learnt[i]))]; // Thanks to Siert Wieringa for this bug fix! - for (int k = ((c.size()==2) ? 0:1); k < c.size(); k++) - if (!seen[var(c[k])] && level(var(c[k])) > 0){ + for (int k = ((c.size() == 2) ? 0 : 1); k < c.size(); k++) + if (!seen[var(c[k])] && level(var(c[k])) > 0) { out_learnt[j++] = out_learnt[i]; - break; } + break; + } } } - }else + } else i = j = out_learnt.size(); max_literals += out_learnt.size(); @@ -626,29 +782,26 @@ void Solver::analyze(CRef confl, vec& out_learnt,vec&selectors, int& o Then, we reduce clauses with small LBD. Otherwise, this can be useless */ - if(!incremental && out_learnt.size()<=lbSizeMinimizingClause) { - minimisationWithBinaryResolution(out_learnt); + if (!incremental && out_learnt.size() <= lbSizeMinimizingClause) { + minimisationWithBinaryResolution(out_learnt); } // Find correct backtrack level: // if (out_learnt.size() == 1) out_btlevel = 0; - else{ + else { int max_i = 1; // Find the first literal assigned at the next-highest level: for (int i = 2; i < out_learnt.size(); i++) if (level(var(out_learnt[i])) > level(var(out_learnt[max_i]))) max_i = i; // Swap-in this literal at index 1: - Lit p = out_learnt[max_i]; + Lit p = out_learnt[max_i]; out_learnt[max_i] = out_learnt[1]; - out_learnt[1] = p; - out_btlevel = level(var(p)); + out_learnt[1] = p; + out_btlevel = level(var(p)); } - - - // Compute the size of the clause without selectors (incremental mode) - if(incremental) { + if(incremental) { szWithoutSelectors = 0; for(int i=0;i& out_learnt,vec&selectors, int& o // Compute LBD lbd = computeLBD(out_learnt,out_learnt.size()-selectors.size()); - - -#ifdef UPDATEVARACTIVITY - // UPDATEVARACTIVITY trick (see competition'09 companion paper) - if(lastDecisionLevel.size()>0) { - for(int i = 0;i 0) { + for (int i = 0; i < lastDecisionLevel.size(); i++) { + if (ca[reason(var(lastDecisionLevel[i]))].lbd() < lbd) + varBumpActivity(var(lastDecisionLevel[i])); + } + lastDecisionLevel.clear(); } - lastDecisionLevel.clear(); - } -#endif - for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared) - for(int j = 0 ; j 0){ + while (analyze_stack.size() > 0) { assert(reason(var(analyze_stack.last())) != CRef_Undef); - Clause& c = ca[reason(var(analyze_stack.last()))]; analyze_stack.pop(); - if(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; - } - - for (int i = 1; i < c.size(); i++){ - Lit p = c[i]; - if (!seen[var(p)] && level(var(p)) > 0){ - if (reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0){ - seen[var(p)] = 1; - analyze_stack.push(p); - analyze_toclear.push(p); - }else{ - for (int j = top; j < analyze_toclear.size(); j++) - seen[var(analyze_toclear[j])] = 0; - analyze_toclear.shrink(analyze_toclear.size() - top); - return false; + Clause& c = ca[reason(var(analyze_stack.last()))]; + analyze_stack.pop(); // + if (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; + } + + for (int i = 1; i < c.size(); i++) { + Lit p = c[i]; + if (!seen[var(p)]) { + if (level(var(p)) > 0) { + if (reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0) { + seen[var(p)] = 1; + analyze_stack.push(p); + analyze_toclear.push(p); + } else { + for (int j = top; j < analyze_toclear.size(); j++) + seen[var(analyze_toclear[j])] = 0; + analyze_toclear.shrink(analyze_toclear.size() - top); + return false; + } } } } @@ -724,8 +878,7 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels) | Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and | stores the result in 'out_conflict'. |________________________________________________________________________________________________@*/ -void Solver::analyzeFinal(Lit p, vec& out_conflict) -{ +void Solver::analyzeFinal(Lit p, vec& out_conflict) { out_conflict.clear(); out_conflict.push(p); @@ -734,21 +887,21 @@ void Solver::analyzeFinal(Lit p, vec& out_conflict) seen[var(p)] = 1; - for (int i = trail.size()-1; i >= trail_lim[0]; i--){ + for (int i = trail.size() - 1; i >= trail_lim[0]; i--) { Var x = var(trail[i]); - if (seen[x]){ - if (reason(x) == CRef_Undef){ + if (seen[x]) { + if (reason(x) == CRef_Undef) { assert(level(x) > 0); out_conflict.push(~trail[i]); - }else{ + } else { Clause& c = ca[reason(x)]; - // for (int j = 1; j < c.size(); j++) Minisat (glucose 2.0) loop - // Bug in case of assumptions due to special data structures for Binary. - // Many thanks to Sam Bayless (sbayless@cs.ubc.ca) for discover this bug. - for (int j = ((c.size()==2) ? 0:1); j < c.size(); j++) + // for (int j = 1; j < c.size(); j++) Minisat (glucose 2.0) loop + // Bug in case of assumptions due to special data structures for Binary. + // Many thanks to Sam Bayless (sbayless@cs.ubc.ca) for discover this bug. + for (int j = ((c.size() == 2) ? 0 : 1); j < c.size(); j++) if (level(var(c[j])) > 0) seen[var(c[j])] = 1; - } + } seen[x] = 0; } @@ -757,16 +910,13 @@ void Solver::analyzeFinal(Lit p, vec& out_conflict) seen[var(p)] = 0; } - -void Solver::uncheckedEnqueue(Lit p, CRef from) -{ +void Solver::uncheckedEnqueue(Lit p, CRef from) { assert(value(p) == l_Undef); assigns[var(p)] = lbool(!sign(p)); vardata[var(p)] = mkVarData(from, decisionLevel()); trail.push_(p); } - /*_________________________________________________________________________________________________ | | propagate : [void] -> [Clause*] @@ -778,60 +928,63 @@ void Solver::uncheckedEnqueue(Lit p, CRef from) | Post-conditions: | * the propagation queue is empty, even if there was a conflict. |________________________________________________________________________________________________@*/ -CRef Solver::propagate() -{ - CRef confl = CRef_Undef; - int num_props = 0; +CRef Solver::propagate() { + CRef confl = CRef_Undef; + int num_props = 0; + int previousqhead = qhead; 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; + unaryWatches.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;k& wbin = watchesBin[p]; + + for (int k = 0; k < wbin.size(); k++) { - for (i = j = (Watcher*)ws, end = i + ws.size(); i != end;){ + Lit imp = wbin[k].blocker; + + if (value(imp) == l_False) { + return wbin[k].cref; + } + + if (value(imp) == l_Undef) { + uncheckedEnqueue(imp, wbin[k].cref); + } + } + + // Now propagate other 2-watched clauses + 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; } + 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; + CRef cr = i->cref; + Clause& c = ca[cr]; + assert(!c.getOneWatched()); + 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. - Lit first = c[0]; - Watcher w = Watcher(cr, first); - if (first != blocker && value(first) == l_True){ - - *j++ = w; continue; } + Lit first = c[0]; + Watcher w = Watcher(cr, first); + if (first != blocker && value(first) == l_True) { - // Look for new watch: + *j++ = w; + continue; + } if(incremental) { // ----------------- INCREMENTAL MODE int choosenPos = -1; for (int k = 2; k < c.size(); k++) { @@ -863,30 +1016,125 @@ CRef Solver::propagate() goto NextClause; } } } - + // Did not find watch -- clause is unit under assignment: *j++ = w; - if (value(first) == l_False){ + if (value(first) == l_False) { confl = cr; qhead = trail.size(); // Copy the remaining watches: while (i < end) *j++ = *i++; - }else { + } else { uncheckedEnqueue(first, cr); - - - } - NextClause:; + + + } +NextClause: + ; } ws.shrink(i - j); + + // unaryWatches "propagation" + if (useUnaryWatched && confl == CRef_Undef) { + confl = propagateUnaryWatches(p); + + } + } + + + propagations += num_props; simpDB_props -= num_props; - + return confl; } +/*_________________________________________________________________________________________________ +| +| propagateUnaryWatches : [Lit] -> [Clause*] +| +| Description: +| Propagates unary watches of Lit p, return a conflict +| otherwise CRef_Undef +| +|________________________________________________________________________________________________@*/ + +CRef Solver::propagateUnaryWatches(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++; + + // We can add it now to the set of clauses when backtracking + //printf("*"); + if (promoteOneWatchedClause) { + nbPromoted++; + // Let's find the two biggest decision levels in the clause s.t. it will correctly be propagated when we'll backtrack + int maxlevel = -1; + int index = -1; + for (int k = 1; k < c.size(); k++) { + assert(value(c[k]) == l_False); + assert(level(var(c[k])) <= level(var(c[0]))); + if (level(var(c[k])) > maxlevel) { + index = k; + maxlevel = level(var(c[k])); + } + } + detachClausePurgatory(cr, true); // TODO: check that the cleanAll is ok (use ",true" otherwise) + assert(index != -1); + Lit tmp = c[1]; + c[1] = c[index], c[index] = tmp; + attachClause(cr); + // TODO used in function ParallelSolver::reportProgressArrayImports + //Override :-( + //goodImportsFromThreads[ca[cr].importedFrom()]++; + ca[cr].setOneWatched(false); + ca[cr].setExported(2); + } +NextClauseUnary: + ; + } + ws.shrink(i - j); + + return confl; +} /*_________________________________________________________________________________________________ | @@ -896,29 +1144,7 @@ CRef Solver::propagate() | 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. |________________________________________________________________________________________________@*/ -struct reduceDB_lt { - ClauseAllocator& ca; - reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {} - bool operator () (CRef x, CRef y) { - - // Main criteria... Like in MiniSat we keep all binary clauses - if(ca[x].size()> 2 && ca[y].size()==2) return 1; - - if(ca[y].size()>2 && ca[x].size()==2) return 0; - if(ca[x].size()==2 && ca[y].size()==2) return 0; - - // Second one based on literal block distance - if(ca[x].lbd()> ca[y].lbd()) return 1; - if(ca[x].lbd()< ca[y].lbd()) return 0; - - - // Finally we can use old activity or size, we choose the last one - 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()); } - } -}; void Solver::reduceDB() { @@ -955,32 +1181,32 @@ void Solver::reduceDB() } -void Solver::removeSatisfied(vec& cs) -{ - +void Solver::removeSatisfied(vec& cs) { + int i, j; - for (i = j = 0; i < cs.size(); i++){ + for (i = j = 0; i < cs.size(); i++) { Clause& c = ca[cs[i]]; - if (satisfied(c)) - removeClause(cs[i]); + if (satisfied(c)) + if (c.getOneWatched()) + removeClause(cs[i], true); + else + removeClause(cs[i]); else cs[j++] = cs[i]; } cs.shrink(i - j); } - -void Solver::rebuildOrderHeap() -{ +void Solver::rebuildOrderHeap() { vec vs; for (Var v = 0; v < nVars(); v++) if (decision[v] && value(v) == l_Undef) vs.push(v); order_heap.build(vs); -} +} /*_________________________________________________________________________________________________ | @@ -990,25 +1216,31 @@ void Solver::rebuildOrderHeap() | 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. |________________________________________________________________________________________________@*/ -bool Solver::simplify() -{ +bool Solver::simplify() { assert(decisionLevel() == 0); - if (!ok || propagate() != CRef_Undef) - return ok = false; + if (!ok) return ok = false; + else { + CRef cr = propagate(); + if (cr != CRef_Undef) { + return ok = false; + } + } + if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) return true; // Remove satisfied clauses: removeSatisfied(learnts); - if (remove_satisfied) // Can be turned off. + removeSatisfied(unaryWatchedClauses); + if (remove_satisfied) // Can be turned off. removeSatisfied(clauses); checkGarbage(); rebuildOrderHeap(); simpDB_assigns = nAssigns(); - simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but it will do for now) + simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but it will do for now) return true; } @@ -1027,131 +1259,156 @@ bool Solver::simplify() | all variables are decision variables, this means that the clause set is satisfiable. 'l_False' | if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached. |________________________________________________________________________________________________@*/ -lbool Solver::search(int nof_conflicts) -{ +lbool Solver::search(int nof_conflicts) { assert(ok); - int backtrack_level; - int conflictC = 0; - vec learnt_clause,selectors; - unsigned int nblevels,szWoutSelectors; - bool blocked=false; + int backtrack_level; + int conflictC = 0; + vec learnt_clause, selectors; + unsigned int nblevels,szWithoutSelectors = 0; + bool blocked = false; starts++; - for (;;){ + for (;;) { + if (decisionLevel() == 0) { // We import clauses FIXME: ensure that we will import clauses enventually (restart after some point) + parallelImportUnaryClauses(); + + if (parallelImportClauses()) + return l_False; + + } CRef confl = propagate(); - if (confl != CRef_Undef){ + + if (confl != CRef_Undef) { + if(parallelJobIsFinished()) + return l_Undef; + + + sumDecisionLevels += decisionLevel(); // CONFLICT - conflicts++; conflictC++;conflictsRestarts++; - if(conflicts%5000==0 && var_decay<0.95) - var_decay += 0.01; - - if (verbosity >= 1 && conflicts%verbEveryConflicts==0){ - printf("c | %8d %7d %5d | %7d %8d %8d | %5d %8d %6d %8d | %6.3f %% |\n", - (int)starts,(int)nbstopsrestarts, (int)(conflicts/starts), - (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals, - (int)nbReduceDB, nLearnts(), (int)nbDL2,(int)nbRemovedClauses, progressEstimate()*100); - } - if (decisionLevel() == 0) { - return l_False; - - } - - trailQueue.push(trail.size()); - // BLOCK RESTART (CP 2012 paper) - if( conflictsRestarts>LOWER_BOUND_FOR_BLOCKING_RESTART && lbdQueue.isvalid() && trail.size()>R*trailQueue.getavg()) { - lbdQueue.fastclear(); - nbstopsrestarts++; - if(!blocked) {lastblockatrestart=starts;nbstopsrestartssame++;blocked=true;} - } + conflicts++; + conflictC++; + conflictsRestarts++; + if (conflicts % 5000 == 0 && var_decay < max_var_decay) + var_decay += 0.01; + + if (verbosity >= 1 && conflicts % verbEveryConflicts == 0) { + printf("c | %8d %7d %5d | %7d %8d %8d | %5d %8d %6d %8d | %6.3f %% |\n", + (int) starts, (int) nbstopsrestarts, (int) (conflicts / starts), + (int) dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int) clauses_literals, + (int) nbReduceDB, nLearnts(), (int) nbDL2, (int) nbRemovedClauses, progressEstimate()*100); + } + if (decisionLevel() == 0) { + return l_False; + + } + + trailQueue.push(trail.size()); + // BLOCK RESTART (CP 2012 paper) + if (conflictsRestarts > LOWER_BOUND_FOR_BLOCKING_RESTART && lbdQueue.isvalid() && trail.size() > R * trailQueue.getavg()) { + lbdQueue.fastclear(); + nbstopsrestarts++; + if (!blocked) { + lastblockatrestart = starts; + nbstopsrestartssame++; + blocked = true; + } + } learnt_clause.clear(); - selectors.clear(); - analyze(confl, learnt_clause, selectors,backtrack_level,nblevels,szWoutSelectors); + selectors.clear(); - lbdQueue.push(nblevels); - sumLBD += nblevels; - + analyze(confl, learnt_clause, selectors, backtrack_level, nblevels,szWithoutSelectors); + + lbdQueue.push(nblevels); + sumLBD += nblevels; cancelUntil(backtrack_level); if (certifiedUNSAT) { - 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"); + 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 (learnt_clause.size() == 1){ - uncheckedEnqueue(learnt_clause[0]);nbUn++; - }else{ + + if (learnt_clause.size() == 1) { + uncheckedEnqueue(learnt_clause[0]); + nbUn++; + parallelExportUnaryClause(learnt_clause[0]); + } else { CRef cr = ca.alloc(learnt_clause, true); - ca[cr].setLBD(nblevels); - ca[cr].setSizeWithoutSelectors(szWoutSelectors); - if(nblevels<=2) nbDL2++; // stats - if(ca[cr].size()==2) nbBin++; // stats + ca[cr].setLBD(nblevels); + ca[cr].setOneWatched(false); + ca[cr].setSizeWithoutSelectors(szWithoutSelectors); + if (nblevels <= 2) nbDL2++; // stats + if (ca[cr].size() == 2) nbBin++; // stats learnts.push(cr); attachClause(cr); - + lastLearntClause = cr; // Use in multithread (to hard to put inside ParallelSolver) + parallelExportClauseDuringSearch(ca[cr]); claBumpActivity(ca[cr]); uncheckedEnqueue(learnt_clause[0], cr); + } varDecayActivity(); claDecayActivity(); - - }else{ - // Our dynamic restart, see the SAT09 competition compagnion paper - if ( - ( lbdQueue.isvalid() && ((lbdQueue.getavg()*K) > (sumLBD / conflictsRestarts)))) { - lbdQueue.fastclear(); - progress_estimate = progressEstimate(); - int bt = 0; - if(incremental) { // DO NOT BACKTRACK UNTIL 0.. USELESS - bt = (decisionLevel()=curRestart* nbclausesbeforereduce) - { - - assert(learnts.size()>0); - curRestart = (conflicts/ nbclausesbeforereduce)+1; - reduceDB(); - nbclausesbeforereduce += incReduceDB; - } - + + } else { + // Our dynamic restart, see the SAT09 competition compagnion paper + if ( + (lbdQueue.isvalid() && ((lbdQueue.getavg() * K) > (sumLBD / conflictsRestarts)))) { + lbdQueue.fastclear(); + progress_estimate = progressEstimate(); + int bt = 0; + if(incremental) // DO NOT BACKTRACK UNTIL 0.. USELESS + bt = (decisionLevel()= ((unsigned int) curRestart * nbclausesbeforereduce)) { + + if (learnts.size() > 0) { + curRestart = (conflicts / nbclausesbeforereduce) + 1; + reduceDB(); + if (!panicModeIsEnabled()) + nbclausesbeforereduce += incReduceDB; + } + } + + lastLearntClause = CRef_Undef; Lit next = lit_Undef; - while (decisionLevel() < assumptions.size()){ + while (decisionLevel() < assumptions.size()) { // Perform user provided assumption: Lit p = assumptions[decisionLevel()]; - if (value(p) == l_True){ + if (value(p) == l_True) { // Dummy decision level: newDecisionLevel(); - }else if (value(p) == l_False){ + } else if (value(p) == l_False) { analyzeFinal(~p, conflict); return l_False; - }else{ + } else { next = p; break; } } - if (next == lit_Undef){ + if (next == lit_Undef) { // New variable decision: decisions++; next = pickBranchLit(); - - if (next == lit_Undef){ - printf("c last restart ## conflicts : %d %d \n",conflictC,decisionLevel()); - // Model found: - return l_True; - } + if (next == lit_Undef) { + printf("c last restart ## conflicts : %d %d \n", conflictC, decisionLevel()); + // Model found: + return l_True; + } } // Increase decision level and enqueue 'next' @@ -1161,13 +1418,11 @@ lbool Solver::search(int nof_conflicts) } } +double Solver::progressEstimate() const { + double progress = 0; + double F = 1.0 / nVars(); -double Solver::progressEstimate() const -{ - double progress = 0; - double F = 1.0 / nVars(); - - for (int i = 0; i <= decisionLevel(); i++){ + for (int i = 0; i <= decisionLevel(); i++) { int beg = i == 0 ? 0 : trail_lim[i - 1]; int end = i == decisionLevel() ? trail.size() : trail_lim[i]; progress += pow(F, i) * (end - beg); @@ -1178,43 +1433,42 @@ double Solver::progressEstimate() const void Solver::printIncrementalStats() { - printf("c---------- Glucose Stats -------------------------\n"); - printf("c restarts : %lld\n", starts); - printf("c nb ReduceDB : %lld\n", nbReduceDB); - printf("c nb removed Clauses : %lld\n",nbRemovedClauses); - printf("c nb learnts DL2 : %lld\n", nbDL2); - printf("c nb learnts size 2 : %lld\n", nbBin); - printf("c nb learnts size 1 : %lld\n", nbUn); + printf("c---------- Glucose Stats -------------------------\n"); + printf("c restarts : %" PRIu64"\n", starts); + printf("c nb ReduceDB : %" PRIu64"\n", nbReduceDB); + printf("c nb removed Clauses : %" PRIu64"\n", nbRemovedClauses); + printf("c nb learnts DL2 : %" PRIu64"\n", nbDL2); + printf("c nb learnts size 2 : %" PRIu64"\n", nbBin); + printf("c nb learnts size 1 : %" PRIu64"\n", nbUn); - printf("c conflicts : %lld \n",conflicts); - printf("c decisions : %lld\n",decisions); - printf("c propagations : %lld\n",propagations); + printf("c conflicts : %" PRIu64"\n", conflicts); + printf("c decisions : %" PRIu64"\n", decisions); + printf("c propagations : %" PRIu64"\n", propagations); - printf("c SAT Calls : %d in %g seconds\n",nbSatCalls,totalTime4Sat); + printf("\nc SAT Calls : %d in %g seconds\n",nbSatCalls,totalTime4Sat); printf("c UNSAT Calls : %d in %g seconds\n",nbUnsatCalls,totalTime4Unsat); - printf("c--------------------------------------------------\n"); - + printf("c--------------------------------------------------\n"); } - // NOTE: assumptions passed in member-variable 'assumptions'. -lbool Solver::solve_() + +lbool Solver::solve_(bool do_simp, bool turn_off_simp) // Parameters are useless in core but useful for SimpSolver.... { - if(incremental && certifiedUNSAT) { + if(incremental && certifiedUNSAT) { printf("Can not use incremental and certified unsat in the same time\n"); exit(-1); } + model.clear(); conflict.clear(); if (!ok) return l_False; double curTime = cpuTime(); - solves++; - + lbool status = l_Undef; if(!incremental && verbosity>=1) { @@ -1222,14 +1476,14 @@ lbool Solver::solve_() printf("c | Constants are supposed to work well together :-) |\n"); printf("c | however, if you find better choices, please let us known... |\n"); printf("c |-------------------------------------------------------------------------------------------------------|\n"); - printf("c | | | |\n"); - printf("c | - Restarts: | - Reduce Clause DB: | - Minimize Asserting: |\n"); - printf("c | * LBD Queue : %6d | * First : %6d | * size < %3d |\n",lbdQueue.maxSize(),nbclausesbeforereduce,lbSizeMinimizingClause); - printf("c | * Trail Queue : %6d | * Inc : %6d | * lbd < %3d |\n",trailQueue.maxSize(),incReduceDB,lbLBDMinimizingClause); - printf("c | * K : %6.2f | * Special : %6d | |\n",K,specialIncReduceDB); - printf("c | * R : %6.2f | * Protected : (lbd)< %2d | |\n",R,lbLBDFrozenClause); - printf("c | | | |\n"); -printf("c ==================================[ Search Statistics (every %6d conflicts) ]=========================\n",verbEveryConflicts); + printf("c | | | |\n"); + printf("c | - Restarts: | - Reduce Clause DB: | - Minimize Asserting: |\n"); + printf("c | * LBD Queue : %6d | * First : %6d | * size < %3d |\n",lbdQueue.maxSize(),nbclausesbeforereduce,lbSizeMinimizingClause); + printf("c | * Trail Queue : %6d | * Inc : %6d | * lbd < %3d |\n",trailQueue.maxSize(),incReduceDB,lbLBDMinimizingClause); + printf("c | * K : %6.2f | * Special : %6d | |\n",K,specialIncReduceDB); + printf("c | * R : %6.2f | * Protected : (lbd)< %2d | |\n",R,lbLBDFrozenClause); + printf("c | | | |\n"); + printf("c ==================================[ Search Statistics (every %6d conflicts) ]=========================\n",verbEveryConflicts); printf("c | |\n"); printf("c | RESTARTS | ORIGINAL | LEARNT | Progress |\n"); @@ -1249,7 +1503,6 @@ printf("c ==================================[ Search Statistics (every %6d confl if (!incremental && verbosity >= 1) printf("c =========================================================================================================\n"); - if (certifiedUNSAT){ // Want certified output if (status == l_False) fprintf(certifiedOutput, "0\n"); @@ -1268,48 +1521,49 @@ printf("c ==================================[ Search Statistics (every %6d confl cancelUntil(0); + double finalTime = cpuTime(); if(status==l_True) { - nbSatCalls++; - totalTime4Sat +=(finalTime-curTime); + nbSatCalls++; + totalTime4Sat +=(finalTime-curTime); } if(status==l_False) { - nbUnsatCalls++; - totalTime4Unsat +=(finalTime-curTime); + nbUnsatCalls++; + totalTime4Unsat +=(finalTime-curTime); } - + return status; + } + + + + //================================================================================================= // Writing CNF to DIMACS: // // FIXME: this needs to be rewritten completely. -static Var mapVar(Var x, vec& map, Var& max) -{ - if (map.size() <= x || map[x] == -1){ - map.growTo(x+1, -1); +static Var mapVar(Var x, vec& map, Var& max) { + if (map.size() <= x || map[x] == -1) { + map.growTo(x + 1, -1); map[x] = max++; } return map[x]; } - -void Solver::toDimacs(FILE* f, Clause& c, vec& map, Var& max) -{ +void Solver::toDimacs(FILE* f, Clause& c, vec& map, Var& max) { if (satisfied(c)) return; for (int i = 0; i < c.size(); i++) if (value(c[i]) != l_False) - fprintf(f, "%s%d ", sign(c[i]) ? "-" : "", mapVar(var(c[i]), map, max)+1); + fprintf(f, "%s%d ", sign(c[i]) ? "-" : "", mapVar(var(c[i]), map, max) + 1); fprintf(f, "0\n"); } - -void Solver::toDimacs(const char *file, const vec& assumps) -{ +void Solver::toDimacs(const char *file, const vec& assumps) { FILE* f = fopen(file, "wr"); if (f == NULL) fprintf(stderr, "could not open file %s\n", file), exit(1); @@ -1317,15 +1571,15 @@ void Solver::toDimacs(const char *file, const vec& assumps) fclose(f); } - -void Solver::toDimacs(FILE* f, const vec& assumps) -{ +void Solver::toDimacs(FILE* f, const vec& assumps) { // Handle case when solver is in contradictory state: - if (!ok){ + if (!ok) { fprintf(f, "p cnf 1 2\n1 0\n-1 0\n"); - return; } + return; + } - vec map; Var max = 0; + vec map; + Var max = 0; // Cannot use removeClauses here because it is not safe // to deallocate them at this point. Could be improved. @@ -1333,9 +1587,9 @@ void Solver::toDimacs(FILE* f, const vec& assumps) for (int i = 0; i < clauses.size(); i++) if (!satisfied(ca[clauses[i]])) cnt++; - + for (int i = 0; i < clauses.size(); i++) - if (!satisfied(ca[clauses[i]])){ + if (!satisfied(ca[clauses[i]])) { Clause& c = ca[clauses[i]]; for (int j = 0; j < c.size(); j++) if (value(c[j]) != l_False) @@ -1347,9 +1601,9 @@ void Solver::toDimacs(FILE* f, const vec& assumps) fprintf(f, "p cnf %d %d\n", max, cnt); - for (int i = 0; i < assumptions.size(); i++){ + for (int i = 0; i < assumptions.size(); i++) { assert(value(assumptions[i]) != l_False); - fprintf(f, "%s%d 0\n", sign(assumptions[i]) ? "-" : "", mapVar(var(assumptions[i]), map, max)+1); + fprintf(f, "%s%d 0\n", sign(assumptions[i]) ? "-" : "", mapVar(var(assumptions[i]), map, max) + 1); } for (int i = 0; i < clauses.size(); i++) @@ -1363,15 +1617,15 @@ void Solver::toDimacs(FILE* f, const vec& assumps) //================================================================================================= // Garbage Collection methods: -void Solver::relocAll(ClauseAllocator& to) -{ +void Solver::relocAll(ClauseAllocator& to) { // All watchers: // // for (int i = 0; i < watches.size(); i++) watches.cleanAll(); watchesBin.cleanAll(); + unaryWatches.cleanAll(); for (int v = 0; v < nVars(); v++) - for (int s = 0; s < 2; s++){ + for (int s = 0; s < 2; s++) { Lit p = mkLit(v, s); // printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1); vec& ws = watches[p]; @@ -1380,11 +1634,14 @@ void Solver::relocAll(ClauseAllocator& to) vec& ws2 = watchesBin[p]; for (int j = 0; j < ws2.size(); j++) ca.reloc(ws2[j].cref, to); + vec& ws3 = unaryWatches[p]; + for (int j = 0; j < ws3.size(); j++) + ca.reloc(ws3[j].cref, to); } // All reasons: // - for (int i = 0; i < trail.size(); i++){ + for (int i = 0; i < trail.size(); i++) { Var v = var(trail[i]); if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)]))) @@ -1400,18 +1657,52 @@ void Solver::relocAll(ClauseAllocator& to) // for (int i = 0; i < clauses.size(); i++) ca.reloc(clauses[i], to); + + for (int i = 0; i < unaryWatchedClauses.size(); i++) + ca.reloc(unaryWatchedClauses[i], to); } -void Solver::garbageCollect() -{ + +void Solver::garbageCollect() { // Initialize the next region to a size corresponding to the estimated utilization degree. This // is not precise but should avoid some unnecessary reallocations for the new region: - ClauseAllocator to(ca.size() - ca.wasted()); + ClauseAllocator to(ca.size() - ca.wasted()); relocAll(to); if (verbosity >= 2) - printf("| Garbage collection: %12d bytes => %12d bytes |\n", - ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size); + printf("| Garbage collection: %12d bytes => %12d bytes |\n", + ca.size() * ClauseAllocator::Unit_Size, to.size() * ClauseAllocator::Unit_Size); to.moveTo(ca); } + +//-------------------------------------------------------------- +// Functions related to MultiThread. +// Useless in case of single core solver (aka original glucose) +// Keep them empty if you just use core solver +//-------------------------------------------------------------- + +bool Solver::panicModeIsEnabled() { + return false; +} + +void Solver::parallelImportUnaryClauses() { +} + +bool Solver::parallelImportClauses() { + return false; +} + + +void Solver::parallelExportUnaryClause(Lit p) { +} +void Solver::parallelExportClauseDuringSearch(Clause &c) { +} + +bool Solver::parallelJobIsFinished() { + // Parallel: another job has finished let's quit + return false; +} + +void Solver::parallelImportClauseDuringConflictAnalysis(Clause &c,CRef confl) { +} diff --git a/core/Solver.h b/core/Solver.h index d923628..63d5316 100644 --- a/core/Solver.h +++ b/core/Solver.h @@ -1,12 +1,33 @@ -/****************************************************************************************[Solver.h] - Glucose -- Copyright (c) 2009, Gilles Audemard, Laurent Simon - CRIL - Univ. Artois, France - LRI - Univ. Paris Sud, France - +/***************************************************************************************[Solver.h] + Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + LRI - Univ. Paris Sud, France (2009-2013) + Labri - Univ. Bordeaux, France + + Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + Labri - Univ. Bordeaux, 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). +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 +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 +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). + + +--------------- Original Minisat Copyrights ---------------- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson Copyright (c) 2007-2010, Niklas Sorensson @@ -24,18 +45,18 @@ NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPO 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. -**************************************************************************************************/ + **************************************************************************************************/ #ifndef Glucose_Solver_h #define Glucose_Solver_h -#include "mtl/Vec.h" #include "mtl/Heap.h" #include "mtl/Alg.h" #include "utils/Options.h" #include "core/SolverTypes.h" #include "core/BoundedQueue.h" #include "core/Constants.h" +#include "mtl/Clone.h" namespace Glucose { @@ -43,24 +64,35 @@ namespace Glucose { //================================================================================================= // Solver -- the main class: -class Solver { +class Solver : public Clone { + + friend class SolverConfiguration; + public: // Constructor/Destructor: // Solver(); + Solver(const Solver &s); + virtual ~Solver(); + + /** + * Clone function + */ + virtual Clone* clone() const { + return new Solver(*this); + } // Problem specification: // - Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode. - + 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 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_( vec& ps); // Add a clause to the solver without making superflous internal copy. Will + virtual bool addClause_( vec& ps); // Add a clause to the solver without making superflous internal copy. Will // change the passed vector 'ps'. // Solving: @@ -74,17 +106,19 @@ class Solver { bool solve (Lit p, Lit q, Lit r); // Search for a model that respects three assumptions. bool okay () const; // FALSE means solver is in a conflicting state + // Convenience versions of 'toDimacs()': void toDimacs (FILE* f, const vec& assumps); // Write CNF to file in DIMACS-format. void toDimacs (const char *file, const vec& assumps); void toDimacs (FILE* f, Clause& c, vec& map, Var& max); - void printLit(Lit l); - void printClause(CRef c); - void printInitialClause(CRef c); - // Convenience versions of 'toDimacs()': void toDimacs (const char* file); 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: // @@ -103,11 +137,13 @@ class Solver { int nVars () const; // The current number of variables. int nFreeVars () const; + inline char valuePhase(Var v) {return polarity[v];} + // Incremental mode void setIncrementalMode(); void initNbInitialVars(int nb); void printIncrementalStats(); - + bool isIncremental(); // Resource contraints: // void setConfBudget(int64_t x); @@ -122,9 +158,6 @@ class Solver { void checkGarbage(double gf); void checkGarbage(); - - - // Extra results: (read-only member variable) // vec model; // If problem is satisfiable, this vector contains the model (if any). @@ -136,6 +169,7 @@ class Solver { int verbosity; int verbEveryConflicts; int showModel; + // Constants For restarts double K; double R; @@ -143,16 +177,18 @@ class Solver { double sizeTrailQueue; // Constants for reduce DB - int firstReduceDB; - int incReduceDB; - int specialIncReduceDB; + int firstReduceDB; + int incReduceDB; + int specialIncReduceDB; unsigned int lbLBDFrozenClause; // Constant for reducing clause - int lbSizeMinimizingClause; + int lbSizeMinimizingClause; unsigned int lbLBDMinimizingClause; + // Constant for heuristic double var_decay; + double max_var_decay; double clause_decay; double random_var_freq; double random_seed; @@ -160,19 +196,44 @@ class Solver { int phase_saving; // Controls the level of phase saving (0=none, 1=limited, 2=full). bool rnd_pol; // Use random polarities for branching heuristics. bool rnd_init_act; // Initialize variable activities with a small random value. + + // Constant for Memory managment double garbage_frac; // The fraction of wasted memory allowed before a garbage collection is triggered. // Certified UNSAT ( Thanks to Marijn Heule) FILE* certifiedOutput; bool certifiedUNSAT; + // 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 + // Overide in ParallelSolver + virtual void parallelImportClauseDuringConflictAnalysis(Clause &c,CRef confl); + virtual bool parallelImportClauses(); // true if the empty clause was received + virtual void parallelImportUnaryClauses(); + virtual void parallelExportUnaryClause(Lit p); + virtual void parallelExportClauseDuringSearch(Clause &c); + virtual bool parallelJobIsFinished(); + virtual bool panicModeIsEnabled(); + + + // Statistics: (read-only member variable) + uint64_t nbPromoted; // Number of clauses from unary to binary watch scheme + uint64_t originalClausesSeen; // Number of original clauses seen + uint64_t sumDecisionLevels; // - uint64_t nbRemovedClauses,nbReducedClauses,nbDL2,nbBin,nbUn,nbReduceDB,solves, starts, decisions, rnd_decisions, propagations, conflicts,conflictsRestarts,nbstopsrestarts,nbstopsrestartssame,lastblockatrestart; + uint64_t nbRemovedClauses,nbRemovedUnaryWatchedClauses, nbReducedClauses,nbDL2,nbBin,nbUn,nbReduceDB,solves, starts, decisions, rnd_decisions, propagations, conflicts,conflictsRestarts,nbstopsrestarts,nbstopsrestartssame,lastblockatrestart; uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals; protected: + long curRestart; // Helper structures: // @@ -185,6 +246,12 @@ class Solver { Watcher(CRef cr, Lit p) : cref(cr), blocker(p) {} bool operator==(const Watcher& w) const { return cref == w.cref; } bool operator!=(const Watcher& w) const { return cref != w.cref; } +/* Watcher &operator=(Watcher w) { + this->cref = w.cref; + this->blocker = w.blocker; + return *this; + } +*/ }; struct WatcherDeleted @@ -203,7 +270,7 @@ class Solver { // Solver state: // - int lastIndexRed; + int lastIndexRed; bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used! double cla_inc; // Amount to bump next clause with. vec activity; // A heuristic measurement of the activity of a variable. @@ -212,14 +279,17 @@ class Solver { watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). OccLists, WatcherDeleted> watchesBin; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). + OccLists, WatcherDeleted> + unaryWatches; // Unary watch scheme (clauses are seen when they become empty vec clauses; // List of problem clauses. vec learnts; // List of learnt clauses. + vec unaryWatchedClauses; // List of imported clauses (after the purgatory) // TODO put inside ParallelSolver vec assigns; // The current assignments. vec polarity; // The preferred polarity of each variable. vec decision; // Declares if a variable is eligible for selection in the decision heuristic. vec trail; // Assignment stack; stores all assigments made in the order they were made. - vec nbpos; + vec nbpos; vec trail_lim; // Separator indices for different decision levels in 'trail'. vec vardata; // Stores reason and level for each variable. int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat). @@ -229,20 +299,23 @@ class Solver { Heap order_heap; // A priority queue of variables ordered with respect to the variable activity. 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 + bool reduceOnSize; + int reduceOnSizeSize; // See XMinisat paper + vec permDiff; // permDiff[var] contains the current conflict number... Used to count the number of LBD -#ifdef UPDATEVARACTIVITY + // UPDATEVARACTIVITY trick (see competition'09 companion paper) vec lastDecisionLevel; -#endif 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... int sumAssumptions; + CRef lastLearntClause; // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is @@ -254,7 +327,7 @@ class Solver { vec add_tmp; unsigned int MYFLAG; - + // Initial reduceDB strategy double max_learnts; double learntsize_adjust_confl; int learntsize_adjust_cnt; @@ -265,7 +338,6 @@ class Solver { int64_t propagation_budget; // -1 means no budget. bool asynch_interrupt; - // Variables added for incremental mode int incremental; // Use incremental SAT Solver int nbVarsInitialFormula; // nb VAR in formula without assumptions (incremental SAT) @@ -282,13 +354,14 @@ class Solver { void uncheckedEnqueue (Lit p, CRef from = CRef_Undef); // Enqueue a literal. Assumes value of literal is undefined. bool enqueue (Lit p, CRef from = CRef_Undef); // Test if fact 'p' contradicts current state, enqueue otherwise. CRef propagate (); // Perform unit propagation. Returns possibly conflicting clause. + CRef propagateUnaryWatches(Lit p); // Perform propagation on unary watches of p, can find only conflicts void cancelUntil (int level); // Backtrack until a certain level. void analyze (CRef confl, vec& out_learnt, vec & selectors, int& out_btlevel,unsigned int &nblevels,unsigned int &szWithoutSelectors); // (bt = backtrack) void analyzeFinal (Lit p, vec& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION? bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') lbool search (int nof_conflicts); // Search for a given number of conflicts. - lbool solve_ (); // Main solve method (assumptions given in 'assumptions'). - void reduceDB (); // Reduce the set of learnt clauses. + virtual lbool solve_ (bool do_simp = true, bool turn_off_simp = false); // Main solve method (assumptions given in 'assumptions'). + virtual void reduceDB (); // Reduce the set of learnt clauses. void removeSatisfied (vec& cs); // Shrink 'cs' to contain only non-satisfied clauses. void rebuildOrderHeap (); @@ -304,7 +377,9 @@ class Solver { // void attachClause (CRef cr); // Attach a clause to watcher lists. void detachClause (CRef cr, bool strict = false); // Detach a clause to watcher lists. - void removeClause (CRef cr); // Detach and free a clause. + void detachClausePurgatory(CRef cr, bool strict = false); + void attachClausePurgatory(CRef cr); + void removeClause (CRef cr, bool inPurgatory = false); // Detach and free a clause. bool locked (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state. bool satisfied (const Clause& c) const; // Returns TRUE if a clause is satisfied in the current state. @@ -312,7 +387,7 @@ class Solver { unsigned int computeLBD(const Clause &c); void minimisationWithBinaryResolution(vec &out_learnt); - void relocAll (ClauseAllocator& to); + virtual void relocAll (ClauseAllocator& to); // Misc: // @@ -439,6 +514,7 @@ 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); } + //================================================================================================= // Debug etc: @@ -469,8 +545,37 @@ inline void Solver::printInitialClause(CRef cr) } } - //================================================================================================= + +struct reduceDB_lt { + ClauseAllocator& ca; + + reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) { + } + + bool operator()(CRef x, CRef y) { + + // Main criteria... Like in MiniSat we keep all binary clauses + if (ca[x].size() > 2 && ca[y].size() == 2) return 1; + + if (ca[y].size() > 2 && ca[x].size() == 2) return 0; + if (ca[x].size() == 2 && ca[y].size() == 2) return 0; + + // Second one based on literal block distance + if (ca[x].lbd() > ca[y].lbd()) return 1; + if (ca[x].lbd() < ca[y].lbd()) return 0; + + + // Finally we can use old activity or size, we choose the last one + 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()); } + } +}; + + } + #endif diff --git a/core/SolverTypes.h b/core/SolverTypes.h index b310489..a905afb 100644 --- a/core/SolverTypes.h +++ b/core/SolverTypes.h @@ -1,12 +1,33 @@ -/***********************************************************************************[SolverTypes.h] - Glucose -- Copyright (c) 2009, Gilles Audemard, Laurent Simon - CRIL - Univ. Artois, France - LRI - Univ. Paris Sud, France - +/***************************************************************************************[SolverTypes.h] + Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + LRI - Univ. Paris Sud, France (2009-2013) + Labri - Univ. Bordeaux, France + + Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + Labri - Univ. Bordeaux, 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). +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 +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 +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). + + +--------------- Original Minisat Copyrights ---------------- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson Copyright (c) 2007-2010, Niklas Sorensson @@ -24,13 +45,15 @@ NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPO 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. -**************************************************************************************************/ + **************************************************************************************************/ #ifndef Glucose_SolverTypes_h #define Glucose_SolverTypes_h #include +#include +#include #include "mtl/IntTypes.h" #include "mtl/Alg.h" @@ -38,6 +61,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "mtl/Map.h" #include "mtl/Alloc.h" + namespace Glucose { //================================================================================================= @@ -128,56 +152,76 @@ inline lbool toLbool(int v) { return lbool((uint8_t)v); } class Clause; typedef RegionAllocator::Ref CRef; +#define BITS_LBD 13 +#define BITS_SIZEWITHOUTSEL 19 +#define BITS_REALSIZE 21 class Clause { struct { - unsigned mark : 2; - unsigned learnt : 1; - unsigned has_extra : 1; - unsigned reloced : 1; - unsigned lbd : 26; - unsigned canbedel : 1; - unsigned size : 32; - unsigned szWithoutSelectors : 32; - - } header; + unsigned mark : 2; + unsigned learnt : 1; + unsigned szWithoutSelectors : BITS_SIZEWITHOUTSEL; + unsigned canbedel : 1; + unsigned extra_size : 2; // extra size (end of 32bits) 0..3 + unsigned size : BITS_REALSIZE; + unsigned seen : 1; + unsigned reloced : 1; + unsigned exported : 2; // Values to keep track of the clause status for exportations + unsigned oneWatched : 1; + unsigned lbd : BITS_LBD; + } header; + union { Lit lit; float act; uint32_t abs; CRef rel; } data[0]; friend class ClauseAllocator; // NOTE: This constructor cannot be used directly (doesn't allocate enough memory). template - Clause(const V& ps, bool use_extra, bool learnt) { + Clause(const V& ps, int _extra_size, bool learnt) { + assert(_extra_size < (1<<2)); header.mark = 0; header.learnt = learnt; - header.has_extra = use_extra; + header.extra_size = _extra_size; header.reloced = 0; header.size = ps.size(); header.lbd = 0; header.canbedel = 1; + header.exported = 0; + header.oneWatched = 0; + header.seen = 0; for (int i = 0; i < ps.size(); i++) data[i].lit = ps[i]; - if (header.has_extra){ + if (header.extra_size > 0){ if (header.learnt) data[header.size].act = 0; else - calcAbstraction(); } + calcAbstraction(); + if (header.extra_size > 1) { + data[header.size+1].abs = 0; // learntFrom + } + } } public: void calcAbstraction() { - assert(header.has_extra); + assert(header.extra_size > 0); uint32_t abstraction = 0; for (int i = 0; i < size(); i++) abstraction |= 1 << (var(data[i].lit) & 31); data[header.size].abs = abstraction; } - int size () const { return header.size; } - void shrink (int i) { assert(i <= size()); if (header.has_extra) data[header.size-i] = data[header.size]; header.size -= i; } + void shrink (int i) { assert(i <= size()); + 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]; + } + } + header.size -= i; } void pop () { shrink(1); } bool learnt () const { return header.learnt; } - bool has_extra () const { return header.has_extra; } + bool has_extra () const { return header.extra_size > 0; } uint32_t mark () const { return header.mark; } void mark (uint32_t m) { header.mark = m; } const Lit& last () const { return data[header.size-1].lit; } @@ -192,16 +236,27 @@ class Clause { Lit operator [] (int i) const { return data[i].lit; } operator const Lit* (void) const { return (Lit*)data; } - float& activity () { assert(header.has_extra); return data[header.size].act; } - uint32_t abstraction () const { assert(header.has_extra); return data[header.size].abs; } + float& activity () { assert(header.extra_size > 0); return data[header.size].act; } + uint32_t abstraction () const { assert(header.extra_size > 0); return data[header.size].abs; } + + // Handle imported clauses lazy sharing + bool wasImported() const {return header.extra_size > 1;} + uint32_t importedFrom () const { assert(header.extra_size > 1); return data[header.size + 1].abs;} + void setImportedFrom(uint32_t ifrom) {assert(header.extra_size > 1); data[header.size+1].abs = ifrom;} Lit subsumes (const Clause& other) const; void strengthen (Lit p); - void setLBD(int i) {header.lbd = i;} + void setLBD(int i) {if (i < (1<<(BITS_LBD-1))) header.lbd = i; else header.lbd = (1<<(BITS_LBD-1));} // unsigned int& lbd () { return header.lbd; } unsigned int lbd () const { return header.lbd; } void setCanBeDel(bool b) {header.canbedel = b;} bool canBeDel() {return header.canbedel;} + void setSeen(bool b) {header.seen = b;} + bool getSeen() {return header.seen;} + void setExported(unsigned int b) {header.exported = b;} + unsigned int getExported() {return header.exported;} + void setOneWatched(bool b) {header.oneWatched = b;} + bool getOneWatched() {return header.oneWatched;} void setSizeWithoutSelectors (unsigned int n) {header.szWithoutSelectors = n; } unsigned int sizeWithoutSelectors () const { return header.szWithoutSelectors; } @@ -215,8 +270,8 @@ class Clause { const CRef CRef_Undef = RegionAllocator::Ref_Undef; class ClauseAllocator : public RegionAllocator { - static int clauseWord32Size(int size, bool has_extra){ - return (sizeof(Clause) + (sizeof(Lit) * (size + (int)has_extra))) / sizeof(uint32_t); } + static int clauseWord32Size(int size, int extra_size){ + return (sizeof(Clause) + (sizeof(Lit) * (size + extra_size))) / sizeof(uint32_t); } public: bool extra_clause_field; @@ -228,14 +283,15 @@ class ClauseAllocator : public RegionAllocator RegionAllocator::moveTo(to); } template - CRef alloc(const Lits& ps, bool learnt = false) + CRef alloc(const Lits& ps, bool learnt = false, bool imported = false) { assert(sizeof(Lit) == sizeof(uint32_t)); assert(sizeof(float) == sizeof(uint32_t)); + bool use_extra = learnt | extra_clause_field; - - CRef cid = RegionAllocator::alloc(clauseWord32Size(ps.size(), use_extra)); - new (lea(cid)) Clause(ps, use_extra, learnt); + int extra_size = imported?3:(use_extra?1:0); + CRef cid = RegionAllocator::alloc(clauseWord32Size(ps.size(), extra_size)); + new (lea(cid)) Clause(ps, extra_size, learnt); return cid; } @@ -259,7 +315,7 @@ class ClauseAllocator : public RegionAllocator if (c.reloced()) { cr = c.relocation(); return; } - cr = to.alloc(c, c.learnt()); + cr = to.alloc(c, c.learnt(), c.wasImported()); c.relocate(cr); // Copy extra data-fields: @@ -268,8 +324,14 @@ class ClauseAllocator : public RegionAllocator if (to[cr].learnt()) { to[cr].activity() = c.activity(); to[cr].setLBD(c.lbd()); + to[cr].setExported(c.getExported()); + to[cr].setOneWatched(c.getOneWatched()); + to[cr].setSeen(c.getSeen()); to[cr].setSizeWithoutSelectors(c.sizeWithoutSelectors()); to[cr].setCanBeDel(c.canBeDel()); + if (c.wasImported()) { + to[cr].setImportedFrom(c.importedFrom()); + } } else if (to[cr].has_extra()) to[cr].calcAbstraction(); } @@ -296,6 +358,15 @@ class OccLists Vec& lookup (const Idx& idx){ if (dirty[toInt(idx)]) clean(idx); return occs[toInt(idx)]; } void cleanAll (); + void copyTo(OccLists ©) const { + + copy.occs.growTo(occs.size()); + for(int i = 0;i 0); assert(other.header.extra_size > 0); if (other.header.size < header.size || (data[header.size].abs & ~other.data[other.header.size].abs) != 0) return lit_Error; diff --git a/mtl/Alloc.h b/mtl/Alloc.h index 61264a2..baa6095 100644 --- a/mtl/Alloc.h +++ b/mtl/Alloc.h @@ -54,6 +54,7 @@ class RegionAllocator uint32_t size () const { return sz; } + uint32_t getCap () const { return cap;} uint32_t wasted () const { return wasted_; } Ref alloc (int size); @@ -79,6 +80,16 @@ class RegionAllocator sz = cap = wasted_ = 0; } + void copyTo(RegionAllocator& to) const { + // if (to.memory != NULL) ::free(to.memory); + to.memory = (T*)xrealloc(to.memory, sizeof(T)*cap); + memcpy(to.memory,memory,sizeof(T)*cap); + to.sz = sz; + to.cap = cap; + to.wasted_ = wasted_; + } + + }; diff --git a/mtl/Clone.h b/mtl/Clone.h new file mode 100644 index 0000000..c0ec225 --- /dev/null +++ b/mtl/Clone.h @@ -0,0 +1,13 @@ +#ifndef Glucose_Clone_h +#define Glucose_Clone_h + + +namespace Glucose { + + class Clone { + public: + virtual Clone* clone() const = 0; + }; +}; + +#endif \ No newline at end of file diff --git a/mtl/Heap.h b/mtl/Heap.h index e134b98..0c40c4f 100644 --- a/mtl/Heap.h +++ b/mtl/Heap.h @@ -41,6 +41,7 @@ class Heap { static inline int parent(int i) { return (i-1) >> 1; } + void percolateUp(int i) { int x = heap[i]; @@ -84,6 +85,7 @@ class Heap { void decrease (int n) { assert(inHeap(n)); percolateUp (indices[n]); } void increase (int n) { assert(inHeap(n)); percolateDown(indices[n]); } + void copyTo(Heap& copy) const {heap.copyTo(copy.heap);indices.copyTo(copy.indices);} // Safe variant of insert/decrease/increase: void update(int n) diff --git a/mtl/Queue.h b/mtl/Queue.h index 6bb1d56..c71e45b 100644 --- a/mtl/Queue.h +++ b/mtl/Queue.h @@ -41,11 +41,22 @@ class Queue { void clear (bool dealloc = false) { buf.clear(dealloc); buf.growTo(1); first = end = 0; } int size () const { return (end >= first) ? end - first : end - first + buf.size(); } + + const T& operator [] (int index) const { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; } T& operator [] (int index) { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; } T peek () const { assert(first != end); return buf[first]; } void pop () { assert(first != end); first++; if (first == buf.size()) first = 0; } + + + void copyTo(Queue& copy) const { + copy.first = first; + copy.end = end; + buf.memCopyTo(copy.buf); + } + + void insert(T elem) { // INVARIANT: buf[end] is always unused buf[end++] = elem; if (end == buf.size()) end = 0; diff --git a/mtl/Vec.h b/mtl/Vec.h index e93a2ca..954eef7 100644 --- a/mtl/Vec.h +++ b/mtl/Vec.h @@ -26,6 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "mtl/IntTypes.h" #include "mtl/XAlloc.h" +#include namespace Glucose { @@ -89,6 +90,12 @@ class vec { // Duplicatation (preferred instead): void copyTo(vec& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; } void moveTo(vec& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; } + void memCopyTo(vec& copy) const{ + copy.capacity(cap); + copy.sz = sz; + memcpy(copy.data,data,sizeof(T)*cap); + } + }; diff --git a/mtl/template.mk b/mtl/template.mk index f9bea84..6727559 100644 --- a/mtl/template.mk +++ b/mtl/template.mk @@ -19,8 +19,8 @@ RCOBJS = $(addsuffix r, $(COBJS)) #CXX ?= /usr/gcc-/bin/g++-4.7.0 CXX ?= g++ -CFLAGS ?= -Wall -Wno-parentheses -LFLAGS ?= -Wall +CFLAGS ?= -Wall -Wno-parentheses -std=c++11 +LFLAGS ?= -Wall -lpthread COPTIMIZE ?= -O3 diff --git a/parallel/ClausesBuffer.cc b/parallel/ClausesBuffer.cc new file mode 100644 index 0000000..5b18767 --- /dev/null +++ b/parallel/ClausesBuffer.cc @@ -0,0 +1,235 @@ +/**********************************************************************************[ClausesBuffer.cc] + Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + LRI - Univ. Paris Sud, France (2009-2013) + Labri - Univ. Bordeaux, France + + Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + 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 +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 +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 +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). + + +--------------- Original Minisat Copyrights + +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. + **************************************************************************************************/ + +/* ClausesBuffer + * + * This class is responsible for exchanging clauses between threads. + * It is based on a fixed-length FIFO array of literals. + * If the FIFO is full, then old clauses are removed (even if it was not yet sent to all threads) + * + * a clause " l1 l2 l3" is pushed in the FIFO with the following 6 unsigned integers + * 3 nseen origin l1 l2 l3 + * + 3 is the size of the pushed clause + * + nseen is the number of thread which imported this clause (initialized with nthreads-1) + * (when set to 0, the clause is removed from the fifo) + * + origin is the thread id of the thread which added this clause to the fifo + * + l1 l2 l3 are the literals of the clause + * + * ********************************************************************************************** + * **CAREFUL** This class is not thread-safe. In glucose-syrup, the SharedCompanion is + * responsible for ensuring atomicity of main functions + * ********************************************************************************************** + * + * */ + +#include "parallel/ClausesBuffer.h" + +//================================================================================================= + +using namespace Glucose; + +extern BoolOption opt_whenFullRemoveOlder; +extern IntOption opt_fifoSizeByCore; + +// index : size clause +// index + 1 : nbSeen +// index + 2 : threadId +// index + 3 : .. index + 3 + size : Lit of clause +ClausesBuffer::ClausesBuffer(int _nbThreads, unsigned int _maxsize) : first(0), last(_maxsize-1), + maxsize(_maxsize), queuesize(0), + removedClauses(0), + forcedRemovedClauses(0), nbThreads(_nbThreads), + whenFullRemoveOlder(opt_whenFullRemoveOlder), fifoSizeByCore(opt_fifoSizeByCore) { + lastOfThread.growTo(_nbThreads); + for(int i=0;i= maxsize) + return i - maxsize; + return i; +} + +void ClausesBuffer::removeLastClause() { + assert(queuesize > 0); + do { + unsigned int size = (unsigned int) elems[nextIndex(last)]; + unsigned int nextlast = addIndex(last, size+headerSize); + + for(int i=0;i 0); + queuesize --; + } + removedClauses ++; + assert(last >= 0); + assert(last < maxsize); + assert(last == nextlast); + } while (queuesize > 0 && (elems[addIndex(last,2)] == 0)); + +} + + +// Pushes a single uint to the fifo +inline void ClausesBuffer::noCheckPush(uint32_t x) { + elems[first] = x; + first = nextIndex(first); +} + +// Pops a single uint from the fifo +inline uint32_t ClausesBuffer::noCheckPop(uint32_t & index) { + index = nextIndex(index); + uint32_t ret = elems[index]; + return ret; +} + + + +// Return true if the clause was succesfully added +bool ClausesBuffer::pushClause(int threadId, Clause & c) { + if (!whenFullRemoveOlder && (queuesize + c.size() + headerSize >= maxsize)) + return false; // We need to remove some old clauses + while (queuesize + c.size() + headerSize >= maxsize) { // We need to remove some old clauses + forcedRemovedClauses ++; + removeLastClause(); + assert(queuesize > 0); + } + noCheckPush(c.size()); + noCheckPush(nbThreads>1?nbThreads-1:1); + noCheckPush(threadId); + for(int i=0;i (%d, %d)\n", first, last); +} + +bool ClausesBuffer::getClause(int threadId, int & threadOrigin, vec & resultClause, bool firstFound) { + assert(lastOfThread.size() > threadId); + unsigned int thislast = lastOfThread[threadId]; + assert(!firstFound || thislast == last); // FIXME: Gilles has this assertion on his cluster + + // Early exiting + if (nextIndex(thislast) == first) return false; + + if ( ( thislast < last && last < first) || + ( first < thislast && thislast < last ) || + ( last < first && first < thislast) ) { + // Special case where last has moved and lastOfThread[threadId] is no more valid (is behind) + thislast = last; + } + assert(!firstFound); + // Go to next clause for this thread id + if (!firstFound) { + while (nextIndex(thislast) != first && elems[addIndex(thislast,3)] == ((unsigned int)threadId)) { // 3 = 2 + 1 + thislast = addIndex(thislast, elems[nextIndex(thislast)] + headerSize); // + assert(thislast >= 0); + assert(thislast < maxsize); + } + assert(nextIndex(thislast)==first || elems[addIndex(thislast,3)] != (unsigned int)threadId); + } + + if (nextIndex(thislast) == first) { + lastOfThread[threadId] = thislast; + return false; + } + assert(elems[addIndex(thislast,3)] != ((unsigned int) threadId)); + unsigned int previouslast = thislast; + bool removeAfter = false; + int csize = noCheckPop(thislast); + removeAfter = (--elems[addIndex(thislast,1)] == 0); // We are sure this is not one of our own clause + thislast = nextIndex(thislast); // Skips the removeAfter fieldr + threadOrigin = noCheckPop(thislast); + assert(threadOrigin != threadId); + resultClause.clear(); + for(int i=0;i elems; + unsigned int first; + unsigned int last; + unsigned int maxsize; + unsigned int queuesize; // Number of current elements (must be < maxsize !) + unsigned int removedClauses; + unsigned int forcedRemovedClauses; + static const int headerSize = 3; + int nbThreads; + bool whenFullRemoveOlder; + unsigned int fifoSizeByCore; + vec lastOfThread; // Last value for a thread + + public: + ClausesBuffer(int _nbThreads, unsigned int _maxsize); + ClausesBuffer(); + + void setNbThreads(int _nbThreads); + unsigned int nextIndex(unsigned int i); + unsigned int addIndex(unsigned int i, unsigned int a); + void removeLastClause(); + + void noCheckPush(uint32_t x); + uint32_t noCheckPop(unsigned int & index); + + // Return true if the clause was succesfully added + bool pushClause(int threadId, Clause & c); + bool getClause(int threadId, int & threadOrigin, vec & resultClause, bool firstFound = false); + + int maxSize() const {return maxsize;} + uint32_t getCap(); + void growTo(int size) { + assert(0); // Not implemented (essentially for efficiency reasons) + elems.growTo(size); + first=0; maxsize=size; queuesize = 0;last = 0; + for(int i=0;i + +#include +#include + + +#include "utils/System.h" +#include "utils/ParseUtils.h" +#include "utils/Options.h" +#include "core/Dimacs.h" +#include "core/SolverTypes.h" + +#include "simp/SimpSolver.h" +#include "parallel/ParallelSolver.h" +#include "parallel/MultiSolvers.h" + +using namespace Glucose; + + + +static MultiSolvers* pmsolver; + +// 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) { pmsolver->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 (pmsolver->verbosity() > 0){ + pmsolver->printFinalStats(); + printf("\n"); printf("*** INTERRUPTED ***\n"); } + _exit(1); } + + +//================================================================================================= +// Main: + + +int main(int argc, char** argv) +{ + double realTimeStart = realTime(); + printf("c\nc This is glucose-syrup 4.0 (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"); + +#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); + + MultiSolvers msolver; + pmsolver = & msolver; + msolver.setVerbosity(verb); + msolver.setVerbEveryConflicts(vv); + msolver.setShowModel(mod); + + double initial_time = cpuTime(); + + // 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 (msolver.verbosity() > 0){ + printf("c ========================================[ Problem Statistics ]===========================================\n"); + printf("c | |\n"); } + + parse_DIMACS(in, msolver); + gzclose(in); + + + + FILE* res = (argc >= 3) ? fopen(argv[argc-1], "wb") : NULL; + + if (msolver.verbosity() > 0){ + printf("c | Number of variables: %12d |\n", msolver.nVars()); + printf("c | Number of clauses: %12d |\n", msolver.nClauses()); } + + double parsed_time = cpuTime(); + if (msolver.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); + + + int ret2 = msolver.simplify(); + if(ret2) + msolver.eliminate(); + double simplified_time = cpuTime(); + if (msolver.verbosity() > 0){ + printf("c | Simplification time: %12.2f s |\n", simplified_time - parsed_time); + printf("c | |\n"); } + + if (!ret2 || !msolver.okay()){ + //if (S.certifiedOutput != NULL) fprintf(S.certifiedOutput, "0\n"), fclose(S.certifiedOutput); + if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res); + if (msolver.verbosity() > 0){ + printf("c =========================================================================================================\n"); + printf("Solved by unit propagation\n"); + printf("c real time : %g s\n", realTime() - realTimeStart); + printf("c cpu time : %g s\n", cpuTime()); + printf("\n"); } + printf("s UNSATISFIABLE\n"); + exit(20); + } + + // vec dummy; + lbool ret = msolver.solve(); + + + printf("c\n"); + printf("c real time : %g s\n", realTime() - realTimeStart); + printf("c cpu time : %g s\n", cpuTime()); + if (msolver.verbosity() > 0){ + msolver.printFinalStats(); + printf("\n"); } + + //-------------- Result is put in a external file + /* I must admit I have to print the model of one thread... But which one? FIXME !! + 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(msolver.getShowModel() && ret==l_True) { + printf("v "); + for (int i = 0; i < msolver.model.size() ; i++) + if (msolver.model[i] != l_Undef) + printf("%s%s%d", (i==0)?"":" ", (msolver.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/parallel/Makefile b/parallel/Makefile new file mode 100644 index 0000000..0da6c25 --- /dev/null +++ b/parallel/Makefile @@ -0,0 +1,4 @@ +EXEC = glucose-syrup +DEPDIR = mtl utils core simp +MROOT = $(PWD)/.. +include $(MROOT)/mtl/template.mk diff --git a/parallel/MultiSolvers.cc b/parallel/MultiSolvers.cc new file mode 100644 index 0000000..b0c1949 --- /dev/null +++ b/parallel/MultiSolvers.cc @@ -0,0 +1,543 @@ +/***************************************************************************************[MultiSolvers.cc] + Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + LRI - Univ. Paris Sud, France (2009-2013) + Labri - Univ. Bordeaux, France + + Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + 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 +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 +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 +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). + + +--------------- Original Minisat Copyrights + +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 "parallel/MultiSolvers.h" +#include "mtl/Sort.h" +#include "utils/System.h" +#include "simp/SimpSolver.h" +#include +#include +#include "parallel/SolverConfiguration.h" + +using namespace Glucose; + +extern const char* _parallel ; +extern const char* _cunstable; +// Options at the parallel solver level +static IntOption opt_nbsolversmultithreads (_parallel, "nthreads", "Number of core threads for syrup (0 for automatic)", 0); +static IntOption opt_maxnbsolvers (_parallel, "maxnbthreads", "Maximum number of core threads to ask for (when nbthreads=0)", 4); +static IntOption opt_maxmemory (_parallel, "maxmemory", "Maximum memory to use (in Mb, 0 for no software limit)", 3000); +static IntOption opt_statsInterval (_parallel, "statsinterval", "Seconds (real time) between two stats reports", 5); +// +// Shared with ClausesBuffer.cc +BoolOption opt_whenFullRemoveOlder (_parallel, "removeolder", "When the FIFO for exchanging clauses between threads is full, remove older clauses", false); +IntOption opt_fifoSizeByCore(_parallel, "fifosize", "Size of the FIFO structure for exchanging clauses between threads, by threads", 100000); +// +// Shared options with Solver.cc +BoolOption opt_dontExportDirectReusedClauses (_cunstable, "reusedClauses", "Don't export directly reused clauses", false); +BoolOption opt_plingeling (_cunstable, "plingeling", "plingeling strategy for sharing clauses (exploratory feature)", false); + +#include +#include +#include + +static inline double cpuTime(void) { + struct rusage ru; + getrusage(RUSAGE_SELF, &ru); +return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; } + + +void MultiSolvers::informEnd(lbool res) { + result = res; + pthread_cond_broadcast(&cfinished); +} + +MultiSolvers::MultiSolvers(ParallelSolver *s): + ok (true) + , maxnbthreads(4), nbthreads(opt_nbsolversmultithreads), nbsolvers(opt_nbsolversmultithreads) + , nbcompanions(4), nbcompbysolver(2) + , allClonesAreBuilt(0) + , showModel(false) + , winner(-1) + , var_decay(1 / 0.95), clause_decay(1 / 0.999),cla_inc(1), var_inc(1) + , random_var_freq(0.02) + , restart_first(100), restart_inc(1.5) + , learntsize_factor((double)1/(double)3), learntsize_inc(1.1) + , expensive_ccmin(true) + , polarity_mode (polarity_false) + , maxmemory(opt_maxmemory), maxnbsolvers(opt_maxnbsolvers) + , verb(0) , verbEveryConflicts(10000) + , numvar(0), numclauses(0) + +{ + result = l_Undef; + SharedCompanion *sc = new SharedCompanion(); + this->sharedcomp = sc; + + // Generate only solver 0. + // It loads the formula + // All others solvers are clone of this one + solvers.push(s); + s->verbosity = 0; // No reportf in solvers... All is done in MultiSolver + s->setThreadNumber(0); + //s->belongsto = this; + s->sharedcomp = sc; + sc->addSolver(s); + assert(solvers[0]->threadNumber() == 0); + + pthread_mutex_init(&m,NULL); //PTHREAD_MUTEX_INITIALIZER; + pthread_mutex_init(&mfinished,NULL); //PTHREAD_MUTEX_INITIALIZER; + pthread_cond_init(&cfinished,NULL); + + if (nbsolvers > 0 ) + fprintf(stdout,"c %d solvers engines and 1 companion as a blackboard created.\n", nbsolvers); +} + +MultiSolvers::MultiSolvers() : MultiSolvers(new ParallelSolver(-1)) { + +} + +MultiSolvers::~MultiSolvers() +{} + +/** + * Generate All solvers + */ + +void MultiSolvers::generateAllSolvers() { + assert(solvers[0] != NULL); + assert(allClonesAreBuilt==0); + + for(int i=1;iclone(); + solvers.push(s); + s->verbosity = 0; // No reportf in solvers... All is done in MultiSolver + s->setThreadNumber(i); + s->sharedcomp = this->sharedcomp; + this->sharedcomp->addSolver(s); + assert(solvers[i]->threadNumber() == i); + } + + adjustParameters(); + + allClonesAreBuilt = 1; +} + +/** + * Choose solver for threads i (if no given in command line see above) + */ + + +ParallelSolver* MultiSolvers::retrieveSolver(int i) { + return new ParallelSolver(i); +} + +Var MultiSolvers::newVar(bool sign, bool dvar) +{ + assert(solvers[0] != NULL); + numvar++; + int v; + sharedcomp->newVar(sign); + if(!allClonesAreBuilt) { // At the beginning we want to generate only solvers 0 + v = solvers[0]->newVar(sign,dvar); + assert(numvar == v+1); // Just a useless check + } else { + for(int i=0;inewVar(sign,dvar); + } + } + return numvar; +} + +bool MultiSolvers::addClause_(vec&ps) { + assert(solvers[0] != NULL); // There is at least one solver. + // Check if clause is satisfied and remove false/duplicate literals: + if (!okay()) return false; + + sort(ps); + Lit p; int i, j; + for (i = j = 0, p = lit_Undef; i < ps.size(); i++) + if (solvers[0]->value(ps[i]) == l_True || ps[i] == ~p) + return true; + else if (solvers[0]->value(ps[i]) != l_False && ps[i] != p) + ps[j++] = p = ps[i]; + ps.shrink(i - j); + + + if (ps.size() == 0) { + return ok = false; + } + else if (ps.size() == 1){ + assert(solvers[0]->value(ps[0]) == l_Undef); // TODO : Passes values to all threads + solvers[0]->uncheckedEnqueue(ps[0]); + if(!allClonesAreBuilt) { + return ok = ( (solvers[0]->propagate()) == CRef_Undef); // checks only main solver here for propagation constradiction + } + + // Here, all clones are built. + // Gives the unit clause to everybody + for(int i=0;iuncheckedEnqueue(ps[0]); + return ok = ( (solvers[0]->propagate()) == CRef_Undef); // checks only main solver here for propagation constradiction + }else{ + // printf("Adding clause %0xd for solver %d.\n",(void*)c, thn); + // At the beginning only solver 0 load the formula + solvers[0]->addClause(ps); + + if(!allClonesAreBuilt) { + numclauses++; + return true; + } + // Clones are built, need to pass the clause to all the threads + for(int i=1;iaddClause(ps); + } + numclauses++; + } + return true; +} + + +bool MultiSolvers::simplify() { + assert(solvers[0] != NULL); // There is at least one solver. + + if (!okay()) return false; + return ok = solvers[0]->simplify(); +} + + +bool MultiSolvers::eliminate() { + + // TODO allow variable elimination when all threads are built! + assert(allClonesAreBuilt==false); + + SimpSolver * s = (SimpSolver*)getPrimarySolver(); + return s->eliminate(true); +} + + +// TODO: Use a template here +void *localLaunch(void*arg) { + ParallelSolver* s = (ParallelSolver*)arg; + + (void)s->solve(); + + pthread_exit(NULL); +} + + +#define MAXIMUM_SLEEP_DURATION 5 +void MultiSolvers::printStats() { + static int nbprinted = 1; + double cpu_time = cpuTime(); + printf("c\n"); + + printf("c |-------------------------------------------------------------------------------------------------------|\n"); + printf("c | id | starts | decisions | confls | Init T | learnts | exported | imported | promoted | %% | \n"); + printf("c |-------------------------------------------------------------------------------------------------------|\n"); + + //printf("%.0fs | ",cpu_time); + for(int i=0;ireportProgress(); + //printf(" %2d: %12ld confl. |", i, (long int) solvers[i]->conflicts); + } + long long int totalconf = 0; + long long int totalprop = 0; + for(int i=0;iconflicts; + totalprop+= solvers[i]->propagations; + } + printf("c \n"); + + printf("c synthesis %11lld conflicts %11lld propagations %8.0f conflicts/sec %8.0f propagations/sec\n", + totalconf, totalprop, (double)totalconf / cpu_time, (double) totalprop / cpu_time); + + + nbprinted ++; +} + +// Still a ugly function... To be rewritten with some statistics class some day +void MultiSolvers::printFinalStats() { + sharedcomp->printStats(); + printf("c\nc\n"); + printf("c\n"); + printf("c |---------------------------------------- FINAL STATS --------------------------------------------------|\n"); + printf("c\n"); + + printf("c |---------------"); + for(int i = 0;iconflicts); + totalconf += solvers[i]->conflicts; + } + printf("| %15lld |\n",totalconf); + + printf("c | Exported "); + uint64_t exported = 0; + for(int i=0;inbexported); + exported += solvers[i]->nbexported; + } + printf("| %15" PRIu64" |\n", exported); + + printf("c | Imported "); + uint64_t imported = 0; + for(int i=0;inbimported); + imported += solvers[i]->nbimported; + } + printf("| %15" PRIu64" |\n", imported); + + printf("c | Good "); + uint64_t importedGood = 0; + for(int i=0;inbImportedGoodClauses); + importedGood += solvers[i]->nbImportedGoodClauses; + } + printf("| %15" PRIu64" |\n", importedGood); + + printf("c | Purge "); + uint64_t importedPurg = 0; + for(int i=0;inbimportedInPurgatory); + importedPurg += solvers[i]->nbimportedInPurgatory; + } + printf("| %15" PRIu64" |\n", importedPurg); + + printf("c | Promoted "); + uint64_t promoted = 0; + for(int i=0;inbPromoted); + promoted += solvers[i]->nbPromoted; + } + printf("| %15" PRIu64" |\n", promoted); + + printf("c | Remove imp "); + uint64_t removedimported = 0; + for(int i=0;inbRemovedUnaryWatchedClauses); + removedimported += solvers[i]->nbRemovedUnaryWatchedClauses; + } + printf("| %15" PRIu64" |\n", removedimported); + + printf("c | Blocked Reuse "); + uint64_t blockedreused = 0; + for(int i=0;inbNotExportedBecauseDirectlyReused); + blockedreused += solvers[i]->nbNotExportedBecauseDirectlyReused; + } + printf("| %15" PRIu64" |\n",blockedreused); + + + printf("c | Orig seen "); + for(int i=0;ioriginalClausesSeen); + } + printf("| |\n"); + + printf("c | Unaries "); + for(int i=0;inbUn); + } + printf("| |\n"); + + printf("c | Binaries "); + for(int i=0;inbBin); + } + printf("| |\n"); + + + printf("c | Glues "); + for(int i=0;inbDL2); + } + printf("| |\n"); + + + int winner = -1; + for(int i=0;iwinner()==solvers[i]) + winner = i; + } + + if(winner!=-1) { +int sum = 0; + printf("c | Hamming "); + for(int i = 0;ivaluePhase(j)!= solvers[winner]->valuePhase(j)) nb++; + } + printf("| %10d ",nb); + sum+=nb; + + } + printf("| %15d |\n",sum/(solvers.size()>1?solvers.size()-1:1)); + } + + printf("c |---------------"); + for(int i = 0;i=1) + printf("c | Automatic Adjustement of the number of solvers. MaxMemory=%5d, MaxCores=%3d. |\n", maxmemory, maxnbsolvers); + unsigned int tmpnbsolvers = maxmemory * 4 / 10 / mem; + if (tmpnbsolvers > maxnbsolvers) tmpnbsolvers = maxnbsolvers; + if (tmpnbsolvers < 1) tmpnbsolvers = 1; + if(verb>=1) + printf("c | One Solver is taking %.2fMb... Let's take %d solvers for this run (max 40%% of the maxmemory). |\n", mem, tmpnbsolvers); + nbsolvers = tmpnbsolvers; + nbthreads = nbsolvers; + } else { + assert(nbthreads == nbsolvers); + } +} + +lbool MultiSolvers::solve() { + pthread_attr_t thAttr; + int i; + + adjustNumberOfCores(); + sharedcomp->setNbThreads(nbsolvers); + if(verb>=1) + printf("c | Generating clones |\n"); + generateAllSolvers(); + if(verb>=1) { + printf("c |  all clones generated. Memory = %6.2fMb. |\n", memUsed()); + printf("c ========================================================================================================|\n"); + } + + + model.clear(); + + /* Initialize and set thread detached attribute */ + pthread_attr_init(&thAttr); + pthread_attr_setdetachstate(&thAttr, PTHREAD_CREATE_JOINABLE); + + + + // Launching all solvers + for (i = 0; i < nbsolvers; i++) { + pthread_t * pt = (pthread_t*)malloc(sizeof(pthread_t)); + threads.push(pt); + solvers[i]->pmfinished = &mfinished; + solvers[i]->pcfinished = &cfinished; + pthread_create(threads[i], &thAttr, &localLaunch, (void*)solvers[i]); + } + + bool done = false; + + (void)pthread_mutex_lock(&m); + while (!done) { + struct timespec timeout; + time(&timeout.tv_sec); + timeout.tv_sec += MAXIMUM_SLEEP_DURATION; + timeout.tv_nsec = 0; + if (pthread_cond_timedwait(&cfinished, &mfinished, &timeout) != ETIMEDOUT) + done = true; + else + printStats(); + + float mem = memUsed(); + if(verb>=1) printf("c Total Memory so far : %.2fMb\n", mem); + if ( (maxmemory > 0) && (mem > maxmemory) && !sharedcomp->panicMode) + printf("c ** reduceDB switching to Panic Mode due to memory limitations !\n"), sharedcomp->panicMode = true; + + } + (void)pthread_mutex_unlock(&m); + + for (i = 0; i < nbsolvers; i++) { // Wait for all threads to finish + pthread_join(*threads[i], NULL); + } + + assert(sharedcomp != NULL); + result = sharedcomp->jobStatus; + if (result == l_True) { + int n = sharedcomp->jobFinishedBy->nVars(); + model.growTo(n); + for(int i = 0; i < n; i++) + model[i] = sharedcomp->jobFinishedBy->model[i]; + } + + + return result; + /* + for(int i=0;i& ps); // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method! + bool addClause_( vec& ps); + + bool simplify (); // Removes already satisfied clauses. + + int nVars () const; // The current number of variables. + int nClauses () const; // The current number of variables. + ParallelSolver *getPrimarySolver(); + + void generateAllSolvers(); + + // Solving: + // + lbool solve (); // Search without assumptions. + bool eliminate(); // Perform variable elimination + void adjustParameters(); + void adjustNumberOfCores(); + void interrupt() {} + vec model; // If problem is satisfiable, this vector contains the model (if any). + inline bool okay() { + if(!ok) return ok; + for(int i = 0;iokay()) { + ok = false; + return false; + } + } + return true; + + } + + protected: + friend class ParallelSolver; + friend class SolverCompanion; + +struct Stats { + uint64_t min, max, avg, std, med; + Stats(uint64_t _min = 0,uint64_t _max = 0,uint64_t _avg = 0,uint64_t _std = 0,uint64_t _med = 0) : + min(_min), max(_max), avg(_avg), std(_std), med(_med) {} +}; + + void printStats(); + int ok; + lbool result; + int maxnbthreads; // Maximal number of threads + int nbthreads; // Current number of threads + int nbsolvers; // Number of CDCL solvers + int nbcompanions; // Number of companions + int nbcompbysolver; // Number of companions by solvers + bool immediateSharingGlue ; + int allClonesAreBuilt; + bool showModel; // show model on/off + + int winner; + + vec add_tmp; + + double var_decay; // Inverse of the variable activity decay factor. (default 1 / 0.95) + double clause_decay; // Inverse of the clause activity decay factor. (1 / 0.999) + double cla_inc; // Amount to bump next clause with. + double var_inc; // Amount to bump next variable with. + double random_var_freq; // The frequency with which the decision heuristic tries to choose a random variable. (default 0.02) + int restart_first; // The initial restart limit. (default 100) + double restart_inc; // The factor with which the restart limit is multiplied in each restart. (default 1.5) + double learntsize_factor; // The intitial limit for learnt clauses is a factor of the original clauses. (default 1 / 3) + double learntsize_inc; // The limit for learnt clauses is multiplied with this factor each restart. (default 1.1) + bool expensive_ccmin; // Controls conflict clause minimization. (default TRUE) + int polarity_mode; // Controls which polarity the decision heuristic chooses. See enum below for allowed modes. (default polarity_false) + unsigned int maxmemory; + unsigned int maxnbsolvers; + int verb; + int verbEveryConflicts; + int numvar; // Number of variables + int numclauses; // Number of clauses + + enum { polarity_true = 0, polarity_false = 1, polarity_user = 2, polarity_rnd = 3 }; + + //ClauseAllocator ca; + SharedCompanion * sharedcomp; + + void informEnd(lbool res); + ParallelSolver* retrieveSolver(int i); + + pthread_mutex_t m; // mutex for any high level sync between all threads (like reportf) + pthread_mutex_t mfinished; // mutex on which main process may wait for... As soon as one process finishes it release the mutex + pthread_cond_t cfinished; // condition variable that says that a thread has finished + + vec solvers; // set of plain solvers + vec solvercompanions; // set of companion solvers + vec threads; // all threads of this process + vec threadIndexOfSolver; // threadIndexOfSolver[solvers[i]] is the index in threads[] of the solver i + vec threadIndexOfSolverCompanion; // threadIndexOfSolverCompanion[solvercompanions[i]] is the index in threads[] of the solvercompanion i +}; + +inline bool MultiSolvers::addClause (const vec& ps) { ps.copyTo(add_tmp); return addClause_(add_tmp); } + +inline void MultiSolvers::setVerbosity(int i) {verb = i;} +inline void MultiSolvers::setVerbEveryConflicts(int i) {verbEveryConflicts=i;} +inline int MultiSolvers::nVars () const { return numvar; } +inline int MultiSolvers::nClauses () const { return numclauses; } +inline int MultiSolvers::verbosity() {return verb;} +inline ParallelSolver* MultiSolvers::getPrimarySolver() {return solvers[0];} + + +} +#endif + diff --git a/parallel/ParallelSolver.cc b/parallel/ParallelSolver.cc new file mode 100644 index 0000000..ff948e9 --- /dev/null +++ b/parallel/ParallelSolver.cc @@ -0,0 +1,490 @@ +/***************************************************************************************[ParallelSolver.cc] + Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + LRI - Univ. Paris Sud, France (2009-2013) + Labri - Univ. Bordeaux, France + + Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + 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 +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 +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 +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). + + +--------------- Original Minisat Copyrights + +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 "parallel/ParallelSolver.h" +#include "mtl/Sort.h" + +using namespace Glucose; + +const char* _cunstable = "CORE/PARALLEL -- UNSTABLE FEATURES"; +const char* _parallel = "PARALLEL"; + +extern BoolOption opt_dontExportDirectReusedClauses; // (_cunstable, "reusedClauses", "Don't export directly reused clauses", false); +extern BoolOption opt_plingeling; // (_cunstable, "plingeling", "plingeling strategy for sharing clauses (exploratory feature)", false); + + +ParallelSolver::ParallelSolver(int threadId) : + SimpSolver() +, thn(threadId) // The thread number of this solver +, nbexported(0) +, nbimported(0) +, nbexportedunit(0), nbimportedunit(0), nbimportedInPurgatory(0), nbImportedGoodClauses(0) +, goodlimitlbd(8) +, goodlimitsize(30) +, purgatory(true) +, shareAfterProbation(!opt_plingeling) // only share clauses after probation +, plingeling(opt_plingeling) +, firstSharing(5000) // Strong limit : do not share anything (except unary clauses) before this number of conflicts +, limitSharingByGoodLBD(true) // Moving limit of what a good LBD is (median value of last learnt clauses set) +, limitSharingByFixedLimitLBD(0) // No fixed bound (like 8 in plingeling) +, limitSharingByFixedLimitSize(0) // No fixed boud (like 40 in plingeling) +, dontExportDirectReusedClauses(opt_dontExportDirectReusedClauses) +, nbNotExportedBecauseDirectlyReused(0) +{ + useUnaryWatched = true; // We want to use promoted clauses here ! +} + + + + +ParallelSolver::~ParallelSolver() { + printf("c Solver of thread %d ended.\n", thn); + fflush(stdout); +} + +ParallelSolver::ParallelSolver(const ParallelSolver &s) : SimpSolver(s) +, nbexported(s.nbexported) +, nbimported(s.nbimported) +, nbexportedunit(s.nbexportedunit), nbimportedunit(s.nbimportedunit), nbimportedInPurgatory(s.nbimportedInPurgatory) +, nbImportedGoodClauses(s.nbImportedGoodClauses) +, goodlimitlbd(s.goodlimitlbd) +, goodlimitsize(s.goodlimitsize) +, purgatory(s.purgatory) +, shareAfterProbation(s.shareAfterProbation) // only share clauses after probation +, plingeling(s.plingeling) +, firstSharing(s.firstSharing) // Strong limit : do not share anything (except unary clauses) before this number of conflicts +, limitSharingByGoodLBD(s.limitSharingByGoodLBD) // Moving limit of what a good LBD is (median value of last learnt clauses set) +, limitSharingByFixedLimitLBD(s.limitSharingByFixedLimitLBD) // No fixed bound (like 8 in plingeling) +, limitSharingByFixedLimitSize(s.limitSharingByFixedLimitSize) // No fixed boud (like 40 in plingeling) +, dontExportDirectReusedClauses(s.dontExportDirectReusedClauses) +, nbNotExportedBecauseDirectlyReused(s.nbNotExportedBecauseDirectlyReused) +{ + s.goodImportsFromThreads.memCopyTo(goodImportsFromThreads); + useUnaryWatched = s.useUnaryWatched; +} + + +// Strategy to reduce unary watches list +struct reduceDB_oneWatched_lt { + ClauseAllocator& ca; + + reduceDB_oneWatched_lt(ClauseAllocator& ca_) : ca(ca_) { + } + + bool operator()(CRef x, CRef y) { + + // Main criteria... Like in MiniSat we keep all binary clauses + if (ca[x].size() > 2 && ca[y].size() == 2) return 1; + + if (ca[y].size() > 2 && ca[x].size() == 2) return 0; + if (ca[x].size() == 2 && ca[y].size() == 2) return 0; + + // Second one based on literal block distance + if (ca[x].size() > ca[y].size()) return 1; + if (ca[x].size() < ca[y].size()) return 0; + + if (ca[x].lbd() > ca[y].lbd()) return 1; + if (ca[x].lbd() < ca[y].lbd()) return 0; + + // Finally we can use old activity or size, we choose the last one + 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()); } + } +}; + +// @overide +void ParallelSolver::reduceDB() { + + int i, j; + nbReduceDB++; + sort(learnts, reduceDB_lt(ca)); + + int limit; + + if (!panicModeIsEnabled()) { + // We have a lot of "good" clauses, it is difficult to compare them. Keep more ! + if (ca[learnts[learnts.size() / RATIOREMOVECLAUSES]].lbd() <= 3) nbclausesbeforereduce += specialIncReduceDB; + // Useless :-) + if (ca[learnts.last()].lbd() <= 5) nbclausesbeforereduce += specialIncReduceDB; + + // Don't delete binary or locked clauses. From the rest, delete clauses from the first half + // Keep clauses which seem to be usefull (their lbd was reduce during this sequence) + + limit = learnts.size() / 2; + } else { + limit = panicModeLastRemoved; + } + panicModeLastRemoved = 0; + + uint64_t sumsize = 0; + for (i = j = 0; i < learnts.size(); i++) { + + Clause& c = ca[learnts[i]]; + if (i == learnts.size() / 2) + goodlimitlbd = c.lbd(); + sumsize += c.size(); + if (c.lbd() > 2 && c.size() > 2 && c.canBeDel() && !locked(c) && (i < limit)) { + removeClause(learnts[i]); + nbRemovedClauses++; + panicModeLastRemoved++; + } else { + if (!c.canBeDel()) limit++; //we keep c, so we can delete an other clause + c.setCanBeDel(true); // At the next step, c can be delete + learnts[j++] = learnts[i]; + } + } + learnts.shrink(i - j); + + if (learnts.size() > 0) + goodlimitsize = 1 + (double) sumsize / (double) learnts.size(); + + // Special treatment for imported clauses + if (!panicModeIsEnabled()) + limit = unaryWatchedClauses.size() - (learnts.size() * 2); + else + limit = panicModeLastRemovedShared; + panicModeLastRemovedShared = 0; + if ((unaryWatchedClauses.size() > 100) && (limit > 0)) { + + sort(unaryWatchedClauses, reduceDB_oneWatched_lt(ca)); + + for (i = j = 0; i < unaryWatchedClauses.size(); i++) { + Clause& c = ca[unaryWatchedClauses[i]]; + if (c.lbd() > 2 && c.size() > 2 && c.canBeDel() && !locked(c) && (i < limit)) { + removeClause(unaryWatchedClauses[i], c.getOneWatched()); // remove from the purgatory (or not) + nbRemovedUnaryWatchedClauses++; + panicModeLastRemovedShared++; + } else { + if (!c.canBeDel()) limit++; //we keep c, so we can delete an other clause + c.setCanBeDel(true); // At the next step, c can be delete + unaryWatchedClauses[j++] = unaryWatchedClauses[i]; + } + } + unaryWatchedClauses.shrink(i - j); + } + + checkGarbage(); +} + + +/*_________________________________________________________________________________________________ +| +| parallelImportClauseDuringConflictAnalysis : (Clause &c,CRef confl) -> [void] +| +| Description: +| Verify if the clause using during conflict analysis is good for export +| @see : analyze +| Output: +|________________________________________________________________________________________________@*/ + + +void ParallelSolver::parallelImportClauseDuringConflictAnalysis(Clause &c,CRef confl) { + if (dontExportDirectReusedClauses && (confl == lastLearntClause) && (c.getExported() < 2)) { // Experimental stuff + c.setExported(2); + nbNotExportedBecauseDirectlyReused++; + } else if (shareAfterProbation && c.getExported() != 2 && conflicts > firstSharing) { + c.setExported(c.getExported() + 1); + if (!c.wasImported() && c.getExported() == 2) { // It's a new interesting clause: + if (c.lbd() == 2 || (c.size() < goodlimitsize && c.lbd() <= goodlimitlbd)) { + shareClause(c); + } + } + } + +} + + + +// These Two functions are useless here !! +void ParallelSolver::reportProgress() { + printf("c | %2d | %6d | %10d | %10d | %8d | %8d | %8d | %8d | %8d | %6.3f |\n",(int)thn,(int)starts,(int)decisions,(int)conflicts,(int)originalClausesSeen,(int)learnts.size(),(int)nbexported,(int)nbimported,(int)nbPromoted,progressEstimate()*100); + + //printf("c thread=%d confl=%lld starts=%llu reduceDB=%llu learnts=%d broadcast=%llu blockedReuse=%lld imported=%llu promoted=%llu limitlbd=%llu limitsize=%llu\n", thn, conflicts, starts, nbReduceDB, learnts.size(), nbexported, nbNotExportedBecauseDirectlyReused, nbimported, nbPromoted, goodlimitlbd, goodlimitsize); +} + +void ParallelSolver::reportProgressArrayImports(vec &totalColumns) { + return ; // TODO : does not currently work + unsigned int totalImports = 0; + printf("c %3d | ", thn); + for (int i = 0; i < sharedcomp->nbThreads; i++) { + totalImports += goodImportsFromThreads[i]; + totalColumns[i] += goodImportsFromThreads[i]; + printf(" %8d", goodImportsFromThreads[i]); + } + printf(" | %8d\n", totalImports); + +} + + + +/*_________________________________________________________________________________________________ +| +| shareClause : (Clause &c) -> [bool] +| +| Description: +| share a clause to other cores +| @see : analyze +| Output: true if the clause is indeed sent +|________________________________________________________________________________________________@*/ + +bool ParallelSolver::shareClause(Clause & c) { + bool sent = sharedcomp->addLearnt(this, c); + if (sent) + nbexported++; + return sent; +} + +/*_________________________________________________________________________________________________ +| +| panicModeIsEnabled : () -> [bool] +| +| Description: +| is panic mode (save memory) is enabled ? +|________________________________________________________________________________________________@*/ + +bool ParallelSolver::panicModeIsEnabled() { + return sharedcomp->panicMode; +} + +/*_________________________________________________________________________________________________ +| +| parallelImportUnaryClauses : () -> [void] +| +| Description: +| import all unary clauses from other cores +|________________________________________________________________________________________________@*/ + +void ParallelSolver::parallelImportUnaryClauses() { + Lit l; + while ((l = sharedcomp->getUnary(this)) != lit_Undef) { + if (value(var(l)) == l_Undef) { + uncheckedEnqueue(l); + nbimportedunit++; + } + } +} + +/*_________________________________________________________________________________________________ +| +| parallelImportClauses : () -> [bool] +| +| Description: +| import all clauses from other cores +| Output : if there is a final conflict +|________________________________________________________________________________________________@*/ + +bool ParallelSolver::parallelImportClauses() { + + assert(decisionLevel() == 0); + int importedFromThread; + while (sharedcomp->getNewClause(this, importedFromThread, importedClause)) { + assert(importedFromThread <= sharedcomp->nbThreads); + assert(importedFromThread >= 0); + + assert(importedFromThread != thn); + + if (importedClause.size() == 0) + return true; + + //printf("Thread %d imports clause from thread %d\n", threadNumber(), importedFromThread); + CRef cr = ca.alloc(importedClause, true, true); + ca[cr].setLBD(importedClause.size()); + if (plingeling) // 0 means a broadcasted clause (good clause), 1 means a survivor clause, broadcasted + ca[cr].setExported(2); // A broadcasted clause (or a survivor clause) do not share it anymore + else { + ca[cr].setExported(1); // next time we see it in analyze, we share it (follow route / broadcast depending on the global strategy, part of an ongoing experimental stuff: a clause in one Watched will be set to exported 2 when promotted. + } + ca[cr].setImportedFrom(importedFromThread); + unaryWatchedClauses.push(cr); + if (plingeling || ca[cr].size() <= 2) {//|| importedRoute == 0) { // importedRoute == 0 means a glue clause in another thread (or any very good clause) + ca[cr].setOneWatched(false); // Warning: those clauses will never be promoted by a conflict clause (or rarely: they are propagated!) + attachClause(cr); + nbImportedGoodClauses++; + } else { + ca[cr].setOneWatched(true); + attachClausePurgatory(cr); // + nbimportedInPurgatory++; + } + assert(ca[cr].learnt()); + nbimported++; + } + return false; +} + + +/*_________________________________________________________________________________________________ +| +| parallelExportUnaryClause : (Lit p) -> [void] +| +| Description: +| export unary clauses to other cores +|________________________________________________________________________________________________@*/ + +void ParallelSolver::parallelExportUnaryClause(Lit p) { + // Multithread + sharedcomp->addLearnt(this,p ); // TODO: there can be a contradiction here (two theads proving a and -a) + nbexportedunit++; +} + + +/*_________________________________________________________________________________________________ +| +| parallelExportClauseDuringSearch : (Clause &c) -> [void] +| +| Description: +| Verify if a new learnt clause is useful for export +| @see search +| +|________________________________________________________________________________________________@*/ + +void ParallelSolver::parallelExportClauseDuringSearch(Clause &c) { + // + // Multithread + // Now I'm sharing the clause if seen in at least two conflicts analysis shareClause(ca[cr]); + if ((plingeling && !shareAfterProbation && c.lbd() < 8 && c.size() < 40) || + (c.lbd() <= 2)) { // For this class of clauses, I'm sharing them asap (they are Glue CLauses, no probation for them) + shareClause(c); + c.setExported(2); + } + +} + + +/*_________________________________________________________________________________________________ +| +| parallelJobIsFinished : () -> [bool] +| +| Description: +| Is a core already finish the search +| +|________________________________________________________________________________________________@*/ + +bool ParallelSolver::parallelJobIsFinished() { + // Parallel: another job has finished let's quit + return (sharedcomp->jobFinished()); +} + +// @overide +lbool ParallelSolver::solve_(bool do_simp, bool turn_off_simp) { + vec extra_frozen; + lbool result = l_True; + do_simp &= use_simplification; + if (do_simp){ + // Assumptions must be temporarily frozen to run variable elimination: + for (int i = 0; i < assumptions.size(); i++){ + Var v = var(assumptions[i]); + + // If an assumption has been eliminated, remember it. + assert(!isEliminated(v)); + + if (!frozen[v]){ + // Freeze and store. + setFrozen(v, true); + extra_frozen.push(v); + } } + + result = lbool(eliminate(turn_off_simp)); + } + + model.clear(); + conflict.clear(); + if (!ok) return l_False; + + solves++; + + + lbool status = l_Undef; + + // Search: + int curr_restarts = 0; + while (status == l_Undef && !sharedcomp->jobFinished()) { + status = search(0); // the parameter is useless in glucose, kept to allow modifications + if (!withinBudget()) break; + curr_restarts++; + } + + if (verbosity >= 1) + printf("c =========================================================================================================\n"); + + +/* if (do_simp) + // Unfreeze the assumptions that were frozen: + for (int i = 0; i < extra_frozen.size(); i++) + setFrozen(extra_frozen[i], false); +*/ + + bool firstToFinish = false; + if (status != l_Undef) + firstToFinish = sharedcomp->IFinished(this); + if (firstToFinish) { + printf("c Thread %d is 100%% pure glucose! First thread to finish! (%s answer).\n", threadNumber(), status == l_True ? "SAT" : status == l_False ? "UNSAT" : "UNKOWN"); + sharedcomp->jobStatus = status; + } + + if (firstToFinish && status == l_True) { + extendModel(); + + + // Extend & copy model: + model.growTo(nVars()); + for (int i = 0; i < nVars(); i++) model[i] = value(i); + } else if (status == l_False && conflict.size() == 0) + ok = false; + + + pthread_cond_signal(pcfinished); + + //cancelUntil(0); + + + return status; + +} diff --git a/parallel/ParallelSolver.h b/parallel/ParallelSolver.h new file mode 100644 index 0000000..9701792 --- /dev/null +++ b/parallel/ParallelSolver.h @@ -0,0 +1,144 @@ +/**************************************************************************************[ParallelSolver.h] + Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + LRI - Univ. Paris Sud, France (2009-2013) + Labri - Univ. Bordeaux, France + + Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + 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 +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 +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 +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). + + +--------------- Original Minisat Copyrights + +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. + **************************************************************************************************/ + +#ifndef PARALLELSOLVER_H +#define PARALLELSOLVER_H + +#include "core/SolverTypes.h" +#include "core/Solver.h" +#include "simp/SimpSolver.h" +#include "parallel/SharedCompanion.h" +namespace Glucose { +//================================================================================================= + //class MultiSolvers; + //class SolverCompanion; + // class MultiSolvers; + +class ParallelSolver : public SimpSolver { + friend class MultiSolvers; + friend class SolverCompanion; + friend class SharedCompanion; +// friend class ReasoningCompanion; +// friend class SolverConfiguration; + +protected : + // Multithread : + int thn; // internal thread number + //MultiSolvers* belongsto; // Not working (due to incomplete types) + SharedCompanion *sharedcomp; + bool coreFUIP; // true if one core is specialized for branching on all FUIP + bool ImTheSolverFUIP; + pthread_mutex_t *pmfinished; // mutex on which main process may wait for... As soon as one process finishes it release the mutex + pthread_cond_t *pcfinished; // condition variable that says that a thread as finished + +public: + // Constructor/Destructor: + // + ParallelSolver(int threadId); + ParallelSolver(const ParallelSolver &s); + ~ParallelSolver(); + + /** + * Clone function + */ + virtual Clone* clone() const { + return new ParallelSolver(*this); + } + + int threadNumber () const; + void setThreadNumber (int i); + void reportProgress(); + void reportProgressArrayImports(vec &totalColumns); + virtual void reduceDB(); + virtual lbool solve_ (bool do_simp = true, bool turn_off_simp = false); + + vec importedClause; // Temporary clause used to copy each imported clause + uint64_t nbexported; + uint64_t nbimported; + uint64_t nbexportedunit, nbimportedunit , nbimportedInPurgatory, nbImportedGoodClauses; + unsigned int goodlimitlbd; // LBD score of the "good" clauses, locally + int goodlimitsize; + bool purgatory; // mode of operation + bool shareAfterProbation; // Share any none glue clause only after probation (seen 2 times in conflict analysis) + bool plingeling; // plingeling strategy for sharing clauses (experimental) + + // Stats front end + uint64_t getNbExported() { return nbexported;} + uint64_t getNbImported() { return nbimported;} + uint64_t getNbExportedUnit() {return nbexportedunit;} + + uint32_t firstSharing, limitSharingByGoodLBD, limitSharingByFixedLimitLBD, limitSharingByFixedLimitSize; + uint32_t probationByFollowingRoads, probationByFriend; + uint32_t survivorLayers; // Number of layers for a common clause to survive + bool dontExportDirectReusedClauses ; // When true, directly reused clauses are not exported + uint64_t nbNotExportedBecauseDirectlyReused; + + + vec goodImportsFromThreads; // Stats of good importations from other threads + + virtual void parallelImportClauseDuringConflictAnalysis(Clause &c,CRef confl); + virtual bool parallelImportClauses(); // true if the empty clause was received + virtual void parallelImportUnaryClauses(); + virtual void parallelExportUnaryClause(Lit p); + virtual void parallelExportClauseDuringSearch(Clause &c); + virtual bool parallelJobIsFinished(); + virtual bool panicModeIsEnabled(); + + bool shareClause(Clause & c); // true if the clause was succesfully sent + + + +}; + + + inline int ParallelSolver::threadNumber () const {return thn;} + inline void ParallelSolver::setThreadNumber (int i) {thn = i;} +} +#endif /* PARALLELSOLVER_H */ + diff --git a/parallel/SharedCompanion.cc b/parallel/SharedCompanion.cc new file mode 100644 index 0000000..dadc672 --- /dev/null +++ b/parallel/SharedCompanion.cc @@ -0,0 +1,167 @@ +/***************************************************************************************[SharedCompanion.cc] + Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + LRI - Univ. Paris Sud, France (2009-2013) + Labri - Univ. Bordeaux, France + + Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + 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 +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 +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 +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). + + +--------------- Original Minisat Copyrights + +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 "core/Solver.h" +#include "parallel/ParallelSolver.h" +#include "core/SolverTypes.h" +#include "parallel/ClausesBuffer.h" +#include "parallel/SharedCompanion.h" + + +using namespace Glucose; + +SharedCompanion::SharedCompanion(int _nbThreads) : + nbThreads(_nbThreads), + bjobFinished(false), + jobFinishedBy(NULL), + panicMode(false), // The bug in the SAT2014 competition :) + jobStatus(l_Undef), + random_seed(9164825) { + + pthread_mutex_init(&mutexSharedClauseCompanion,NULL); // This is the shared companion lock + pthread_mutex_init(&mutexSharedUnitCompanion,NULL); // This is the shared companion lock + pthread_mutex_init(&mutexSharedCompanion,NULL); // This is the shared companion lock + pthread_mutex_init(&mutexJobFinished,NULL); // This is the shared companion lock + if (_nbThreads> 0) { + setNbThreads(_nbThreads); + fprintf(stdout,"c Shared companion initialized: handling of clauses of %d threads.\nc %d ints for the sharing clause buffer (not expandable) .\n", _nbThreads, clausesBuffer.maxSize()); + } + +} + +void SharedCompanion::setNbThreads(int _nbThreads) { + nbThreads = _nbThreads; + clausesBuffer.setNbThreads(_nbThreads); +} + +void SharedCompanion::printStats() { +} + +// No multithread safe +bool SharedCompanion::addSolver(ParallelSolver* s) { + watchedSolvers.push(s); + pthread_mutex_t* mu = (pthread_mutex_t*)malloc(sizeof(pthread_mutex_t)); + pthread_mutex_init(mu,NULL); + assert(s->thn == watchedSolvers.size()-1); // all solvers must have been registered in the good order + nextUnit.push(0); + + return true; +} +void SharedCompanion::newVar(bool sign) { + isUnary .push(l_Undef); +} + +void SharedCompanion::addLearnt(ParallelSolver *s,Lit unary) { + pthread_mutex_lock(&mutexSharedUnitCompanion); + if (isUnary[var(unary)]==l_Undef) { + unitLit.push(unary); + isUnary[var(unary)] = sign(unary)?l_False:l_True; + } + pthread_mutex_unlock(&mutexSharedUnitCompanion); +} + +Lit SharedCompanion::getUnary(ParallelSolver *s) { + int sn = s->thn; + Lit ret = lit_Undef; + + pthread_mutex_lock(&mutexSharedUnitCompanion); + if (nextUnit[sn] < unitLit.size()) + ret = unitLit[nextUnit[sn]++]; + pthread_mutex_unlock(&mutexSharedUnitCompanion); + return ret; +} + +// Specialized functions for this companion +// must be multithread safe +// Add a clause to the threads-wide clause database (all clauses, through) +bool SharedCompanion::addLearnt(ParallelSolver *s, Clause & c) { + int sn = s->thn; // thread number of the solver + bool ret = false; + assert(watchedSolvers.size()>sn); + + pthread_mutex_lock(&mutexSharedClauseCompanion); + ret = clausesBuffer.pushClause(sn, c); + pthread_mutex_unlock(&mutexSharedClauseCompanion); + return ret; +} + + +bool SharedCompanion::getNewClause(ParallelSolver *s, int & threadOrigin, vec& newclause) { // gets a new interesting clause for solver s + int sn = s->thn; + + // First, let's get the clauses on the big blackboard + pthread_mutex_lock(&mutexSharedClauseCompanion); + bool b = clausesBuffer.getClause(sn, threadOrigin, newclause); + pthread_mutex_unlock(&mutexSharedClauseCompanion); + + return b; +} + +bool SharedCompanion::jobFinished() { + bool ret = false; + pthread_mutex_lock(&mutexJobFinished); + ret = bjobFinished; + pthread_mutex_unlock(&mutexJobFinished); + return ret; +} + +bool SharedCompanion::IFinished(ParallelSolver *s) { + bool ret = false; + pthread_mutex_lock(&mutexJobFinished); + if (!bjobFinished) { + ret = true; + bjobFinished = true; + jobFinishedBy = s; + } + pthread_mutex_unlock(&mutexJobFinished); + return ret; +} + + + diff --git a/parallel/SharedCompanion.h b/parallel/SharedCompanion.h new file mode 100644 index 0000000..9ab3461 --- /dev/null +++ b/parallel/SharedCompanion.h @@ -0,0 +1,122 @@ +/***************************************************************************************[SharedCompanion.h] + Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + LRI - Univ. Paris Sud, France (2009-2013) + Labri - Univ. Bordeaux, France + + Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + 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 +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 +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 +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). + + +--------------- Original Minisat Copyrights + +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. + **************************************************************************************************/ + +/* This class is responsible for protecting (by mutex) information exchange between threads. + * It also allows each solver to send / receive clause / unary clauses. + * + * Only one sharedCompanion is created for all the solvers + */ + + +#ifndef SharedCompanion_h +#define SharedCompanion_h +#include "core/SolverTypes.h" +#include "parallel/ParallelSolver.h" +#include "parallel/SolverCompanion.h" +#include "parallel/ClausesBuffer.h" + +namespace Glucose { + + +class SharedCompanion : public SolverCompanion { + friend class MultiSolvers; + friend class ParallelSolver; +public: + SharedCompanion(int nbThreads=0); + void setNbThreads(int _nbThreads); // Sets the number of threads (cannot by changed once the solver is running) + void newVar(bool sign); // Adds a var (used to keep track of unary variables) + void printStats(); // Printing statistics of all solvers + + bool jobFinished(); // True if the job is over + bool IFinished(ParallelSolver *s); // returns true if you are the first solver to finish + bool addSolver(ParallelSolver*); // attach a solver to accompany + void addLearnt(ParallelSolver *s,Lit unary); // Add a unary clause to share + bool addLearnt(ParallelSolver *s, Clause & c); // Add a clause to the shared companion, as a database manager + + bool getNewClause(ParallelSolver *s, int &th, vec & nc); // gets a new interesting clause for solver s + Lit getUnary(ParallelSolver *s); // Gets a new unary literal + inline ParallelSolver* winner(){return jobFinishedBy;} // Gets the first solver that called IFinished() + + protected: + + ClausesBuffer clausesBuffer; // A big blackboard for all threads sharing non unary clauses + int nbThreads; // Number of threads + + // A set of mutex variables + pthread_mutex_t mutexSharedCompanion; // mutex for any high level sync between all threads (like reportf) + pthread_mutex_t mutexSharedClauseCompanion; // mutex for reading/writing clauses on the blackboard + pthread_mutex_t mutexSharedUnitCompanion; // mutex for reading/writing unit clauses on the blackboard + pthread_mutex_t mutexJobFinished; + + bool bjobFinished; + ParallelSolver *jobFinishedBy; + bool panicMode; // panicMode means no more increasing space needed + lbool jobStatus; // globale status of the job + + // Shared clauses are a queue of lits... + // friend class wholearnt; + vec nextUnit; // indice of next unit clause to retrieve for solver number i + vec unitLit; // Set of unit literals found so far + vec isUnary; // sign of the unary var (if proved, or l_Undef if not) + double random_seed; + + // Returns a random float 0 <= x < 1. Seed must never be 0. + static inline double drand(double& seed) { + seed *= 1389796; + int q = (int)(seed / 2147483647); + seed -= (double)q * 2147483647; + return seed / 2147483647; } + + // 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); } + +}; +} +#endif diff --git a/parallel/SolverCompanion.cc b/parallel/SolverCompanion.cc new file mode 100644 index 0000000..8cd5c51 --- /dev/null +++ b/parallel/SolverCompanion.cc @@ -0,0 +1,87 @@ +/***************************************************************************************[SolverCompanion.cc] + Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + LRI - Univ. Paris Sud, France (2009-2013) + Labri - Univ. Bordeaux, France + + Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + 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 +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 +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 +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). + + +--------------- Original Minisat Copyrights + +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. + **************************************************************************************************/ + +/* This class is a general companion for a solver. + * The idea is to be able to have different kind of companions: + * - SharedCompanion that shares clauses between threads + * - NetworkCompanion (Not in this version) that sends clauses over the network + * + * The implementaton is trivial. Just keep track of watched Solvers by the companion. + **/ + +#include "parallel/SolverCompanion.h" + +using namespace Glucose; + +SolverCompanion::SolverCompanion() +{} + +SolverCompanion::~SolverCompanion() +{} + + +bool SolverCompanion::addSolver(ParallelSolver* s) { + watchedSolvers.push(s); + return true; +} + +int SolverCompanion::runOnceCompanion() { + int errcode = 0; + for(int indexSolver = 0; indexSolver watchedSolvers; +}; +} +#endif + diff --git a/parallel/SolverConfiguration.cc b/parallel/SolverConfiguration.cc new file mode 100644 index 0000000..48127c2 --- /dev/null +++ b/parallel/SolverConfiguration.cc @@ -0,0 +1,131 @@ +/***************************************************************************************[SolverConfiguration.cc] + Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + LRI - Univ. Paris Sud, France (2009-2013) + Labri - Univ. Bordeaux, France + + Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + 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 +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 +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 +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). + + +--------------- Original Minisat Copyrights + +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 "parallel/MultiSolvers.h" +#include "core/Solver.h" +//#include "parallel/ParallelSolver.h" +#include "parallel/SolverConfiguration.h" + +using namespace Glucose; + + void SolverConfiguration::configure(MultiSolvers *ms, int nbsolvers) { + + if (nbsolvers < 2 ) return; + + ms->solvers[1]->var_decay = 0.94; + ms->solvers[1]->max_var_decay = 0.96; + ms->solvers[1]->firstReduceDB=600; + + if (nbsolvers < 3 ) return; + + ms->solvers[2]->var_decay = 0.90; + ms->solvers[2]->max_var_decay = 0.97; + ms->solvers[2]->firstReduceDB=500; + + if (nbsolvers < 4 ) return; + + ms->solvers[3]->var_decay = 0.85; + ms->solvers[3]->max_var_decay = 0.93; + ms->solvers[3]->firstReduceDB=400; + + if (nbsolvers < 5 ) return; + + // Glucose 2.0 (+ blocked restarts) + ms->solvers[4]->var_decay = 0.95; + ms->solvers[4]->max_var_decay = 0.95; + ms->solvers[4]->firstReduceDB=4000; + ms->solvers[4]->lbdQueue.growTo(100); + ms->solvers[4]->sizeLBDQueue = 100; + ms->solvers[4]->K = 0.7; + ms->solvers[4]->incReduceDB = 500; + + if (nbsolvers < 6 ) return; + + ms->solvers[5]->var_decay = 0.93; + ms->solvers[5]->max_var_decay = 0.96; + ms->solvers[5]->firstReduceDB=100; + ms->solvers[5]->incReduceDB = 500; + + if (nbsolvers < 7 ) return; + + ms->solvers[6]->var_decay = 0.75; + ms->solvers[6]->max_var_decay = 0.94; + ms->solvers[6]->firstReduceDB=2000; + + if (nbsolvers < 8 ) return; + + ms->solvers[7]->var_decay = 0.94; + ms->solvers[7]->max_var_decay = 0.96; + ms->solvers[7]->firstReduceDB=800; + + if (nbsolvers < 9) return; + + ms->solvers[8]->reduceOnSize = true; + + if (nbsolvers < 10 ) return; + + ms->solvers[9]->reduceOnSize = true; + ms->solvers[9]->reduceOnSizeSize = 14; + + if (nbsolvers < 11 ) return; + + double noisevar_decay = 0.005; + int noiseReduceDB = 50; + for (int i=10;isolvers[i]-> var_decay = ms->solvers[i%8]->var_decay; + ms->solvers[i]-> max_var_decay = ms->solvers[i%8]->max_var_decay; + ms->solvers[i]-> firstReduceDB= ms->solvers[i%8]->firstReduceDB; + ms->solvers[i]->var_decay += noisevar_decay; + ms->solvers[i]->firstReduceDB+=noiseReduceDB; + if ((i+1) % 8 == 0) { + noisevar_decay += 0.006; + noiseReduceDB += 25; + } + } + } diff --git a/parallel/SolverConfiguration.h b/parallel/SolverConfiguration.h new file mode 100644 index 0000000..475ec72 --- /dev/null +++ b/parallel/SolverConfiguration.h @@ -0,0 +1,68 @@ +/***************************************************************************************[SolverConfiguration.h] + Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + LRI - Univ. Paris Sud, France (2009-2013) + Labri - Univ. Bordeaux, France + + Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + 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 +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 +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 +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). + + +--------------- Original Minisat Copyrights + +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. + **************************************************************************************************/ + + +#ifndef SolverConfiguration_h +#define SolverConfiguration_h + + + +namespace Glucose { + +class MultiSolvers; + +class SolverConfiguration { + +public : + static void configure(MultiSolvers *ms, int nbsolvers); + +}; + +} +#endif diff --git a/simp/Main.cc b/simp/Main.cc index 8aa30b6..ca3bf42 100644 --- a/simp/Main.cc +++ b/simp/Main.cc @@ -1,12 +1,32 @@ -/*****************************************************************************************[Main.cc] - Glucose -- Copyright (c) 2009, Gilles Audemard, Laurent Simon - CRIL - Univ. Artois, France - LRI - Univ. Paris Sud, France - +/***************************************************************************************[Main.cc] + Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + LRI - Univ. Paris Sud, France (2009-2013) + Labri - Univ. Bordeaux, France + + Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + Labri - Univ. Bordeaux, 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). +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 +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 +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). + + +--------------- Original Minisat Copyrights Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson Copyright (c) 2007-2010, Niklas Sorensson @@ -25,7 +45,7 @@ NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPO 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 @@ -43,25 +63,26 @@ using namespace Glucose; //================================================================================================= +static const char* _certified = "CORE -- CERTIFIED UNSAT"; 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); + 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 : %" PRIu64"\n", solver.nbReduceDB); + printf("c nb removed Clauses : %" PRIu64"\n",solver.nbRemovedClauses); + printf("c nb learnts DL2 : %" PRIu64"\n", solver.nbDL2); + printf("c nb learnts size 2 : %" PRIu64"\n", solver.nbBin); + printf("c nb learnts size 1 : %" PRIu64"\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 : %" PRIu64"\n",solver.nbReducedClauses); if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used); printf("c CPU time : %g s\n", cpu_time); @@ -91,7 +112,8 @@ static void SIGINT_exit(int signum) { int main(int argc, char** argv) { try { - printf("c\nc This is glucose 3.0 -- based on MiniSAT (Many thanks to MiniSAT team)\nc Simplification mode is turned on\nc\n"); + printf("c\nc This is glucose 4.0 -- 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"); @@ -99,7 +121,7 @@ int main(int argc, char** argv) #if defined(__linux__) fpu_control_t oldcw, newcw; _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw); - printf("WARNING: for repeatability, setting FPU to use double precision\n"); + //printf("c WARNING: for repeatability, setting FPU to use double precision\n"); #endif // Extra options: // @@ -110,24 +132,40 @@ int main(int argc, char** argv) StringOption dimacs ("MAIN", "dimacs", "If given, stop after preprocessing and write the result to this file."); 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)); + // BoolOption opt_incremental ("MAIN","incremental", "Use incremental SAT solving",false); + BoolOption opt_certified (_certified, "certified", "Certified UNSAT using DRUP format", false); + StringOption opt_certified_file (_certified, "certified-output", "Certified UNSAT output file", "NULL"); + parseOptions(argc, argv, true); SimpSolver S; double initial_time = cpuTime(); S.parsing = 1; - if (!pre) S.eliminate(true); + //if (!pre) S.eliminate(true); S.verbosity = verb; S.verbEveryConflicts = vv; S.showModel = mod; + + S.certifiedUNSAT = opt_certified; + if(S.certifiedUNSAT) { + if(!strcmp(opt_certified_file,"NULL")) { + S.certifiedOutput = fopen("/dev/stdout", "wb"); + } else { + S.certifiedOutput = fopen(opt_certified_file, "wb"); + } + fprintf(S.certifiedOutput,"o proof DRUP\n"); + } + 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; @@ -135,7 +173,7 @@ int main(int argc, char** argv) 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("WARNING! Could not set resource limit: CPU-time.\n"); + printf("c WARNING! Could not set resource limit: CPU-time.\n"); } } // Set limit on virtual memory: @@ -146,11 +184,11 @@ int main(int argc, char** argv) 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("WARNING! Could not set resource limit: Virtual memory.\n"); + printf("c WARNING! Could not set resource limit: Virtual memory.\n"); } } if (argc == 1) - printf("Reading from standard input... Use '--help' for help.\n"); + 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) @@ -179,12 +217,15 @@ int main(int argc, char** argv) signal(SIGXCPU,SIGINT_interrupt); S.parsing = 0; - S.eliminate(true); + if(pre/* && !S.isIncremental()*/) { + printf("c | Preprocesing is fully done\n"); + S.eliminate(true); double simplified_time = cpuTime(); if (S.verbosity > 0){ printf("c | Simplification time: %12.2f s |\n", simplified_time - parsed_time); - printf("c | |\n"); } - + } + } + printf("c | |\n"); if (!S.okay()){ if (S.certifiedUNSAT) fprintf(S.certifiedOutput, "0\n"), fclose(S.certifiedOutput); if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res); @@ -193,7 +234,7 @@ int main(int argc, char** argv) printf("Solved by simplification\n"); printStats(S); printf("\n"); } - printf("s UNSATISFIABLE\n"); + printf("s UNSATISFIABLE\n"); exit(20); } @@ -223,7 +264,7 @@ int main(int argc, char** argv) fprintf(res, " 0\n"); } else { if (ret == l_False){ - fprintf(res, "UNSAT\n"), fclose(res); + fprintf(res, "UNSAT\n"); } } fclose(res); @@ -238,6 +279,8 @@ int main(int argc, char** argv) } + if (S.certifiedUNSAT) fprintf(S.certifiedOutput, "0\n"), fclose(S.certifiedOutput); + #ifdef NDEBUG exit(ret == l_True ? 10 : ret == l_False ? 20 : 0); // (faster than "return", which will invoke the destructor for 'Solver') #else diff --git a/simp/SimpSolver.cc b/simp/SimpSolver.cc index 50c1362..84bc725 100644 --- a/simp/SimpSolver.cc +++ b/simp/SimpSolver.cc @@ -1,5 +1,34 @@ -/***********************************************************************************[SimpSolver.cc] -Copyright (c) 2006, Niklas Een, Niklas Sorensson +/***************************************************************************************[SimpSolver.cc] + Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + LRI - Univ. Paris Sud, France (2009-2013) + Labri - Univ. Bordeaux, France + + Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + 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 +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 +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 +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). + + +--------------- Original Minisat Copyrights + +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 @@ -16,7 +45,7 @@ NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPO 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 "mtl/Sort.h" #include "simp/SimpSolver.h" @@ -44,7 +73,8 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of SimpSolver::SimpSolver() : - grow (opt_grow) + Solver() + , grow (opt_grow) , clause_lim (opt_clause_lim) , subsumption_lim (opt_subsumption_lim) , simp_garbage_frac (opt_simp_garbage_frac) @@ -73,9 +103,54 @@ SimpSolver::~SimpSolver() } + +SimpSolver::SimpSolver(const SimpSolver &s) : Solver(s) + , grow (s.grow) + , clause_lim (s.clause_lim) + , subsumption_lim (s.subsumption_lim) + , simp_garbage_frac (s.simp_garbage_frac) + , use_asymm (s.use_asymm) + , use_rcheck (s.use_rcheck) + , use_elim (s.use_elim) + , merges (s.merges) + , asymm_lits (s.asymm_lits) + , eliminated_vars (s.eliminated_vars) + , elimorder (s.elimorder) + , use_simplification (s.use_simplification) + , occurs (ClauseDeleted(ca)) + , elim_heap (ElimLt(n_occ)) + , bwdsub_assigns (s.bwdsub_assigns) + , n_touched (s.n_touched) +{ + // TODO: Copy dummy... what is it??? + vec dummy(1,lit_Undef); + ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below. + bwdsub_tmpunit = ca.alloc(dummy); + remove_satisfied = false; + //End TODO + + + s.elimclauses.memCopyTo(elimclauses); + s.touched.memCopyTo(touched); + s.occurs.copyTo(occurs); + s.n_occ.memCopyTo(n_occ); + s.elim_heap.copyTo(elim_heap); + s.subsumption_queue.copyTo(subsumption_queue); + s.frozen.memCopyTo(frozen); + s.eliminated.memCopyTo(eliminated); + + use_simplification = s.use_simplification; + bwdsub_assigns = s.bwdsub_assigns; + n_touched = s.n_touched; + bwdsub_tmpunit = s.bwdsub_tmpunit; + qhead = s.qhead; + ok = s.ok; +} + + + Var SimpSolver::newVar(bool sign, bool dvar) { Var v = Solver::newVar(sign, dvar); - frozen .push((char)false); eliminated.push((char)false); @@ -88,13 +163,10 @@ Var SimpSolver::newVar(bool sign, bool dvar) { } return v; } - - lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) { vec extra_frozen; lbool result = l_True; - do_simp &= use_simplification; if (do_simp){ @@ -127,6 +199,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) for (int i = 0; i < extra_frozen.size(); i++) setFrozen(extra_frozen[i], false); + return result; } @@ -177,7 +250,8 @@ bool SimpSolver::addClause_(vec& ps) } -void SimpSolver::removeClause(CRef cr) + +void SimpSolver::removeClause(CRef cr,bool inPurgatory) { const Clause& c = ca[cr]; @@ -188,7 +262,7 @@ void SimpSolver::removeClause(CRef cr) occurs.smudge(var(c[i])); } - Solver::removeClause(cr); + Solver::removeClause(cr,inPurgatory); } @@ -586,6 +660,8 @@ void SimpSolver::extendModel() int i, j; Lit x; + if(model.size()==0) model.growTo(nVars()); + for (i = elimclauses.size()-1; i > 0; i -= j){ for (j = elimclauses[i--]; j > 1; j--, i--) if (modelValue(toLit(elimclauses[i])) != l_False) @@ -600,8 +676,10 @@ void SimpSolver::extendModel() bool SimpSolver::eliminate(bool turn_off_elim) { - if (!simplify()) + if (!simplify()) { + ok = false; return false; + } else if (!use_simplification) return true; @@ -682,11 +760,14 @@ bool SimpSolver::eliminate(bool turn_off_elim) checkGarbage(); } - if (verbosity >= 1 && elimclauses.size() > 0) + if (verbosity >= 0 && elimclauses.size() > 0) printf("c | Eliminated clauses: %10.2f Mb |\n", double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024)); + return ok; + + } diff --git a/simp/SimpSolver.h b/simp/SimpSolver.h index ff692c3..5f457a8 100644 --- a/simp/SimpSolver.h +++ b/simp/SimpSolver.h @@ -1,5 +1,34 @@ -/************************************************************************************[SimpSolver.h] -Copyright (c) 2006, Niklas Een, Niklas Sorensson +/***************************************************************************************[SimpSolver.h] + Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + LRI - Univ. Paris Sud, France (2009-2013) + Labri - Univ. Bordeaux, France + + Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + 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 +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 +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 +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). + + +--------------- Original Minisat Copyrights + +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 @@ -16,14 +45,14 @@ NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPO 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. -**************************************************************************************************/ + **************************************************************************************************/ #ifndef Glucose_SimpSolver_h #define Glucose_SimpSolver_h #include "mtl/Queue.h" #include "core/Solver.h" - +#include "mtl/Clone.h" namespace Glucose { @@ -36,16 +65,27 @@ class SimpSolver : public Solver { // SimpSolver(); ~SimpSolver(); - + + SimpSolver(const SimpSolver &s); + + + /** + * Clone function + */ + virtual Clone* clone() const { + return new SimpSolver(*this); + } + + // Problem specification: // - Var newVar (bool polarity = true, bool dvar = true); + virtual Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode. bool addClause (const vec& ps); bool addEmptyClause(); // Add the empty 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. - bool addClause_( vec& ps); + virtual bool addClause_( vec& ps); bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction). // Variable mode: @@ -90,7 +130,6 @@ class SimpSolver : public Solver { bool use_asymm; // Shrink clauses by asymmetric branching. bool use_rcheck; // Check if a clause is already implied. Prett costly, and subsumes subsumptions :) bool use_elim; // Perform variable elimination. - // Statistics: // int merges; @@ -144,7 +183,7 @@ class SimpSolver : public Solver { // Main internal methods: // - lbool solve_ (bool do_simp = true, bool turn_off_simp = false); + virtual lbool solve_ (bool do_simp = true, bool turn_off_simp = false); bool asymm (Var v, CRef cr); bool asymmVar (Var v); void updateElimHeap (Var v); @@ -155,11 +194,11 @@ class SimpSolver : public Solver { bool eliminateVar (Var v); void extendModel (); - void removeClause (CRef cr); + void removeClause (CRef cr,bool inPurgatory=false); bool strengthenClause (CRef cr, Lit l); void cleanUpClauses (); bool implied (const vec& c); - void relocAll (ClauseAllocator& to); + virtual void relocAll (ClauseAllocator& to); }; diff --git a/utils/Options.h b/utils/Options.h index 3570f23..a86e4c7 100644 --- a/utils/Options.h +++ b/utils/Options.h @@ -282,15 +282,15 @@ class Int64Option : public Option if (range.begin == INT64_MIN) fprintf(stderr, "imin"); else - fprintf(stderr, "%4"PRIi64, range.begin); + fprintf(stderr, "%4" PRIi64, range.begin); fprintf(stderr, " .. "); if (range.end == INT64_MAX) fprintf(stderr, "imax"); else - fprintf(stderr, "%4"PRIi64, range.end); + fprintf(stderr, "%4" PRIi64, range.end); - fprintf(stderr, "] (default: %"PRIi64")\n", value); + fprintf(stderr, "] (default: %" PRIi64")\n", value); if (verbose){ fprintf(stderr, "\n %s\n", description); fprintf(stderr, "\n"); diff --git a/utils/System.h b/utils/System.h index 4788070..4e48fee 100644 --- a/utils/System.h +++ b/utils/System.h @@ -32,6 +32,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA namespace Glucose { static inline double cpuTime(void); // CPU-time in seconds. +static inline double realTime(void); extern double memUsed(); // Memory in mega bytes (returns 0 for unsupported architectures). extern double memUsedPeak(); // Peak-memory in mega bytes (returns 0 for unsupported architectures). @@ -57,4 +58,10 @@ static inline double Glucose::cpuTime(void) { #endif +// Laurent: I know that this will not compile directly under Windows... sorry for that +static inline double Glucose::realTime() { + struct timeval tv; + gettimeofday(&tv, NULL); + return (double)tv.tv_sec + (double) tv.tv_usec / 1000000; } + #endif