1 #ifndef sat_h
2 #define sat_h
3
4 #include <climits>
5 #include <cmath>
6 #include <map>
7 #include <set>
8 #include <string>
9 #include <chuffed/support/misc.h>
10 #include <chuffed/support/heap.h>
11 #include <chuffed/core/sat-types.h>
12 #include <chuffed/branching/branching.h>
13
14 #include <sstream>
15
16 #define TEMP_SC_LEN 1024
17 #define MAX_SHARE_LEN 512
18
19 class IntVar;
20 class SClause;
21
22 extern std::map<int,std::string> litString;
23
24 inline
getLitString(int n)25 std::string getLitString(int n) {
26 if (n == toInt(lit_True)) return "true";
27 if (n == toInt(lit_False)) return "false";
28 if (n == toInt(~lit_True)) return "false";
29 if (n == toInt(~lit_False)) return "true";
30 std::map<int,std::string>::const_iterator it = litString.find(n);
31 if (it != litString.end())
32 return it->second;
33 else {
34 std::stringstream ss;
35 ss << "UNKNOWN_LITERAL (" << n << ")";
36 return ss.str();
37 }
38 }
39
40 class SAT : public Branching {
41 // For sorting Lits in learnt clause
42 struct LitSort {
43 vec<int>& level;
operatorLitSort44 bool operator() (Lit i, Lit j) { return (level[var(i)] > level[var(j)]); }
LitSortLitSort45 LitSort(vec<int>& l) : level(l) {}
46 } lit_sort;
47
48 // For VSIDS
49 struct VarOrderLt {
50 const vec<double>& activity;
operatorVarOrderLt51 bool operator () (int x, int y) const { return activity[x] > activity[y]; }
VarOrderLtVarOrderLt52 VarOrderLt(const vec<double>& act) : activity(act) {}
53 };
54
55 public:
56
57 // Persistent state
58
59 vec<Clause*> clauses; // List of problem clauses
60 vec<Clause*> learnts; // List of learnt clauses
61
62 vec<ChannelInfo> c_info; // Channel info
63 vec<vec<WatchElem> > watches; // Watched lists
64 vec<char> assigns; // The current assignments
65 vec<Reason> reason; // explanation for the variable's current value, or 'NULL' if none
66 vec<int> trailpos; // the trailPos at which the assignment was made
67 vec<LitFlags> flags; // Info about literal
68
69 duration pushback_time;
70
71 // Lazy Lit Generation
72 int orig_cutoff;
73 vec<int> var_free_list;
74 vec<int> num_used;
75
76 vec<vec<Lit> > trail; // Boolean vars fix order
77 vec<int> qhead;
78
79 vec<vec<Clause*> > rtrail; // List of temporary reason clauses
80
81 // Intermediate state
82 Clause *confl;
83 int index;
84 vec<Lit> out_learnt;
85 vec<int> out_learnt_level;
86 vec<char> seen;
87 vec<bool> ivseen;
88 vec<int> ivseen_toclear;
89 vec<Lit> analyze_stack;
90 vec<Lit> analyze_toclear;
91 vec<IntVar*> min_vars;
92 SClause *temp_sc;
93
94 Clause *short_expl;
95 Clause *short_confl;
96
97 // VSIDS
98 double var_inc; // Amount to bump variable with.
99 double cla_inc; // Amount to bump clause with.
100 vec<double> activity; // A heuristic measurement of the activity of a variable.
101 Heap<VarOrderLt> order_heap; // A priority queue of variables ordered with respect to the variable activity.
102 vec<bool> polarity;
103
104 void insertVarOrder(int x); // Insert a variable in the decision order priority queue.
105 void varDecayActivity(); // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead.
106 void varBumpActivity(Lit p); // Increase a variable with the current 'bump' value.
107 void claDecayActivity(); // Decay all clause activities with the specified factor
108 void learntLenDecayActivity();
109 void learntLenBumpActivity(int l);
110
111 // Statistics
112 int bin_clauses, tern_clauses, long_clauses, learnt_clauses;
113 long long int propagations, back_jumps, nrestarts, next_simp_db;
114 long long int clauses_literals, learnts_literals, max_literals, tot_literals;
115 double avg_depth;
116 double confl_rate;
117
118 // Parallel
119
120 time_point ll_time;
121 double ll_inc;
122 double learnt_len_el;
123 vec<double> learnt_len_occ;
124
125 // Propagator methods
126
127 SAT();
128 ~SAT();
129 void init();
130 int newVar(int n = 1, ChannelInfo ci = ci_null);
131 int getLazyVar(ChannelInfo ci);
132 void removeLazyVar(int v);
133 void addClause(Lit p, Lit q);
134 void addClause(vec<Lit>& ps, bool one_watch = false);
135 void addClause(Clause& c, bool one_watch = false);
136 void removeClause(Clause& c);
137 void topLevelCleanUp();
138 void simplifyDB();
139 bool simplify(Clause& c);
140 void enqueue(Lit p, Reason r = NULL);
141 void cEnqueue(Lit p, Reason r);
142 void aEnqueue(Lit p, Reason r, int l);
143 void untrailToPos(vec<Lit>& t, int p);
144 void btToLevel(int level);
145 void btToPos(int sat_pos, int core_pos);
146 bool propagate();
147 Clause* getExpl(Lit p);
148 Clause* _getExpl(Lit p);
149 Clause* getConfl(Reason& r, Lit p);
150
151
152 void reduceDB();
153 void printStats();
154 void printLearntStats();
155
156 // Branching methods
157
158 bool finished();
getScore(VarBranch vb)159 double getScore(VarBranch vb) { NEVER; }
160 DecInfo* branch();
161
162 // Parallel methods
163
164 void convertToSClause(Clause& c);
165 void convertToClause(SClause& sc);
166 void addLearnt();
167 void updateShareParam();
168
169 // Conflict methods
170
171 void analyze(int nodeid, std::set<int>& contributingNogoods);
172 void getLearntClause(int nodeid, std::set<int>& contributingNogoods);
173 int findConflictLevel();
174 void explainUnlearnable(std::set<int>& contributingNogoods);
175 void explainToExhaustion(std::set<int>& contributingNogoods);
176 void clearSeen();
177 int findBackTrackLevel();
178
179
consistent()180 bool consistent () const { return qhead.last() == trail.last().size(); }
nVars()181 int nVars () const { return assigns.size(); }
decisionLevel()182 int decisionLevel () const { return trail.size()-1; }
decLit(int i)183 Lit decLit (int i) const { return trail[i][0]; }
value(Lit p)184 lbool value (Lit p) const { return toLbool(assigns[var(p)]) ^ sign(p); }
locked(Clause & c)185 bool locked (Clause& c) const { return reason[var(c[0])].pt == &c && value(c[0]) == l_True; }
186
187 void newDecisionLevel();
188 void incVarUse(int v);
189 void decVarUse(int v);
190 void setConfl(Lit p = lit_False, Lit q = lit_False);
191
isRootLevel(int v)192 bool isRootLevel(int v) const { return engine.trail_lim.size()==0 || trailpos[v] < engine.trail_lim[0]; }
isCurLevel(int v)193 bool isCurLevel(int v) const { return trailpos[v] >= engine.trail_lim.last(); }
getLevel(int v)194 int getLevel(int v) const {
195 for (int i = engine.trail_lim.size(); i--; ) {
196 if (trailpos[v] >= engine.trail_lim[i])
197 return i;
198 }
199 return 0;
200 }
201
202 // Debug Methods
203
204 void printLit(Lit p);
205 template <class T> void printClause(T& c);
206 void checkConflict();
207 void checkExplanation(Clause& c, int clevel, int index);
208
209 };
210
newDecisionLevel()211 inline void SAT::newDecisionLevel() {
212 trail.push();
213 qhead.push(0);
214 rtrail.push();
215 }
216
incVarUse(int v)217 inline void SAT::incVarUse(int v) {
218 v -= orig_cutoff;
219 if (v >= 0) num_used[v]++;
220 }
221
decVarUse(int v)222 inline void SAT::decVarUse(int v) {
223 v -= orig_cutoff;
224 if (v >= 0) num_used[v]--;
225 }
226
getExpl(Lit p)227 inline Clause* SAT::getExpl(Lit p) {
228 Reason& r = reason[var(p)];
229 switch(r.d.type) {
230 case 0:
231 return r.pt;
232 case 1:
233 btToPos(index, trailpos[var(p)]);
234 return _getExpl(p);
235 default:
236 Clause& c = *short_expl;
237 c.sz = r.d.type; c[1] = toLit(r.d.d1);
238 if (c.sz == 3)
239 c[2] = toLit(r.d.d2);
240 return short_expl;
241 }
242 }
243
244 extern SAT sat;
245
246 #endif
247