1/****************************************************************************************[Solver.h] 2MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson 3 4Permission is hereby granted, free of charge, to any person obtaining a copy of this software and 5associated documentation files (the "Software"), to deal in the Software without restriction, 6including without limitation the rights to use, copy, modify, merge, publish, distribute, 7sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is 8furnished to do so, subject to the following conditions: 9 10The above copyright notice and this permission notice shall be included in all copies or 11substantial portions of the Software. 12 13THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT 14NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND 15NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, 16DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT 17OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. 18**************************************************************************************************/ 19 20#ifndef Solver_h 21#define Solver_h 22 23#include "SolverTypes.h" 24#include "VarOrder.h" 25#include "Proof.h" 26 27// Redfine if you want output to go somewhere else: 28#define reportf(format, args...) ( printf(format , ## args), fflush(stdout) ) 29 30 31//================================================================================================= 32// Solver -- the main class: 33 34 35struct SolverStats { 36 int64 starts, decisions, propagations, conflicts; 37 int64 clauses_literals, learnts_literals, max_literals, tot_literals; 38 SolverStats() : starts(0), decisions(0), propagations(0), conflicts(0) 39 , clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) { } 40}; 41 42 43struct SearchParams { 44 double var_decay, clause_decay, random_var_freq; // (reasonable values are: 0.95, 0.999, 0.02) 45 SearchParams(double v = 1, double c = 1, double r = 0) : var_decay(v), clause_decay(c), random_var_freq(r) { } 46}; 47 48 49class Solver { 50protected: 51 // Solver state: 52 // 53 bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used! 54 vec<Clause*> clauses; // List of problem clauses. 55 vec<Clause*> learnts; // List of learnt clauses. 56 vec<ClauseId> unit_id; // 'unit_id[var]' is the clause ID for the unit literal 'var' or '~var' (if set at toplevel). 57 double cla_inc; // Amount to bump next clause with. 58 double cla_decay; // INVERSE decay factor for clause activity: stores 1/decay. 59 60 vec<double> activity; // A heuristic measurement of the activity of a variable. 61 double var_inc; // Amount to bump next variable with. 62 double var_decay; // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order. 63 VarOrder order; // Keeps track of the decision variable order. 64 65 vec<vec<Clause*> > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). 66 vec<char> assigns; // The current assignments (lbool:s stored as char:s). 67 vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made. 68 vec<int> trail_lim; // Separator indices for different decision levels in 'trail[]'. 69 vec<Clause*> reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none. 70 vec<bool> sreason; // true if var is negated in reason[var]. used to write out pivot sign info to proof log 71 vec<int> level; // 'level[var]' is the decision level at which assignment was made. 72 vec<int> trail_pos; // 'trail_pos[var]' is the variable's position in 'trail[]'. This supersedes 'level[]' in some sense, and 'level[]' will probably be removed in future releases. 73 int root_level; // Level of first proper decision. 74 int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat). 75 int simpDB_assigns; // Number of top-level assignments since last execution of 'simplifyDB()'. 76 int64 simpDB_props; // Remaining number of propagations that must be made before next execution of 'simplifyDB()'. 77 78 // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which is used: 79 // 80 vec<char> analyze_seen; 81 vec<Lit> analyze_stack; 82 vec<Lit> analyze_toclear; 83 Clause* propagate_tmpbin; 84 Clause* analyze_tmpbin; 85 vec<Lit> addUnit_tmp; 86 vec<Lit> addBinary_tmp; 87 vec<Lit> addTernary_tmp; 88 89 // Main internal methods: 90 // 91 bool assume (Lit p); 92 void cancelUntil (int level); 93 void record (const vec<Lit>& clause); 94 95 void analyze (Clause* confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack) 96 bool analyze_removable(Lit p, uint min_level); // (helper method for 'analyze()') 97 void analyzeFinal (Clause* confl, bool skip_first = false); 98 bool enqueue (Lit fact, Clause* from = NULL); 99 Clause* propagate (); 100 void reduceDB (); 101 Lit pickBranchLit (const SearchParams& params); 102 lbool search (int nof_conflicts, int nof_learnts, const SearchParams& params); 103 double progressEstimate (); 104 105 // Activity: 106 // 107 void varBumpActivity(Lit p) { 108 if (var_decay < 0) return; // (negative decay means static variable order -- don't bump) 109 if ( (activity[var(p)] += var_inc) > 1e100 ) varRescaleActivity(); 110 order.update(var(p)); } 111 void varDecayActivity () { if (var_decay >= 0) var_inc *= var_decay; } 112 void varRescaleActivity(); 113 void claDecayActivity () { cla_inc *= cla_decay; } 114 void claRescaleActivity(); 115 116 // Operations on clauses: 117 // 118 void newClause(const vec<Lit>& ps, bool learnt = false, ClauseId id = ClauseId_NULL); 119 void claBumpActivity (Clause* c) { if ( (c->activity() += cla_inc) > 1e20 ) claRescaleActivity(); } 120 void remove (Clause* c, bool just_dealloc = false); 121 bool locked (const Clause* c) const { return reason[var((*c)[0])] == c; } 122 bool simplify (Clause* c) const; 123 124 int decisionLevel() const { return trail_lim.size(); } 125 126public: 127 Solver() : ok (true) 128 , cla_inc (1) 129 , cla_decay (1) 130 , var_inc (1) 131 , var_decay (1) 132 , order (assigns, activity) 133 , qhead (0) 134 , simpDB_assigns (0) 135 , simpDB_props (0) 136 , default_params (SearchParams(0.95, 0.999, 0.02)) 137 , expensive_ccmin (true) 138 , proof (NULL) 139 , verbosity (0) 140 , progress_estimate(0) 141 , conflict_id (ClauseId_NULL) 142 { 143 vec<Lit> dummy(2,lit_Undef); 144 propagate_tmpbin = Clause_new(false, dummy); 145 analyze_tmpbin = Clause_new(false, dummy); 146 addUnit_tmp .growTo(1); 147 addBinary_tmp .growTo(2); 148 addTernary_tmp.growTo(3); 149 } 150 151 ~Solver() { 152 for (int i = 0; i < learnts.size(); i++) remove(learnts[i], true); 153 for (int i = 0; i < clauses.size(); i++) if (clauses[i] != NULL) remove(clauses[i], true); 154 remove(propagate_tmpbin, true); 155 remove(analyze_tmpbin, true); 156 } 157 158 // Helpers: (semi-internal) 159 // 160 lbool value(Var x) const { return toLbool(assigns[x]); } 161 lbool value(Lit p) const { return sign(p) ? ~toLbool(assigns[var(p)]) : toLbool(assigns[var(p)]); } 162 163 int nAssigns() { return trail.size(); } 164 int nClauses() { return clauses.size(); } 165 int nLearnts() { return learnts.size(); } 166 167 // Statistics: (read-only member variable) 168 // 169 SolverStats stats; 170 171 // Mode of operation: 172 // 173 SearchParams default_params; // Restart frequency etc. 174 bool expensive_ccmin; // Controls conflict clause minimization. TRUE by default. 175 Proof* proof; // Set this directly after constructing 'Solver' to enable proof logging. Initialized to NULL. 176 int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything 177 178 // Problem specification: 179 // 180 Var newVar (); 181 int nVars () { return assigns.size(); } 182 void addUnit (Lit p) { addUnit_tmp [0] = p; addClause(addUnit_tmp); } 183 void addBinary (Lit p, Lit q) { addBinary_tmp [0] = p; addBinary_tmp [1] = q; addClause(addBinary_tmp); } 184 void addTernary(Lit p, Lit q, Lit r) { addTernary_tmp[0] = p; addTernary_tmp[1] = q; addTernary_tmp[2] = r; addClause(addTernary_tmp); } 185 void addClause (const vec<Lit>& ps) { newClause(ps); } // (used to be a difference between internal and external method...) 186 187 // Solving: 188 // 189 bool okay() { return ok; } // FALSE means solver is in an conflicting state (must never be used again!) 190 void simplifyDB(); 191 bool solve(const vec<Lit>& assumps); 192 bool solve() { vec<Lit> tmp; return solve(tmp); } 193 194 double progress_estimate; // Set by 'search()'. 195 vec<lbool> model; // If problem is satisfiable, this vector contains the model (if any). 196 vec<Lit> conflict; // If problem is unsatisfiable under assumptions, this vector represent the conflict clause expressed in the assumptions. 197 ClauseId conflict_id; // (In proof logging mode only.) ID for the clause 'conflict' (for proof traverseral). NOTE! The empty clause is always the last clause derived, but for conflicts under assumption, this is not necessarly true. 198}; 199 200 201//================================================================================================= 202// Debug: 203 204 205#define L_LIT "%s%d" 206#define L_lit(p) sign(p)?"-":"", var(p)+1 207 208// Just like 'assert()' but expression will be evaluated in the release version as well. 209inline void check(bool expr) { assert(expr); } 210 211 212//================================================================================================= 213#endif 214