add minisat and TNM sequential solvers in sat problem
[charm.git] / examples / charm++ / satisfiability / minisat / Solver.h
1 /****************************************************************************************[Solver.h]
2 MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
3
4 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
5 associated documentation files (the "Software"), to deal in the Software without restriction,
6 including without limitation the rights to use, copy, modify, merge, publish, distribute,
7 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
8 furnished to do so, subject to the following conditions:
9
10 The above copyright notice and this permission notice shall be included in all copies or
11 substantial portions of the Software.
12
13 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
14 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
15 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
16 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
17 OF 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 <cstdio>
24
25 #include "mtl/Vec.h"
26 #include "mtl/minisatHeap.h"
27 #include "mtl/Alg.h"
28
29 #include "SolverTypes.h"
30
31 #include <vector>
32
33 using namespace std;
34
35 //=================================================================================================
36 // Solver -- the main class:
37
38
39 bool seq_processing(int var_size, const vector< vector<int> >& clauses);
40
41     class Solver {
42 public:
43
44     // Constructor/Destructor:
45     //
46     Solver();
47     ~Solver();
48
49
50     // Problem specification:
51     //
52     Var     newVar    (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
53     bool    addClause (vec<Lit>& ps);                           // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method!
54
55     // Solving:
56     //
57     bool    simplify     ();                        // Removes already satisfied clauses.
58     bool    solve        (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions.
59     bool    solve        ();                        // Search without assumptions.
60     bool    okay         () const;                  // FALSE means solver is in a conflicting state
61
62     // Variable mode:
63     // 
64     void    setPolarity    (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
65     void    setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic.
66
67     // Read state:
68     //
69     lbool   value      (Var x) const;       // The current value of a variable.
70     lbool   value      (Lit p) const;       // The current value of a literal.
71     lbool   modelValue (Lit p) const;       // The value of a literal in the last model. The last call to solve must have been satisfiable.
72     int     nAssigns   ()      const;       // The current number of assigned literals.
73     int     nClauses   ()      const;       // The current number of original clauses.
74     int     nLearnts   ()      const;       // The current number of learnt clauses.
75     int     nVars      ()      const;       // The current number of variables.
76
77     // Extra results: (read-only member variable)
78     //
79     vec<lbool> model;             // If problem is satisfiable, this vector contains the model (if any).
80     vec<Lit>   conflict;          // If problem is unsatisfiable (possibly under assumptions),
81                                   // this vector represent the final conflict clause expressed in the assumptions.
82
83     // Mode of operation:
84     //
85     double    var_decay;          // Inverse of the variable activity decay factor.                                            (default 1 / 0.95)
86     double    clause_decay;       // Inverse of the clause activity decay factor.                                              (1 / 0.999)
87     double    random_var_freq;    // The frequency with which the decision heuristic tries to choose a random variable.        (default 0.02)
88     int       restart_first;      // The initial restart limit.                                                                (default 100)
89     double    restart_inc;        // The factor with which the restart limit is multiplied in each restart.                    (default 1.5)
90     double    learntsize_factor;  // The intitial limit for learnt clauses is a factor of the original clauses.                (default 1 / 3)
91     double    learntsize_inc;     // The limit for learnt clauses is multiplied with this factor each restart.                 (default 1.1)
92     bool      expensive_ccmin;    // Controls conflict clause minimization.                                                    (default TRUE)
93     int       polarity_mode;      // Controls which polarity the decision heuristic chooses. See enum below for allowed modes. (default polarity_false)
94     int       verbosity;          // Verbosity level. 0=silent, 1=some progress report                                         (default 0)
95
96     enum { polarity_true = 0, polarity_false = 1, polarity_user = 2, polarity_rnd = 3 };
97
98     // Statistics: (read-only member variable)
99     //
100     uint64_t starts, decisions, rnd_decisions, propagations, conflicts;
101     uint64_t clauses_literals, learnts_literals, max_literals, tot_literals;
102
103 protected:
104
105     // Helper structures:
106     //
107     struct VarOrderLt {
108         const vec<double>&  activity;
109         bool operator () (Var x, Var y) const { return activity[x] > activity[y]; }
110         VarOrderLt(const vec<double>&  act) : activity(act) { }
111     };
112
113     friend class VarFilter;
114     struct VarFilter {
115         const Solver& s;
116         VarFilter(const Solver& _s) : s(_s) {}
117         bool operator()(Var v) const { return toLbool(s.assigns[v]) == l_Undef && s.decision_var[v]; }
118     };
119
120     // Solver state:
121     //
122     bool                ok;               // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
123     vec<Clause*>        clauses;          // List of problem clauses.
124     vec<Clause*>        learnts;          // List of learnt clauses.
125     double              cla_inc;          // Amount to bump next clause with.
126     vec<double>         activity;         // A heuristic measurement of the activity of a variable.
127     double              var_inc;          // Amount to bump next variable with.
128     vec<vec<Clause*> >  watches;          // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
129     vec<char>           assigns;          // The current assignments (lbool:s stored as char:s).
130     vec<char>           polarity;         // The preferred polarity of each variable.
131     vec<char>           decision_var;     // Declares if a variable is eligible for selection in the decision heuristic.
132     vec<Lit>            trail;            // Assignment stack; stores all assigments made in the order they were made.
133     vec<int>            trail_lim;        // Separator indices for different decision levels in 'trail'.
134     vec<Clause*>        reason;           // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
135     vec<int>            level;            // 'level[var]' contains the level at which the assignment was made.
136     int                 qhead;            // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
137     int                 simpDB_assigns;   // Number of top-level assignments since last execution of 'simplify()'.
138     int64_t             simpDB_props;     // Remaining number of propagations that must be made before next execution of 'simplify()'.
139     vec<Lit>            assumptions;      // Current set of assumptions provided to solve by the user.
140     Heap<VarOrderLt>    order_heap;       // A priority queue of variables ordered with respect to the variable activity.
141     double              random_seed;      // Used by the random variable selection.
142     double              progress_estimate;// Set by 'search()'.
143     bool                remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'.
144
145     // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is
146     // used, exept 'seen' wich is used in several places.
147     //
148     vec<char>           seen;
149     vec<Lit>            analyze_stack;
150     vec<Lit>            analyze_toclear;
151     vec<Lit>            add_tmp;
152
153     // Main internal methods:
154     //
155     void     insertVarOrder   (Var x);                                                 // Insert a variable in the decision order priority queue.
156     Lit      pickBranchLit    (int polarity_mode, double random_var_freq);             // Return the next decision variable.
157     void     newDecisionLevel ();                                                      // Begins a new decision level.
158     void     uncheckedEnqueue (Lit p, Clause* from = NULL);                            // Enqueue a literal. Assumes value of literal is undefined.
159     bool     enqueue          (Lit p, Clause* from = NULL);                            // Test if fact 'p' contradicts current state, enqueue otherwise.
160     Clause*  propagate        ();                                                      // Perform unit propagation. Returns possibly conflicting clause.
161     void     cancelUntil      (int level);                                             // Backtrack until a certain level.
162     void     analyze          (Clause* confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack)
163     void     analyzeFinal     (Lit p, vec<Lit>& out_conflict);                         // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
164     bool     litRedundant     (Lit p, uint32_t abstract_levels);                       // (helper method for 'analyze()')
165     lbool    search           (int nof_conflicts, int nof_learnts);                    // Search for a given number of conflicts.
166     void     reduceDB         ();                                                      // Reduce the set of learnt clauses.
167     void     removeSatisfied  (vec<Clause*>& cs);                                      // Shrink 'cs' to contain only non-satisfied clauses.
168
169     // Maintaining Variable/Clause activity:
170     //
171     void     varDecayActivity ();                      // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead.
172     void     varBumpActivity  (Var v);                 // Increase a variable with the current 'bump' value.
173     void     claDecayActivity ();                      // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead.
174     void     claBumpActivity  (Clause& c);             // Increase a clause with the current 'bump' value.
175
176     // Operations on clauses:
177     //
178     void     attachClause     (Clause& c);             // Attach a clause to watcher lists.
179     void     detachClause     (Clause& c);             // Detach a clause to watcher lists.
180     void     removeClause     (Clause& c);             // Detach and free a clause.
181     bool     locked           (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state.
182     bool     satisfied        (const Clause& c) const; // Returns TRUE if a clause is satisfied in the current state.
183
184     // Misc:
185     //
186     int      decisionLevel    ()      const; // Gives the current decisionlevel.
187     uint32_t abstractLevel    (Var x) const; // Used to represent an abstraction of sets of decision levels.
188     double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
189
190     // Debug:
191     void     printLit         (Lit l);
192     template<class C>
193     void     printClause      (const C& c);
194     void     verifyModel      ();
195     void     checkLiteralCount();
196
197     // Static helpers:
198     //
199
200     // Returns a random float 0 <= x < 1. Seed must never be 0.
201     static inline double drand(double& seed) {
202         seed *= 1389796;
203         int q = (int)(seed / 2147483647);
204         seed -= (double)q * 2147483647;
205         return seed / 2147483647; }
206
207     // Returns a random integer 0 <= x < size. Seed must never be 0.
208     static inline int irand(double& seed, int size) {
209         return (int)(drand(seed) * size); }
210 };
211
212
213 //=================================================================================================
214 // Implementation of inline methods:
215
216
217 inline void Solver::insertVarOrder(Var x) {
218     if (!order_heap.inHeap(x) && decision_var[x]) order_heap.insert(x); }
219
220 inline void Solver::varDecayActivity() { var_inc *= var_decay; }
221 inline void Solver::varBumpActivity(Var v) {
222     if ( (activity[v] += var_inc) > 1e100 ) {
223         // Rescale:
224         for (int i = 0; i < nVars(); i++)
225             activity[i] *= 1e-100;
226         var_inc *= 1e-100; }
227
228     // Update order_heap with respect to new activity:
229     if (order_heap.inHeap(v))
230         order_heap.decrease(v); }
231
232 inline void Solver::claDecayActivity() { cla_inc *= clause_decay; }
233 inline void Solver::claBumpActivity (Clause& c) {
234         if ( (c.activity() += cla_inc) > 1e20 ) {
235             // Rescale:
236             for (int i = 0; i < learnts.size(); i++)
237                 learnts[i]->activity() *= 1e-20;
238             cla_inc *= 1e-20; } }
239
240 inline bool     Solver::enqueue         (Lit p, Clause* from)   { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }
241 inline bool     Solver::locked          (const Clause& c) const { return reason[var(c[0])] == &c && value(c[0]) == l_True; }
242 inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); }
243
244 inline int      Solver::decisionLevel ()      const   { return trail_lim.size(); }
245 inline uint32_t Solver::abstractLevel (Var x) const   { return 1 << (level[x] & 31); }
246 inline lbool    Solver::value         (Var x) const   { return toLbool(assigns[x]); }
247 inline lbool    Solver::value         (Lit p) const   { return toLbool(assigns[var(p)]) ^ sign(p); }
248 inline lbool    Solver::modelValue    (Lit p) const   { return model[var(p)] ^ sign(p); }
249 inline int      Solver::nAssigns      ()      const   { return trail.size(); }
250 inline int      Solver::nClauses      ()      const   { return clauses.size(); }
251 inline int      Solver::nLearnts      ()      const   { return learnts.size(); }
252 inline int      Solver::nVars         ()      const   { return assigns.size(); }
253 inline void     Solver::setPolarity   (Var v, bool b) { polarity    [v] = (char)b; }
254 inline void     Solver::setDecisionVar(Var v, bool b) { decision_var[v] = (char)b; if (b) { insertVarOrder(v); } }
255 inline bool     Solver::solve         ()              { vec<Lit> tmp; return solve(tmp); }
256 inline bool     Solver::okay          ()      const   { return ok; }
257
258
259
260 //=================================================================================================
261 // Debug + etc:
262
263
264 #define reportf(format, args...) ( fflush(stdout), fprintf(stderr, format, ## args), fflush(stderr) )
265
266 static inline void logLit(FILE* f, Lit l)
267 {
268     fprintf(f, "%sx%d", sign(l) ? "~" : "", var(l)+1);
269 }
270
271 static inline void logLits(FILE* f, const vec<Lit>& ls)
272 {
273     fprintf(f, "[ ");
274     if (ls.size() > 0){
275         logLit(f, ls[0]);
276         for (int i = 1; i < ls.size(); i++){
277             fprintf(f, ", ");
278             logLit(f, ls[i]);
279         }
280     }
281     fprintf(f, "] ");
282 }
283
284 static inline const char* showBool(bool b) { return b ? "true" : "false"; }
285
286
287 // Just like 'assert()' but expression will be evaluated in the release version as well.
288 static inline void check(bool expr) { assert(expr); }
289
290
291 inline void Solver::printLit(Lit l)
292 {
293     reportf("%s%d:%c", sign(l) ? "-" : "", var(l)+1, value(l) == l_True ? '1' : (value(l) == l_False ? '0' : 'X'));
294 }
295
296
297 template<class C>
298 inline void Solver::printClause(const C& c)
299 {
300     for (int i = 0; i < c.size(); i++){
301         printLit(c[i]);
302         fprintf(stderr, " ");
303     }
304 }
305
306
307 //=================================================================================================
308 #endif