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