1 /******************************************
2 Copyright (c) 2016, Mate Soos
3
4 Permission is hereby granted, free of charge, to any person obtaining a copy
5 of this software and associated documentation files (the "Software"), to deal
6 in the Software without restriction, including without limitation the rights
7 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
8 copies of the Software, and to permit persons to whom the Software is
9 furnished to do so, subject to the following conditions:
10
11 The above copyright notice and this permission notice shall be included in
12 all copies or substantial portions of the Software.
13
14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
15 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
16 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
17 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
18 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
19 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
20 THE SOFTWARE.
21 ***********************************************/
22
23 #ifndef __PROPENGINE_H__
24 #define __PROPENGINE_H__
25
26 #include <cstdio>
27 #include <string.h>
28 #include <stack>
29 #include <set>
30 #include <cmath>
31
32 //#define ANIMATE3D
33
34 #include "constants.h"
35 #include "propby.h"
36 #include "vmtf.h"
37
38 #include "avgcalc.h"
39 #include "propby.h"
40 #include "heap.h"
41 #include "alg.h"
42 #include "clause.h"
43 #include "boundedqueue.h"
44 #include "cnf.h"
45 #include "watchalgos.h"
46
47 namespace CMSat {
48
49 using std::set;
50 class Solver;
51 class SQLStats;
52
53 //#define VERBOSE_DEBUG_FULLPROP
54 //#define VERBOSE_DEBUG
55
56 #ifdef VERBOSE_DEBUG
57 #define VERBOSE_DEBUG_FULLPROP
58 #define ENQUEUE_DEBUG
59 #define DEBUG_ENQUEUE_LEVEL0
60 #endif
61
62 class Solver;
63 class ClauseAllocator;
64 class Gaussian;
65
66 enum PropResult {
67 PROP_FAIL = 0
68 , PROP_NOTHING = 1
69 , PROP_SOMETHING = 2
70 , PROP_TODO = 3
71 };
72
73 struct Trail {
74
TrailTrail75 Trail () {
76 }
77
TrailTrail78 Trail (Lit _lit, uint32_t _lev) :
79 lit(_lit)
80 , lev(_lev)
81 {}
82
83 Lit lit;
84 uint32_t lev;
85 };
86
87 /**
88 @brief The propagating and conflict generation class
89
90 Handles watchlists, conflict analysis, propagation, variable settings, etc.
91 */
92 class PropEngine: public CNF
93 {
94 public:
95
96 // Constructor/Destructor:
97 //
98 PropEngine(
99 const SolverConf* _conf
100 , Solver* solver
101 , std::atomic<bool>* _must_interrupt_inter
102 );
103 ~PropEngine();
104
105 // Read state:
106 //
107 uint32_t nAssigns () const; ///<The current number of assigned literals.
108
109 //Get state
110 uint32_t decisionLevel() const; ///<Returns current decision level
111 size_t getTrailSize() const; //number of variables set at decision level 0
trail_size()112 size_t trail_size() const {
113 return trail.size();
114 }
trail_at(size_t at)115 Lit trail_at(size_t at) const {
116 return trail[at].lit;
117 }
118 bool propagate_occur();
119 PropStats propStats;
120 template<bool update_bogoprops = true>
121 void enqueue(const Lit p, const uint32_t level, const PropBy from = PropBy());
122 template<bool update_bogoprops = true>
123 void enqueue(const Lit p);
124 void new_decision_level();
125
126 /////////////////////
127 // Branching
128 /////////////////////
129 vector<ActAndOffset> var_act_vsids;
130 vector<ActAndOffset> var_act_maple;
131 double var_decay;
132 double var_decay_max;
133 double maple_step_size;
134 struct VarOrderLt { ///Order variables according to their activities
135 const vector<ActAndOffset>& activities;
operatorVarOrderLt136 bool operator () (const uint32_t x, const uint32_t y) const
137 {
138 return activities[x].combine() > activities[y].combine();
139 }
140
VarOrderLtVarOrderLt141 explicit VarOrderLt(const vector<ActAndOffset>& _activities) :
142 activities(_activities)
143 {}
144 };
145 ///activity-ordered heap of decision variables.
146 Heap<VarOrderLt> order_heap_vsids; ///NOT VALID WHILE SIMPLIFYING
147 Heap<VarOrderLt> order_heap_maple; ///NOT VALID WHILE SIMPLIFYING
148 #ifdef VMTF_NEEDED
149 Queue vmtf_queue;
150 vector<uint64_t> vmtf_btab; // enqueue time stamps for queue
151 void vmtf_update_queue_unassigned (uint32_t idx);
152 void vmtf_init_enqueue (uint32_t idx);
153 void vmtf_bump_queue (uint32_t var);
vmtf_link(uint32_t var)154 Link & vmtf_link (uint32_t var) { return vmtf_links[var]; }
155 Links vmtf_links; // table of vmtf_links for decision queue
156 #endif
157 double max_vsids_act = 0.0;
158
159 //Clause activities
160 double max_cl_act = 0.0;
161
162 protected:
163 int64_t simpDB_props = 0;
164 void new_var(const bool bva, const uint32_t orig_outer) override;
165 void new_vars(const size_t n) override;
166 void save_on_var_memory();
167 template<class T> uint32_t calc_glue(const T& ps);
168
169 //For state saving
170 void save_state(SimpleOutFile& f) const;
171 void load_state(SimpleInFile& f);
172
173 //Stats for conflicts
174 ConflCausedBy lastConflictCausedBy;
175
176 // Solver state:
177 //
178 vector<Trail> trail; ///< Assignment stack; stores all assignments made in the order they were made.
179 vector<uint32_t> trail_lim; ///< Separator indices for different decision levels in 'trail'.
180 uint32_t qhead; ///< Head of queue (as index into the trail)
181 Lit failBinLit; ///< Used to store which watches[lit] we were looking through when conflict occured
182
183 friend class EGaussian;
184
185 PropBy propagate_any_order_fast();
186 template<bool update_bogoprops>
187 PropBy propagate_any_order();
188 PropResult prop_normal_helper(
189 Clause& c
190 , ClOffset offset
191 , Watched*& j
192 , const Lit p
193 );
194 PropResult handle_normal_prop_fail(Clause& c, ClOffset offset, PropBy& confl);
195
196 /////////////////
197 // Operations on clauses:
198 /////////////////
199 void attachClause(
200 const Clause& c
201 , const bool checkAttach = true
202 );
203
204 void detach_bin_clause(
205 Lit lit1
206 , Lit lit2
207 , bool red
208 , bool allow_empty_watch = false
209 , bool allow_change_order = false
210 ) {
211 if (!allow_change_order) {
212 if (!(allow_empty_watch && watches[lit1].empty())) {
213 removeWBin(watches, lit1, lit2, red);
214 }
215 if (!(allow_empty_watch && watches[lit2].empty())) {
216 removeWBin(watches, lit2, lit1, red);
217 }
218 } else {
219 if (!(allow_empty_watch && watches[lit1].empty())) {
220 removeWBin_change_order(watches, lit1, lit2, red);
221 }
222 if (!(allow_empty_watch && watches[lit2].empty())) {
223 removeWBin_change_order(watches, lit2, lit1, red);
224 }
225 }
226 }
227 void attach_bin_clause(
228 const Lit lit1
229 , const Lit lit2
230 , const bool red
231 , const bool checkUnassignedFirst = true
232 );
233 void detach_modified_clause(
234 const Lit lit1
235 , const Lit lit2
236 , const Clause* address
237 );
238
239 // Debug & etc:
240 void print_all_clauses();
241 void printWatchList(const Lit lit) const;
242 bool satisfied(const BinaryClause& bin);
243 void print_trail();
244
245 //Var selection, activity, etc.
246 void updateVars(
247 const vector<uint32_t>& outerToInter
248 , const vector<uint32_t>& interToOuter
249 );
250
mem_used()251 size_t mem_used() const
252 {
253 size_t mem = 0;
254 mem += CNF::mem_used();
255 mem += trail.capacity()*sizeof(Lit);
256 mem += trail_lim.capacity()*sizeof(uint32_t);
257 mem += toClear.capacity()*sizeof(Lit);
258 return mem;
259 }
260
261 private:
262 Solver* solver;
263 bool propagate_binary_clause_occur(const Watched& ws);
264 bool propagate_long_clause_occur(const ClOffset offset);
265 template<bool update_bogoprops = true>
266 bool prop_bin_cl(
267 const Watched* i
268 , const Lit p
269 , PropBy& confl
270 , uint32_t currLevel
271 ); ///<Propagate 2-long clause
272 template<bool update_bogoprops>
273 bool prop_long_cl_any_order(
274 Watched* i
275 , Watched*& j
276 , const Lit p
277 , PropBy& confl
278 , uint32_t currLevel
279 );
280 void sql_dump_vardata_picktime(uint32_t v, PropBy from);
281 };
282
new_decision_level()283 inline void PropEngine::new_decision_level()
284 {
285 trail_lim.push_back(trail.size());
286 #ifdef VERBOSE_DEBUG
287 cout << "New decision level: " << trail_lim.size() << endl;
288 #endif
289 }
290
decisionLevel()291 inline uint32_t PropEngine::decisionLevel() const
292 {
293 return trail_lim.size();
294 }
295
nAssigns()296 inline uint32_t PropEngine::nAssigns() const
297 {
298 return trail.size();
299 }
300
getTrailSize()301 inline size_t PropEngine::getTrailSize() const
302 {
303 if (decisionLevel() == 0) {
304 return trail.size();
305 } else {
306 return trail_lim[0];
307 }
308 }
309
satisfied(const BinaryClause & bin)310 inline bool PropEngine::satisfied(const BinaryClause& bin)
311 {
312 return ((value(bin.getLit1()) == l_True)
313 || (value(bin.getLit2()) == l_True));
314 }
315
316 template<class T> inline
calc_glue(const T & ps)317 uint32_t PropEngine::calc_glue(const T& ps)
318 {
319 MYFLAG++;
320 uint32_t nblevels = 0;
321 for (Lit lit: ps) {
322 int l = varData[lit.var()].level;
323 if (l != 0 && permDiff[l] != MYFLAG) {
324 permDiff[l] = MYFLAG;
325 nblevels++;
326 if (nblevels >= conf.max_glue_cutoff_gluehistltlimited) {
327 return nblevels;
328 }
329 }
330 }
331 return nblevels;
332 }
333
prop_normal_helper(Clause & c,ClOffset offset,Watched * & j,const Lit p)334 inline PropResult PropEngine::prop_normal_helper(
335 Clause& c
336 , ClOffset offset
337 , Watched*& j
338 , const Lit p
339 ) {
340 #ifdef STATS_NEEDED
341 c.stats.clause_looked_at++;
342 #endif
343
344 // Make sure the false literal is data[1]:
345 if (c[0] == ~p) {
346 std::swap(c[0], c[1]);
347 }
348
349 assert(c[1] == ~p);
350
351 // If 0th watch is true, then clause is already satisfied.
352 if (value(c[0]) == l_True) {
353 *j = Watched(offset, c[0]);
354 j++;
355 return PROP_NOTHING;
356 }
357
358 // Look for new watch:
359 for (Lit *k = c.begin() + 2, *end2 = c.end()
360 ; k != end2
361 ; k++
362 ) {
363 //Literal is either unset or satisfied, attach to other watchlist
364 if (value(*k) != l_False) {
365 c[1] = *k;
366 *k = ~p;
367 watches[c[1]].push(Watched(offset, c[0]));
368 return PROP_NOTHING;
369 }
370 }
371
372 return PROP_TODO;
373 }
374
375
handle_normal_prop_fail(Clause & c,ClOffset offset,PropBy & confl)376 inline PropResult PropEngine::handle_normal_prop_fail(
377 Clause&
378 #ifdef STATS_NEEDED
379 c
380 #endif
381 , ClOffset offset
382 , PropBy& confl
383 ) {
384 confl = PropBy(offset);
385 #ifdef VERBOSE_DEBUG_FULLPROP
386 cout << "Conflict from ";
387 Clause& c = *cl_alloc.ptr(offset);
388 for(size_t i = 0; i < c.size(); i++) {
389 cout << c[i] << " , ";
390 }
391 cout << endl;
392 #endif //VERBOSE_DEBUG_FULLPROP
393
394 //Update stats
395 #ifdef STATS_NEEDED
396 c.stats.conflicts_made++;
397 if (c.red())
398 lastConflictCausedBy = ConflCausedBy::longred;
399 else
400 lastConflictCausedBy = ConflCausedBy::longirred;
401 #endif
402
403 qhead = trail.size();
404 return PROP_FAIL;
405 }
406
407 template<bool update_bogoprops>
enqueue(const Lit p)408 void PropEngine::enqueue(const Lit p)
409 {
410 enqueue<update_bogoprops>(p, decisionLevel(), PropBy());
411 }
412
413 template<bool update_bogoprops>
enqueue(const Lit p,const uint32_t level,const PropBy from)414 void PropEngine::enqueue(const Lit p, const uint32_t level, const PropBy from)
415 {
416 #ifdef DEBUG_ENQUEUE_LEVEL0
417 #ifndef VERBOSE_DEBUG
418 if (decisionLevel() == 0)
419 #endif //VERBOSE_DEBUG
420 cout << "enqueue var " << p.var()+1
421 << " to val " << !p.sign()
422 << " level: " << decisionLevel()
423 << " sublevel: " << trail.size()
424 << " by: " << from << endl;
425 #endif //DEBUG_ENQUEUE_LEVEL0
426
427 #ifdef ENQUEUE_DEBUG
428 assert(trail.size() <= nVarsOuter());
429 #endif
430 assert(varData[p.var()].removed == Removed::none);
431
432 const uint32_t v = p.var();
433 assert(value(v) == l_Undef);
434 if (!watches[~p].empty()) {
435 watches.prefetch((~p).toInt());
436 }
437
438 if (!update_bogoprops &&
439 branch_strategy == branch::maple &&
440 from != PropBy())
441 {
442 varData[v].maple_last_picked = sumConflicts;
443 varData[v].maple_conflicted = 0;
444
445 assert(sumConflicts >= varData[v].maple_cancelled);
446 uint32_t age = sumConflicts - varData[v].maple_cancelled;
447 if (age > 0) {
448 double decay = std::pow(var_decay, age);
449 var_act_maple[v].act *= decay;
450 if (order_heap_maple.inHeap(v))
451 order_heap_maple.increase(v);
452 }
453 }
454
455 #if defined(STATS_NEEDED_BRANCH) || defined(FINAL_PREDICTOR_BRANCH)
456 if (!update_bogoprops) {
457 varData[v].set++;
458 if (from == PropBy()) {
459 #ifdef STATS_NEEDED_BRANCH
460 sql_dump_vardata_picktime(v, from);
461 varData[v].num_decided++;
462 varData[v].last_decided_on = sumConflicts;
463 if (!p.sign()) varData[v].num_decided_pos++;
464 #endif
465 } else {
466 sumPropagations++;
467 #ifdef STATS_NEEDED_BRANCH
468 bool flipped = (varData[v].polarity != !p.sign());
469 if (flipped) {
470 varData[v].last_flipped = sumConflicts;
471 }
472 varData[v].num_propagated++;
473 varData[v].last_propagated = sumConflicts;
474 if (!p.sign()) varData[v].num_propagated_pos++;
475 #endif
476 }
477 }
478 #endif
479
480 const bool sign = p.sign();
481 assigns[v] = boolToLBool(!sign);
482 varData[v].reason = from;
483 varData[v].level = level;
484 if (!update_bogoprops) {
485 if (polarity_mode == PolarityMode::polarmode_automatic) {
486 varData[v].polarity = !sign;
487 }
488 #ifdef STATS_NEEDED
489 if (sign) {
490 propStats.varSetNeg++;
491 } else {
492 propStats.varSetPos++;
493 }
494 #endif
495 }
496 trail.push_back(Trail(p, level));
497
498 if (update_bogoprops) {
499 propStats.bogoProps += 1;
500 }
501
502 #ifdef ANIMATE3D
503 std::cerr << "s " << v << " " << p.sign() << endl;
504 #endif
505 }
506
attach_bin_clause(const Lit lit1,const Lit lit2,const bool red,const bool checkUnassignedFirst)507 inline void PropEngine::attach_bin_clause(
508 const Lit lit1
509 , const Lit lit2
510 , const bool red
511 , const bool
512 #ifdef DEBUG_ATTACH
513 checkUnassignedFirst
514 #endif
515 ) {
516 #ifdef DEBUG_ATTACH
517 assert(lit1.var() != lit2.var());
518 if (checkUnassignedFirst) {
519 assert(value(lit1.var()) == l_Undef);
520 assert(value(lit2) == l_Undef || value(lit2) == l_False);
521 }
522
523 assert(varData[lit1.var()].removed == Removed::none);
524 assert(varData[lit2.var()].removed == Removed::none);
525 #endif //DEBUG_ATTACH
526
527 watches[lit1].push(Watched(lit2, red));
528 watches[lit2].push(Watched(lit1, red));
529 }
530
531 } //end namespace
532
533 #endif //__PROPENGINE_H__
534