glucose-syrup/parallel/MultiSolvers.h

   1 /***************************************************************************************[MultiSolvers.h]
   2  Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon
   3                                 CRIL - Univ. Artois, France
   4                                 LRI  - Univ. Paris Sud, France (2009-2013)
   5                                 Labri - Univ. Bordeaux, France
   6
   7  Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon
   8                                 CRIL - Univ. Artois, France
   9                                 Labri - Univ. Bordeaux, France
  10
  11 Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of
  12 Glucose (sources until 2013, Glucose 3.0, single core) are exactly the same as Minisat on which it
  13 is based on. (see below).
  14
  15 Glucose-Syrup sources are based on another copyright. Permissions and copyrights for the parallel
  16 version of Glucose-Syrup (the "Software") are granted, free of charge, to deal with the Software
  17 without restriction, including the rights to use, copy, modify, merge, publish, distribute,
  18 sublicence, and/or sell copies of the Software, and to permit persons to whom the Software is
  19 furnished to do so, subject to the following conditions:
  20
  21 - The above and below copyrights notices and this permission notice shall be included in all
  22 copies or substantial portions of the Software;
  23 - The parallel version of Glucose (all files modified since Glucose 3.0 releases, 2013) cannot
  24 be used in any competitive event (sat competitions/evaluations) without the express permission of
  25 the authors (Gilles Audemard / Laurent Simon). This is also the case for any competitive event
  26 using Glucose Parallel as an embedded SAT engine (single core or not).
  27
  28
  29 --------------- Original Minisat Copyrights
  30
  31 Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
  32 Copyright (c) 2007-2010, Niklas Sorensson
  33
  34 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
  35 associated documentation files (the "Software"), to deal in the Software without restriction,
  36 including without limitation the rights to use, copy, modify, merge, publish, distribute,
  37 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
  38 furnished to do so, subject to the following conditions:
  39
  40 The above copyright notice and this permission notice shall be included in all copies or
  41 substantial portions of the Software.
  42
  43 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
  44 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  45 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
  46 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
  47 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  48  **************************************************************************************************/
  49
  50 #ifndef MultiSolvers_h
  51 #define MultiSolvers_h
  52
  53 #include "parallel/ParallelSolver.h"
  54
  55 namespace Glucose {
  56     class SolverConfiguration;
  57
  58 class MultiSolvers {
  59     friend class SolverConfiguration;
  60
  61 public:
  62   MultiSolvers(ParallelSolver *s);
  63   MultiSolvers();
  64   ~MultiSolvers();
  65
  66   void printFinalStats();
  67
  68   void setVerbosity(int i);
  69   int verbosity();
  70   void setVerbEveryConflicts(int i);
  71   void setShowModel(int i) {showModel = i;}
  72   int getShowModel() {return showModel;}
  73   // Problem specification:
  74   //
  75   Var     newVar    (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
  76   bool    addClause (const vec<Lit>& ps);                           // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method!
  77   bool    addClause_(      vec<Lit>& ps);
  78
  79   bool    simplify     ();                        // Removes already satisfied clauses.
  80
  81   int     nVars      ()      const;       // The current number of variables.
  82   int     nClauses      ()      const;       // The current number of variables.
  83   ParallelSolver *getPrimarySolver();
  84
  85   void generateAllSolvers();
  86
  87   // Solving:
  88   //
  89   lbool    solve        ();                        // Search without assumptions.
  90   bool eliminate();             // Perform variable elimination
  91   void adjustParameters();
  92   void adjustNumberOfCores();
  93   void interrupt() {}
  94   vec<lbool> model;             // If problem is satisfiable, this vector contains the model (if any).
  95   inline bool okay() {
  96     if(!ok) return ok;
  97     for(int i = 0;i<solvers.size();i++) {
  98         if(!((SimpSolver*)solvers[i])->okay()) {
  99             ok = false;
 100             return false;
 101         }
 102     }
 103     return true;
 104
 105   }
 106
 107  protected:
 108         friend class ParallelSolver;
 109         friend class SolverCompanion;
 110
 111 struct Stats {
 112     uint64_t min, max, avg, std, med;
 113     Stats(uint64_t _min = 0,uint64_t _max = 0,uint64_t  _avg = 0,uint64_t  _std = 0,uint64_t  _med = 0) :
 114         min(_min), max(_max), avg(_avg), std(_std), med(_med) {}
 115 };
 116
 117         void printStats();
 118         int ok;
 119         lbool result;
 120         int maxnbthreads; // Maximal number of threads
 121         int nbthreads; // Current number of threads
 122         int nbsolvers; // Number of CDCL solvers
 123         int nbcompanions; // Number of companions
 124         int nbcompbysolver; // Number of companions by solvers
 125         bool immediateSharingGlue ;
 126         int allClonesAreBuilt;
 127         bool showModel; // show model on/off
 128
 129         int winner;
 130
 131     vec<Lit>            add_tmp;
 132
 133     double    var_decay;          // Inverse of the variable activity decay factor.                                            (default 1 / 0.95)
 134     double    clause_decay;       // Inverse of the clause activity decay factor.                                              (1 / 0.999)
 135     double    cla_inc;          // Amount to bump next clause with.
 136     double    var_inc;          // Amount to bump next variable with.
 137     double    random_var_freq;    // The frequency with which the decision heuristic tries to choose a random variable.        (default 0.02)
 138     int       restart_first;      // The initial restart limit.                                                                (default 100)
 139     double    restart_inc;        // The factor with which the restart limit is multiplied in each restart.                    (default 1.5)
 140     double    learntsize_factor;  // The intitial limit for learnt clauses is a factor of the original clauses.                (default 1 / 3)
 141     double    learntsize_inc;     // The limit for learnt clauses is multiplied with this factor each restart.                 (default 1.1)
 142     bool      expensive_ccmin;    // Controls conflict clause minimization.                                                    (default TRUE)
 143     int       polarity_mode;      // Controls which polarity the decision heuristic chooses. See enum below for allowed modes. (default polarity_false)
 144     unsigned int maxmemory;
 145     unsigned int maxnbsolvers;
 146     int verb;
 147     int verbEveryConflicts;
 148     int numvar; // Number of variables
 149     int numclauses; // Number of clauses
 150
 151     enum { polarity_true = 0, polarity_false = 1, polarity_user = 2, polarity_rnd = 3 };
 152
 153    //ClauseAllocator     ca;
 154    SharedCompanion * sharedcomp;
 155
 156     void informEnd(lbool res);
 157     ParallelSolver* retrieveSolver(int i);
 158
 159     pthread_mutex_t m; // mutex for any high level sync between all threads (like reportf)
 160     pthread_mutex_t mfinished; // mutex on which main process may wait for... As soon as one process finishes it release the mutex
 161     pthread_cond_t cfinished; // condition variable that says that a thread has finished
 162
 163     vec<ParallelSolver*> solvers; // set of plain solvers
 164     vec<SolverCompanion*> solvercompanions; // set of companion solvers
 165     vec<pthread_t*> threads; // all threads of this process
 166     vec<int> threadIndexOfSolver; // threadIndexOfSolver[solvers[i]] is the index in threads[] of the solver i
 167     vec<int> threadIndexOfSolverCompanion; // threadIndexOfSolverCompanion[solvercompanions[i]] is the index in threads[] of the solvercompanion i
 168 };
 169
 170 inline bool     MultiSolvers::addClause       (const vec<Lit>& ps)    { ps.copyTo(add_tmp); return addClause_(add_tmp); }
 171
 172 inline void MultiSolvers::setVerbosity(int i) {verb = i;}
 173 inline void MultiSolvers::setVerbEveryConflicts(int i) {verbEveryConflicts=i;}
 174 inline int      MultiSolvers::nVars         ()      const   { return numvar; }
 175 inline int      MultiSolvers::nClauses      ()      const   { return numclauses; }
 176 inline int MultiSolvers::verbosity()  {return verb;}
 177 inline ParallelSolver* MultiSolvers::getPrimarySolver() {return solvers[0];}
 178
 179
 180 }
 181 #endif
 182