1 #include <cstdio>
2 #include <cassert>
3
4 #include <fstream>
5 #include <iostream>
6 #include <vector>
7 #include <iterator>
8 #include <sstream>
9
10 #include <chuffed/core/options.h>
11 #include <chuffed/core/engine.h>
12 #include <chuffed/core/sat.h>
13 #include <chuffed/core/propagator.h>
14 #include <chuffed/branching/branching.h>
15 #include <chuffed/mip/mip.h>
16 #include <chuffed/parallel/parallel.h>
17 #include <chuffed/ldsb/ldsb.h>
18
19 #include <chuffed/flatzinc/flatzinc.h>
20
21 #ifdef HAS_PROFILER
22 #include <submodules/cp-profiler-integration/connector.hpp>
23 #include <submodules/cp-profiler-integration/message.hpp>
24 #endif
25
26 // #include <boost/date_time/posix_time/posix_time.hpp>
27
28 Engine engine;
29
30 uint64_t bit[65];
31
32 Tint trail_inc;
33
34 int nextnodeid = 0;
35
36 #ifdef HAS_PROFILER
37 cpprofiler::Connector* profilerConnector;
38 #endif
39
40 std::map<IntVar*, string> intVarString;
41 std::map<BoolView, string> boolVarString;
42 string mostRecentLabel;
43
44 extern std::map<int,string> learntClauseString;
45 extern std::ofstream learntStatsStream;
46
47 std::ofstream node_stream;
48
49 #ifdef HAS_PROFILER
doProfiling()50 static bool doProfiling() {
51 return so.print_nodes || profilerConnector->connected();
52 }
53
operator <<(ostream & os,const cpprofiler::NodeUID & uid)54 static ostream& operator<<(ostream& os, const cpprofiler::NodeUID& uid) {
55 return os << "{" << uid.nid << ", " << uid.rid << ", " << uid.tid << "}";
56 }
57
58 template<typename T>
printNode(T && node,std::ostream & os)59 static void printNode(T&& node, std::ostream& os) {
60 os << node.nodeUID() << ", parent: " << node.parentUID()
61 << ", alt: " << node.alt() << ", kids: " << node.kids()
62 << ", status: " << node.status();
63 if (node.label().valid()) {
64 os << ", label: " << node.label().value();
65 }
66 if (node.nogood().valid()) {
67 os << ", nogood: " << node.nogood().value();
68 }
69 if (node.info().valid()) {
70 os << ", info: " << node.info().value();
71 }
72 os << "\n";
73 }
74
75 template<typename T>
sendNode(T && node)76 static void sendNode(T&& node) {
77 if (so.print_nodes) {
78 if (!node_stream.is_open()) {
79 node_stream.open("node-log.log");
80 }
81 printNode(node, node_stream);
82 if (so.debug) {
83 printNode(node, std::cerr);
84 }
85 }
86 node.send();
87 }
88 #endif
89
90 // nodepath is the sequence of node ids leading from the root to the
91 // current node (inclusive).
92 std::vector<int> nodepath;
93
94 // altpath is the sequence of alternatives one follows to get from the
95 // root to the current node. It is typically one element shorter than
96 // nodepath.
97 std::vector<int> altpath;
98
99 // decisionLevelTip[i] is the number of elements in nodepath that
100 // belong to decision level i or above. For example, in this
101 // situation:
102 //
103 // nodepath = [0, 1, 7]
104 // altpath = [0, 1]
105 // decisionLevelTip = [1,3]
106 //
107 // we have that decision level 0 contains only node 0, and decision
108 // level 1 contains nodes 1 and 7. Since decisionLevelTip[1]=3, if we
109 // wish to return to decision level 1 via a backjump, we should keep
110 // the first 3 elements of nodepath.
111 //
112 // Note that decisionLevelTip is never shrunk so its size should not
113 // be depended on. In other words, there may be elements at the end
114 // of the vector, past the current decision level, whose values are
115 // stale and meaningless.
116 std::vector<int> decisionLevelTip;
117
118 // When we rewind after a backjump, should we send the skipped nodes
119 // to the profiler?
120 enum RewindStyle {
121 REWIND_OMIT_SKIPPED,
122 REWIND_SEND_SKIPPED
123 };
124
showVector(const std::vector<int> & v)125 std::string showVector(const std::vector<int>& v) {
126 stringstream ss;
127 for (int i = 0 ; i < v.size() ; i++) {
128 if (i > 0)
129 ss << " ";
130 ss << v[i];
131 }
132 return ss.str();
133 }
134
showVec(const vec<int> & v)135 std::string showVec(const vec<int>& v) {
136 stringstream ss;
137 for (int i = 0 ; i < v.size() ; i++) {
138 if (i > 0)
139 ss << " ";
140 ss << v[i];
141 }
142 return ss.str();
143 }
144
145 // Rewind nodepath and altpath after a backjump.
rewindPaths(int previousDecisionLevel,int newDecisionLevel,RewindStyle rewindStyle,long timestamp)146 void rewindPaths(
147 int previousDecisionLevel, int newDecisionLevel, RewindStyle rewindStyle,
148 long timestamp
149 ) {
150 int currentDecisionLevel;
151 switch (rewindStyle) {
152 case REWIND_OMIT_SKIPPED:
153 nodepath.resize(decisionLevelTip[newDecisionLevel]);
154 altpath.resize(decisionLevelTip[newDecisionLevel]-1);
155 break;
156 case REWIND_SEND_SKIPPED:
157 #if DEBUG_VERBOSE
158 std::cerr << "rewinding to level " << newDecisionLevel << "\n";
159 std::cerr << "before, nodepath is: " << showVector(nodepath) << "\n";
160 std::cerr << " and altpath is: " << showVector(altpath) << "\n";
161 std::cerr << " and dlTip is: " << showVector(decisionLevelTip) << "\n";
162 #endif
163
164 // The tip of the nodepath and altpath lead us to the node
165 // that failed. (That is, the last element of nodepath is the
166 // id of the node that failed.) We first unwind that tip to
167 // the next decision level, so that we don't send a "skipped
168 // child" for that node or any others at this level.
169 nodepath.resize(decisionLevelTip[previousDecisionLevel-1]);
170 altpath.resize(decisionLevelTip[previousDecisionLevel-1] - 1);
171 currentDecisionLevel = previousDecisionLevel-1;
172
173 // Now walk back through the decision levels, sending a
174 // "skipped" node for each child that was never visited.
175 while (nodepath.size() > decisionLevelTip[newDecisionLevel]) {
176 int nodeid = nextnodeid;
177 nextnodeid++;
178 int parent = (nodepath.size() == 0) ? (-1) : (nodepath[nodepath.size()-1]);
179 int myalt = (altpath.size() == 0) ? (-1) : (altpath[altpath.size()-1]);
180
181 // myalt is the alternative that led to the failure; the
182 // skipped node is conceptually the next alternative.
183 myalt++;
184
185 #ifdef HAS_PROFILER
186 if (doProfiling()) {
187 sendNode(profilerConnector->createNode(
188 {nodeid, engine.restart_count, 0}, {parent, 0, 0}, myalt, 0,
189 cpprofiler::NodeStatus::SKIPPED));
190 // .set_decision_level(currentDecisionLevel)
191 // .set_time(timestamp));
192 }
193 #endif
194 nodepath.resize(nodepath.size() - 1);
195 altpath.resize(altpath.size() - 1);
196 currentDecisionLevel--;
197 }
198 #if DEBUG_VERBOSE
199 std::cerr << "after, nodepath is: " << showVector(nodepath) << "\n";
200 std::cerr << " and altpath is: " << showVector(altpath) << "\n";
201 std::cerr << " and dlTip is: " << showVector(decisionLevelTip) << "\n";
202 #endif
203 break;
204 default:
205 abort();
206 }
207 }
208
Engine()209 Engine::Engine()
210 : finished_init(false)
211 , problem(NULL)
212 , opt_var(NULL)
213 , best_sol(-1)
214 , last_prop(NULL)
215
216 , start_time(chuffed_clock::now())
217 , opt_time(duration::zero())
218 , conflicts(0)
219 , nodes(1)
220 , propagations(0)
221 , solutions(0)
222 , next_simp_db(0)
223 , output_stream(&std::cout)
224 {
225 p_queue.growTo(num_queues);
226 for (int i = 0; i < 64; i++) bit[i] = ((long long) 1 << i);
227 branching = new BranchGroup();
228 mip = new MIP();
229 }
230
newDecisionLevel()231 inline void Engine::newDecisionLevel() {
232 trail_inc++;
233 if (so.debug) {
234 std::cerr << "Engine::newDecisionLevel\n";
235 std::cerr << " trail_lim size is currently " << trail_lim.size() << "\n";
236 std::cerr << " pushing " << trail.size() << " to trail_lim\n";
237 }
238 trail_lim.push(trail.size());
239 if (so.debug) {
240 std::cerr << "trail_lim is now: " << showVec(trail_lim) << "\n";
241 }
242 sat.newDecisionLevel();
243 if (so.mip) mip->newDecisionLevel();
244 assert(dec_info.size() == decisionLevel());
245 peak_depth = max(peak_depth, decisionLevel());
246 }
247
doFixPointStuff()248 inline void Engine::doFixPointStuff() {
249 // ask other objects to do fix point things
250 for (int i = 0; i < pseudo_props.size(); i++) {
251 pseudo_props[i]->doFixPointStuff();
252 }
253 }
254
makeDecision(DecInfo & di,int alt)255 inline void Engine::makeDecision(DecInfo& di, int alt) {
256 ++nodes;
257 altpath.push_back(alt);
258 if (di.var) {
259 #if DEBUG_VERBOSE
260 std::cerr << "makeDecision: " << intVarString[(IntVar*)di.var] << " / " << di.val << " (" << alt << ")" << std::endl;
261 #endif
262 #ifdef HAS_PROFILER
263 if (doProfiling()) {
264 std::stringstream ss;
265 /* ss << intVarString[(IntVar*)di.var] << " / " << di.val << " (" << alt << ")"; */
266 ss << intVarString[(IntVar*)di.var];
267 switch (di.type) {
268 case 1: ss << "=="; break;
269 case 2: ss << ">="; break;
270 case 3: ss << "<="; break;
271 default: ss << "?="; break;
272 }
273 ss << di.val;
274 mostRecentLabel = ss.str();
275 }
276 #endif
277 ((IntVar*) di.var)->set(di.val, di.type ^ alt);
278 } else {
279 #if DEBUG_VERBOSE
280 std::cerr << "enqueing SAT literal: " << di.val << "^" << alt << " = " << (di.val ^ alt) << std::endl;
281 #endif
282 #ifdef HAS_PROFILER
283 if (doProfiling()) {
284 std::stringstream ss;
285 ss << getLitString(di.val^alt);
286 mostRecentLabel = ss.str();
287 }
288 #endif
289 sat.enqueue(toLit(di.val ^ alt));
290 }
291 if (so.ldsb && di.var && di.type == 1) ldsb.processDec(sat.trail.last()[0]);
292 // if (opt_var && di.var == opt_var && ((IntVar*) di.var)->isFixed()) printf("objective = %d\n", ((IntVar*) di.var)->getVal());
293 }
294
optimize(IntVar * v,int t)295 void optimize(IntVar* v, int t) {
296 engine.opt_var = v;
297 engine.opt_type = t;
298 engine.branching->add(v);
299 v->setPreferredVal(t == OPT_MIN ? PV_MIN : PV_MAX);
300 }
301
constrain()302 inline bool Engine::constrain() {
303 best_sol = opt_var->getVal();
304 opt_time = std::chrono::duration_cast<duration>(chuffed_clock::now() - start_time) - init_time;
305
306 sat.btToLevel(0);
307 restart_count++;
308 nodepath.resize(0);
309 altpath.resize(0);
310 /* nextnodeid = 0; */
311 #ifdef HAS_PROFILER
312 if (doProfiling()) {
313 profilerConnector->restart(restart_count);
314 }
315 #endif
316
317 if (so.parallel) {
318 Lit p = opt_type ? opt_var->getLit(best_sol+1, 2) : opt_var->getLit(best_sol-1, 3);
319 vec<Lit> ps;
320 ps.push(p);
321 Clause *c = Clause_new(ps, true);
322 slave.shareClause(*c);
323 free(c);
324 }
325
326 // printf("opt_var = %d, opt_type = %d, best_sol = %d\n", opt_var->var_id, opt_type, best_sol);
327 // printf("%% opt_var min = %d, opt_var max = %d\n", opt_var->getMin(), opt_var->getMax());
328
329 Lit p = opt_type ? opt_var->getLit(best_sol+1, 2) : opt_var->getLit(best_sol-1, 3);
330 assumptions.clear();
331 assumptions.push(toInt(p));
332
333 if (so.mip) mip->setObjective(best_sol);
334
335 /* return (opt_type ? opt_var->setMin(best_sol+1) : opt_var->setMax(best_sol-1)); */
336 return true;
337 }
338
propagate()339 bool Engine::propagate() {
340 if (async_fail) {
341 async_fail = false;
342 assert(!so.lazy || sat.confl);
343 return false;
344 }
345
346 last_prop = NULL;
347
348 WakeUp:
349
350 if (!sat.consistent() && !sat.propagate()) return false;
351
352 for (int i = 0; i < v_queue.size(); i++) {
353 v_queue[i]->wakePropagators();
354 }
355 v_queue.clear();
356
357 if (sat.confl) return false;
358
359 last_prop = NULL;
360
361 for (int i = 0; i < num_queues; i++) {
362 if (p_queue[i].size()) {
363 Propagator *p = p_queue[i].last(); p_queue[i].pop();
364 propagations++;
365 bool ok = p->propagate();
366 p->clearPropState();
367 if (!ok) return false;
368 goto WakeUp;
369 }
370 }
371
372 return true;
373 }
374
375 // Clear all uncleared intermediate propagation states
clearPropState()376 void Engine::clearPropState() {
377 for (int i = 0; i < v_queue.size(); i++) v_queue[i]->clearPropState();
378 v_queue.clear();
379
380 for (int i = 0; i < num_queues; i++) {
381 for (int j = 0; j < p_queue[i].size(); j++) p_queue[i][j]->clearPropState();
382 p_queue[i].clear();
383 }
384 }
385
btToPos(int pos)386 void Engine::btToPos(int pos) {
387 for (int i = trail.size(); i-- > pos; ) {
388 trail[i].undo();
389 }
390 trail.resize(pos);
391 }
392
btToLevel(int level)393 void Engine::btToLevel(int level) {
394 if (so.debug) {
395 std::cerr << "Engine::btToLevel( " << level << ")\n";
396 }
397 if (decisionLevel() == 0 && level == 0) return;
398 assert(decisionLevel() > level);
399
400 btToPos(trail_lim[level]);
401 trail_lim.resize(level);
402 if (so.debug) {
403 std::cerr << "trail_lim is now: " << showVec(trail_lim) << "\n";
404 }
405 dec_info.resize(level);
406 }
407
408
409
topLevelCleanUp()410 void Engine::topLevelCleanUp() {
411 trail.clear();
412
413 if (so.fd_simplify && propagations >= next_simp_db) simplifyDB();
414
415 sat.topLevelCleanUp();
416 }
417
simplifyDB()418 void Engine::simplifyDB() {
419 int cost = 0;
420 for (int i = 0; i < propagators.size(); i++) {
421 cost += propagators[i]->checkSatisfied();
422 }
423 cost += propagators.size();
424 for (int i = 0; i < vars.size(); i++) {
425 cost += vars[i]->simplifyWatches();
426 }
427 cost += vars.size();
428 cost *= 10;
429 // printf("simp db cost: %d\n", cost);
430 next_simp_db = propagations + cost;
431 }
432
blockCurrentSol()433 void Engine::blockCurrentSol() {
434 Clause& c = *Reason_new(outputs.size());
435 bool root_failure = true;
436 for (int i = 0; i < outputs.size(); i++) {
437 Var *v = (Var*) outputs[i];
438 if (v->getType() == BOOL_VAR) {
439 c[i] = ((BoolView*) outputs[i])->getValLit();
440 } else {
441 c[i] = ((IntVar*) outputs[i])->getValLit();
442 }
443 if (!sat.isRootLevel(var(c[i]))) root_failure = false;
444 assert(sat.value(c[i]) == l_False);
445 }
446 if (root_failure) sat.btToLevel(0);
447 sat.confl = &c;
448 }
449
450
getRestartLimit(unsigned int i)451 unsigned int Engine::getRestartLimit(unsigned int i) {
452 switch (so.restart_type) {
453 case NONE:
454 if (i > 1) {
455 CHUFFED_ERROR("A restart occurred while using search without restarts");
456 }
457 return UINT_MAX;
458 case CONSTANT:
459 return so.restart_scale;
460 case LINEAR:
461 return i * so.restart_scale;
462 case LUBY:
463 while (true) {
464 unsigned int exp = 0U;
465 if (i != 1U) {
466 while ( (i >> (++exp)) > 1U ) {}
467 }
468 if (i == (1U<<(exp+1))-1) {
469 return static_cast<int>(1UL << exp) * so.restart_scale;
470 }
471 i=i-(1U<<exp)+1;
472 }
473 case GEOMETRIC:
474 return so.restart_scale * ((int) pow(so.restart_base, i));
475 default:
476 i = (i+1)/2;
477 return (((i-1) & ~i) + 1) * so.restart_scale;
478 }
479 NEVER;
480 }
481
toggleVSIDS()482 void Engine::toggleVSIDS() {
483 if (!so.vsids) {
484 vec<Branching*> old_x;
485 branching->x.moveTo(old_x);
486 branching->add(&sat);
487 for (int i = 0; i < old_x.size(); i++) branching->add(old_x[i]);
488 branching->fin = 0;
489 branching->cur = -1;
490 so.vsids = true;
491 } else {
492 vec<Branching*> old_x;
493 branching->x.moveTo(old_x);
494 for (int i = 1; i < old_x.size(); i++) branching->add(old_x[i]);
495 branching->fin = 0;
496 branching->cur = -1;
497 so.vsids = false;
498 }
499 }
500
search(const std::string & problemLabel)501 RESULT Engine::search(const std::string& problemLabel) {
502 unsigned int starts = 1;
503 unsigned int nof_conflicts = getRestartLimit(starts);
504 unsigned int conflictC = 0;
505
506 if (so.print_variable_list) {
507 std::ofstream s;
508 s.open("variable-list");
509 for (auto const & p : intVarString) {
510 s << p.second << "\n";
511 }
512 for (auto const & p : boolVarString) {
513 s << p.second << "\n";
514 }
515 }
516
517 std::stringstream ss;
518 for (auto const & p : intVarString) {
519 ss << p.second << " ";
520 }
521 ss << ";";
522 for (auto const & p : boolVarString) {
523 ss << p.second << " ";
524 }
525 std::string variableListString = ss.str();
526
527 restart_count = 0;
528 #ifdef HAS_PROFILER
529 if (doProfiling()) {
530 // TODO: use 'variableListString'?
531 profilerConnector->start(problemLabel, so.cpprofiler_id, true);
532 }
533 #endif
534
535 decisionLevelTip.push_back(1);
536
537 /* boost::posix_time::ptime start_time = boost::posix_time::microsec_clock::universal_time(); */
538
539 while (true) {
540 if (so.parallel && slave.checkMessages()) return RES_UNK;
541
542 int nodeid = nextnodeid;
543 nextnodeid++;
544 int parent = (nodepath.size() == 0) ? (-1) : (nodepath[nodepath.size()-1]);
545 nodepath.push_back(nodeid);
546 int myalt = (altpath.size() == 0) ? (-1) : (altpath[altpath.size()-1]);
547 #if DEBUG_VERBOSE
548 std::cerr << "propagate (";
549 for (int i = 0 ; i < nodepath.size() ; i++)
550 std::cerr << " " << nodepath[i];
551 std::cerr << ")\n";
552 std::cerr << "altpath (";
553 for (int i = 0 ; i < altpath.size() ; i++)
554 std::cerr << " " << altpath[i];
555 std::cerr << ")\n";
556 #endif
557 if (decisionLevel() >= decisionLevelTip.size())
558 decisionLevelTip.resize(decisionLevel()+1);
559 decisionLevelTip[decisionLevel()] = nodepath.size();
560 #if DEBUG_VERBOSE
561 std::cerr << "setting decisionLevelTip[" << decisionLevel() << "] to " << nodepath.size() << "\n";
562 #endif
563
564 int previousDecisionLevel = decisionLevel();
565
566 bool propResult = propagate();
567 /* boost::posix_time::ptime current_time = boost::posix_time::microsec_clock::universal_time(); */
568 /* boost::posix_time::time_duration dur = current_time - start_time; */
569 long timeus = 0;
570 // long timeus = dur.total_microseconds();
571 if (!propResult) {
572 #if DEBUG_VERBOSE
573 std::cerr << "failure\n";
574 std::cerr << "createNode(" << nodeid << ", " << parent << ", " << myalt << ", 0, NodeStatus::FAILED)\n";
575 std::cerr << "label: " << mostRecentLabel << "\n";
576 std::cerr << "restart: " << restart_count << "\n";
577 #endif
578 /* c.createNode(nodeid, parent, myalt, 0, FAILED).set_label(mostRecentLabel).send(); */
579 /* mostRecentLabel = ""; */
580
581 clearPropState();
582
583 Conflict:
584 conflicts++; conflictC++;
585
586 if (so.time_out > duration(0) && chuffed_clock::now() > time_out) {
587 (*output_stream) << "% Time limit exceeded!\n";
588 return RES_UNK;
589 }
590
591 if (decisionLevel() == 0) {
592 #ifdef HAS_PROFILER
593 if (doProfiling()) {
594 sendNode(profilerConnector
595 ->createNode({nodeid, restart_count, 0},
596 {parent, restart_count, 0}, myalt, 0,
597 cpprofiler::NodeStatus::FAILED)
598 // .set_time(timeus)
599 .set_label(mostRecentLabel));
600 // .set_decision_level(previousDecisionLevel));
601 mostRecentLabel = "";
602 }
603 #endif
604 return RES_GUN;
605 }
606
607
608 // Derive learnt clause and perform backjump
609 if (so.lazy) {
610 std::set<int> contributingNogoods;
611 sat.analyze(nodeid, contributingNogoods);
612 #ifdef HAS_PROFILER
613 if (doProfiling()) {
614 std::stringstream ss;
615 for (int i = 0 ; i < sat.out_learnt.size() ; i++)
616 ss << " " << getLitString(toInt(sat.out_learnt[i]));
617 std::stringstream contribString;
618 contribString << "{\"nogoods\":[";
619 for (std::set<int>::const_iterator it = contributingNogoods.begin() ;
620 it != contributingNogoods.end() ;
621 it++) {
622 contribString << (it == contributingNogoods.begin() ? "" : ",") << *it;
623 }
624 contribString << "],";
625 contribString << "\"blocks\":[";
626 // We leave duplicates in the list of blocks, so
627 // that the profiler can make use of them.
628 std::set<int> levels;
629 for (int i = 0 ; i < sat.out_learnt_level.size() ; i++) {
630 int rawLevel = sat.out_learnt_level[i];
631 // We increment the "raw level" by one,
632 // because internally (on the trail) the first
633 // decision level -- that is, after a single
634 // search decision has been made -- is called
635 // zero. We would rather that it be called
636 // one, to equal the number of decisions made.
637 int adjustedLevel = rawLevel + 1;
638 contribString << ((i==0) ? "" : ",") << adjustedLevel;
639 levels.insert(adjustedLevel);
640 }
641 contribString << "]}";
642
643 // Calculate block level distance.
644 int bld = levels.size();
645
646 // Does this nogood involve literals that are
647 // derived from assumption literals?
648 int numAssumptions = assumptions.size();
649 bool usesAssumptions = false;
650 for (int i = 0 ; i < sat.out_learnt_level.size() ; i++) {
651 if (sat.out_learnt_level[i] < numAssumptions) {
652 usesAssumptions = true;
653 }
654 }
655
656 if (so.debug) {
657 std::cerr << "uses assumptions: " << usesAssumptions << "\n";
658 }
659
660 int backjumpDistance = previousDecisionLevel - decisionLevel();
661
662 if (doProfiling()) {
663 sendNode(profilerConnector
664 ->createNode({nodeid, restart_count, 0},
665 {parent, restart_count, 0},
666 myalt, 0,
667 cpprofiler::NodeStatus::FAILED)
668 // .set_time(timeus)
669 .set_label(mostRecentLabel)
670 .set_nogood(ss.str())
671 // .set_nogood_bld(bld)
672 // .set_uses_assumptions(usesAssumptions)
673 .set_info(contribString.str()));
674 // .set_backjump_distance(backjumpDistance)
675 // .set_decision_level(previousDecisionLevel));
676 }
677 mostRecentLabel = "";
678 #if DEBUG_VERBOSE
679 std::cerr << "after analyze, decisionLevel() is " << decisionLevel() << "\n";
680 std::cerr << "decisionLevelTip:";
681 for (int i = 0 ; i < decisionLevelTip.size() ; i++)
682 std::cerr << " " << decisionLevelTip[i];
683 std::cerr << "\n";
684 #endif
685
686 rewindPaths(previousDecisionLevel, decisionLevel(), (so.send_skipped ? REWIND_SEND_SKIPPED : REWIND_OMIT_SKIPPED), timeus);
687
688 std::stringstream ss2;
689 /* ss2 << "-> "; */
690 string ls = getLitString(toInt(sat.out_learnt[0]));
691 ss2 << ls;
692 if (ls.size() < 2) {
693 std::cerr << "WARNING: short label for " << toInt(sat.out_learnt[0]) << ": " << ls << "\n";
694 }
695 mostRecentLabel = ss2.str();
696 altpath.push_back(1);
697 }
698 #endif
699 } else {
700 #ifdef HAS_PROFILER
701 if (doProfiling()) {
702 sendNode(profilerConnector
703 ->createNode({nodeid, restart_count, 0},
704 {parent, restart_count, 0}, myalt, 0,
705 cpprofiler::NodeStatus::FAILED)
706 // .set_time(timeus)
707 .set_label(mostRecentLabel));
708 // .set_decision_level(previousDecisionLevel));
709 mostRecentLabel = "";
710 }
711 #endif
712 sat.confl = NULL;
713 DecInfo& di = dec_info.last();
714 sat.btToLevel(decisionLevel()-1);
715 #ifdef HAS_PROFILER
716 if (doProfiling()) {
717 rewindPaths(previousDecisionLevel, decisionLevel(), (so.send_skipped ? REWIND_SEND_SKIPPED : REWIND_OMIT_SKIPPED), timeus);
718 }
719 #endif
720 makeDecision(di, 1);
721 }
722
723 if (!so.vsids && !so.toggle_vsids && conflictC >= so.switch_to_vsids_after) {
724 if (so.restart_scale >= 1000000000) so.restart_scale = 100;
725 if (so.verbosity >= 2)
726 std::cerr << "restarting and switching to VSIDS\n";
727 sat.btToLevel(0);
728 restart_count++;
729 nodepath.resize(0);
730 altpath.resize(0);
731 /* nextnodeid = 0; */
732 #ifdef HAS_PROFILER
733 if (doProfiling()) {
734 profilerConnector->restart(restart_count);
735 }
736 #endif
737 toggleVSIDS();
738 }
739
740 } else {
741
742 if (conflictC >= nof_conflicts) {
743 if (so.verbosity >= 2)
744 std::cerr << "restarting due to number of conflicts\n";
745 starts++;
746 nof_conflicts += getRestartLimit(starts);
747 sat.btToLevel(0);
748 restart_count++;
749 nodepath.resize(0);
750 altpath.resize(0);
751 /* nextnodeid = 0; */
752 #ifdef HAS_PROFILER
753 if (doProfiling()) {
754 profilerConnector->restart(restart_count);
755 }
756 #endif
757
758 sat.confl = NULL;
759 if (so.lazy && so.toggle_vsids && (starts % 2 == 1)) toggleVSIDS();
760 continue;
761 }
762
763 if (decisionLevel() == 0) {
764 topLevelCleanUp();
765 if (opt_var && so.verbosity >= 3) {
766 printf("%% root level bounds on objective: min %d max %d\n", opt_var->getMin(), opt_var->getMax());
767 }
768 }
769
770 DecInfo *di = NULL;
771
772 // Propagate assumptions
773 while (decisionLevel() < assumptions.size()) {
774 int p = assumptions[decisionLevel()];
775 if (sat.value(toLit(p)) == l_True) {
776 // Dummy decision level:
777 assert(sat.trail.last().size() == sat.qhead.last());
778 engine.dec_info.push(DecInfo(NULL, p));
779 newDecisionLevel();
780 } else if (sat.value(toLit(p)) == l_False) {
781 return RES_LUN;
782 } else {
783 di = new DecInfo(NULL, p);
784 break;
785 }
786 }
787
788 if (!di) di = branching->branch();
789
790 if (!di) {
791 solutions++;
792 if (std::stringstream* oss = dynamic_cast<std::stringstream*>(output_stream)) {
793 oss->str("");
794 }
795 if (so.print_sol) {
796 problem->print(*output_stream);
797 (*output_stream) << "\n----------\n";
798 output_stream->flush();
799 }
800 #if DEBUG_VERBOSE
801 std::cerr << "solution\n";
802 std::cerr << "createNode(" << nodeid << ", " << parent << ", " << myalt << ", 0, SOLVED)\n";
803 std::cerr << "label: " << mostRecentLabel << "\n";
804 #endif
805
806 #ifdef HAS_PROFILER
807 if (doProfiling()) {
808 FlatZinc::FlatZincSpace *fzs = dynamic_cast<FlatZinc::FlatZincSpace*>(problem);
809 if (fzs != NULL) {
810 std::stringstream s;
811 fzs->printDomains(s);
812 sendNode(
813 profilerConnector
814 ->createNode({nodeid, restart_count, 0},
815 {parent, restart_count, 0}, myalt,
816 0, cpprofiler::NodeStatus::SOLVED)
817 // .set_time(timeus)
818 .set_label(mostRecentLabel)
819 // .set_decision_level(previousDecisionLevel)
820 .set_info(s.str()));
821 }
822 else {
823 sendNode(profilerConnector
824 ->createNode({nodeid, restart_count, 0},
825 {parent, restart_count, 0},
826 myalt, 0,
827 cpprofiler::NodeStatus::SOLVED)
828 // .set_time(timeus)
829 // .set_decision_level(previousDecisionLevel)
830 .set_label(mostRecentLabel));
831 }
832 }
833 //FlatZinc::FlatZincSpace *fzs = dynamic_cast<FlatZinc::FlatZincSpace*>(problem);
834 //if (fzs != NULL) {
835 // std::stringstream s;
836 // fzs->printDomains(s);
837 // if (doProfiling()) {
838 // sendNode(profilerConnector.createNode(nodeid, parent, myalt, 0, SOLVED)
839 // .set_time(timeus)
840 // .set_label(mostRecentLabel)
841 // .set_info(s.str())
842 // .set_decision_level(previousDecisionLevel)
843 // .set_restart_id(restart_count));
844 // }
845 //} else {
846 // if (doProfiling()) {
847 // sendNode(profilerConnector.createNode(nodeid, parent, myalt, 0, SOLVED)
848 // .set_time(timeus)
849 // .set_label(mostRecentLabel)
850 // .set_decision_level(previousDecisionLevel)
851 // .set_restart_id(restart_count));
852 // }
853 //}
854 #endif
855
856 mostRecentLabel = "";
857 if (!opt_var) {
858 if (solutions == so.nof_solutions) return RES_SAT;
859 if (so.lazy) blockCurrentSol();
860 goto Conflict;
861 }
862 if (!constrain()) {
863 return RES_GUN;
864 }
865 continue;
866 }
867
868
869 engine.dec_info.push(*di);
870 newDecisionLevel();
871
872 doFixPointStuff();
873
874 #if DEBUG_VERBOSE
875 std::cerr << "createNode(" << nodeid << ", " << parent << ", " << myalt << ", 2, NodeStatus::BRANCH)\n";
876 std::cerr << "label: " << mostRecentLabel << "\n";
877 #endif
878 #ifdef HAS_PROFILER
879 if (doProfiling()) {
880 string info;
881 if (so.send_domains) {
882 FlatZinc::FlatZincSpace* fzs = dynamic_cast<FlatZinc::FlatZincSpace*>(problem);
883 if (fzs != NULL) {
884 info = fzs->getDomainsString();
885 }
886 }
887
888 sendNode(profilerConnector
889 ->createNode({nodeid, restart_count, 0},
890 {parent, restart_count, 0}, myalt, 2,
891 cpprofiler::NodeStatus::BRANCH)
892 .set_label(mostRecentLabel)
893 // .set_decision_level(previousDecisionLevel)
894 .set_info(info));
895 mostRecentLabel = "";
896 }
897 #endif
898
899 makeDecision(*di, 0);
900
901 delete di;
902
903 }
904 }
905 }
906
solve(Problem * p,const std::string & problemLabel)907 void Engine::solve(Problem *p, const std::string& problemLabel) {
908 problem = p;
909
910 // Setting the random seed
911 if (so.rnd_seed == 0) {
912 so.rnd_seed = time(0);
913 }
914 srand(so.rnd_seed);
915
916
917 init();
918
919 time_out = chuffed_clock::now() + so.time_out;
920
921 init_time = std::chrono::duration_cast<duration>(chuffed_clock::now() - start_time);
922 base_memory = memUsed();
923
924 #ifdef HAS_PROFILER
925 profilerConnector = new cpprofiler::Connector(so.cpprofiler_port);
926 if (so.cpprofiler_enabled) {
927 profilerConnector->connect();
928 }
929 #endif
930
931 /* if (so.debug) { */
932 /* for (int i = 0 ; i < 2*sat.nVars() ; i++) { */
933 /* std::cerr << "literal " << i << " is " << litString[i] << "\n"; */
934 /* } */
935 /* } */
936
937 if (so.learnt_stats) {
938 learntStatsStream.open("learnt-stats.csv");
939 learntStatsStream << "id,length,block";
940 if (so.learnt_stats_nogood)
941 learntStatsStream << ",nogood";
942 learntStatsStream << ",rawActivity\n";
943 }
944
945 if (!so.parallel) {
946 // sequential
947 status = search(problemLabel);
948 if (status == RES_GUN || status == RES_LUN) {
949 if (solutions > 0)
950 (*output_stream) << "==========\n";
951 else
952 (*output_stream) << "=====UNSATISFIABLE=====\n";
953 }
954 } else {
955 // parallel
956 if (so.thread_no == -1) master.solve();
957 else slave.solve();
958 if (so.thread_no == -1 && master.status == RES_GUN) (*output_stream) << "==========\n";
959 }
960
961 if (so.learnt_stats) {
962 for (int i = 0 ; i < sat.learnts.size() ; i++) {
963 Clause& c = *(sat.learnts[i]);
964 // std::cerr << "clausescore," << c.clauseID() << ","
965 // << c.rawActivity() << "\n";
966 int id = c.clauseID();
967 learntStatsStream << learntClauseString[id];
968 learntStatsStream << ",";
969 learntStatsStream << c.rawActivity();
970 learntStatsStream << "\n";
971 }
972 }
973
974 #ifdef HAS_PROFILER
975 if (doProfiling()) {
976 profilerConnector->done();
977 if (profilerConnector->connected()) {
978 profilerConnector->disconnect();
979 }
980 }
981 delete profilerConnector;
982 #endif
983
984 if (so.verbosity >= 1) printStats();
985
986 if (so.parallel) master.finalizeMPI();
987 }
988