1 #include <cstdio>
2 #include <algorithm>
3 #include <cassert>
4 #include <chuffed/core/options.h>
5 #include <chuffed/core/engine.h>
6 #include <chuffed/core/sat.h>
7 #include <chuffed/core/propagator.h>
8 #include <chuffed/mip/mip.h>
9 #include <chuffed/parallel/parallel.h>
10
11 #include <iostream>
12 #include <sstream>
13 #include <fstream>
14
15 #define PRINT_ANALYSIS 0
16
17 SAT sat;
18
19 std::map<int,std::string> litString;
20
21 std::map<int,string> learntClauseString;
22 std::ofstream learntStatsStream;
23
24 cassert(sizeof(Lit) == 4);
25 cassert(sizeof(Clause) == 4);
26 cassert(sizeof(WatchElem) == 8);
27 cassert(sizeof(Reason) == 8);
28
29 //---------
30 // inline methods
31
32
33
insertVarOrder(int x)34 inline void SAT::insertVarOrder(int x) {
35 if (!order_heap.inHeap(x) && flags[x].decidable) order_heap.insert(x);
36 }
37
setConfl(Lit p,Lit q)38 inline void SAT::setConfl(Lit p, Lit q) {
39 (*short_confl)[0] = p;
40 (*short_confl)[1] = q;
41 confl = short_confl;
42 }
43
untrailToPos(vec<Lit> & t,int p)44 inline void SAT::untrailToPos(vec<Lit>& t, int p) {
45 int dl = decisionLevel();
46
47 for (int i = t.size(); i-- > p; ) {
48 int x = var(t[i]);
49 assigns[x] = toInt(l_Undef);
50 #if PHASE_SAVING
51 if (so.phase_saving >= 1 || (so.phase_saving == 1 && dl >= l0))
52 polarity[x] = sign(t[i]);
53 #endif
54 insertVarOrder(x);
55 }
56 t.resize(p);
57 }
58
59 //---------
60 // main methods
61
62
SAT()63 SAT::SAT() :
64 lit_sort(trailpos)
65 , pushback_time(duration::zero())
66 , trail(1)
67 , qhead(1,0)
68 , rtrail(1)
69 , confl(NULL)
70 , var_inc(1)
71 , cla_inc(1)
72 , order_heap(VarOrderLt(activity))
73 , bin_clauses(0)
74 , tern_clauses(0)
75 , long_clauses(0)
76 , learnt_clauses(0)
77 , propagations(0)
78 , back_jumps(0)
79 , nrestarts(0)
80 , next_simp_db(100000)
81 , clauses_literals(0)
82 , learnts_literals(0)
83 , max_literals(0)
84 , tot_literals(0)
85 , avg_depth(100)
86 , confl_rate(1000)
87 , ll_time(chuffed_clock::now())
88 , ll_inc(1)
89 , learnt_len_el(10)
90 , learnt_len_occ(MAX_SHARE_LEN,learnt_len_el*1000/MAX_SHARE_LEN)
91 {
92 newVar(); enqueue(Lit(0,1));
93 newVar(); enqueue(Lit(1,0));
94 temp_sc = (SClause*) malloc(TEMP_SC_LEN * sizeof(int));
95 short_expl = (Clause*) malloc(sizeof(Clause) + 3 * sizeof(Lit));
96 short_confl = (Clause*) malloc(sizeof(Clause) + 2 * sizeof(Lit));
97 short_expl->clearFlags();
98 short_confl->clearFlags();
99 short_confl->sz = 2;
100 }
101
~SAT()102 SAT::~SAT() {
103 for (int i = 0; i < clauses.size(); i++) free(clauses[i]);
104 for (int i = 0; i < learnts.size(); i++) free(learnts[i]);
105 }
106
init()107 void SAT::init() {
108 orig_cutoff = nVars();
109 ivseen.growTo(engine.vars.size(), false);
110 }
111
newVar(int n,ChannelInfo ci)112 int SAT::newVar(int n, ChannelInfo ci) {
113 int s = assigns.size();
114
115 watches .growBy(n);
116 watches .growBy(n);
117 assigns .growBy(n, toInt(l_Undef));
118 reason .growBy(n, NULL);
119 trailpos .growBy(n, -1);
120 seen .growBy(n, 0);
121 activity .growBy(n, 0);
122 polarity .growBy(n, 1);
123 flags .growBy(n, 7);
124
125 for (int i = 0; i < n; i++) {
126 c_info.push(ci);
127 ci.val++;
128 insertVarOrder(s+i);
129 }
130
131 return s;
132 }
133
getLazyVar(ChannelInfo ci)134 int SAT::getLazyVar(ChannelInfo ci) {
135 int v;
136 if (var_free_list.size()) {
137 v = var_free_list.last();
138 var_free_list.pop();
139 fprintf(stderr, "reuse %d\n", v);
140 assert(assigns[v] == toInt(l_Undef));
141 assert(watches[2*v].size() == 0);
142 assert(watches[2*v+1].size() == 0);
143 assert(num_used[v] == 0);
144 c_info[v] = ci;
145 activity[v] = 0;
146 polarity[v] = 1;
147 flags[v] = 7;
148 } else {
149 v = newVar(1, ci);
150 num_used.push(0);
151 }
152 // flags[v].setDecidable(false);
153 return v;
154 }
155
removeLazyVar(int v)156 void SAT::removeLazyVar(int v) {
157 return;
158 ChannelInfo& ci = c_info[v];
159 assert(assigns[v] == toInt(l_Undef));
160 assert(watches[2*v].size() == 0);
161 assert(watches[2*v+1].size() == 0);
162 fprintf(stderr, "free %d\n", v);
163 var_free_list.push(v);
164 if (ci.cons_type == 1) {
165 ((IntVarLL*) engine.vars[ci.cons_id])->freeLazyVar(ci.val);
166 } else if (ci.cons_type == 2) {
167 engine.propagators[ci.cons_id]->freeLazyVar(ci.val);
168 } else NEVER;
169 }
170
addClause(Lit p,Lit q)171 void SAT::addClause(Lit p, Lit q) {
172 if (value(p) == l_True || value(q) == l_True) return;
173 if (value(p) == l_False && value(q) == l_False) {
174 assert(false);
175 TL_FAIL();
176 }
177 if (value(p) == l_False) {
178 assert(decisionLevel() == 0);
179 enqueue(q);
180 return;
181 }
182 if (value(q) == l_False) {
183 assert(decisionLevel() == 0);
184 enqueue(p);
185 return;
186 }
187 bin_clauses++;
188 watches[toInt(~p)].push(q);
189 watches[toInt(~q)].push(p);
190 }
191
addClause(vec<Lit> & ps,bool one_watch)192 void SAT::addClause(vec<Lit>& ps, bool one_watch) {
193 int i, j;
194 for (i = j = 0; i < ps.size(); i++) {
195 if (value(ps[i]) == l_True) return;
196 if (value(ps[i]) == l_Undef) ps[j++] = ps[i];
197 }
198 ps.resize(j);
199 if (ps.size() == 0) {
200 assert(false);
201 TL_FAIL();
202 }
203 addClause(*Clause_new(ps), one_watch);
204 }
205
addClause(Clause & c,bool one_watch)206 void SAT::addClause(Clause& c, bool one_watch) {
207 assert(c.size() > 0);
208 if (c.size() == 1) {
209 assert(decisionLevel() == 0);
210 if (DEBUG) fprintf(stderr, "warning: adding length 1 clause!\n");
211 if (value(c[0]) == l_False) TL_FAIL();
212 if (value(c[0]) == l_Undef) enqueue(c[0]);
213 free(&c);
214 return;
215 }
216 if (!c.learnt) {
217 if (c.size() == 2) bin_clauses++;
218 else if (c.size() == 3) tern_clauses++;
219 else long_clauses++;
220 }
221
222 // Mark lazy lits which are used
223 if (c.learnt) for (int i = 0; i < c.size(); i++) incVarUse(var(c[i]));
224
225 if (c.size() == 2 && ((!c.learnt) || (so.bin_clause_opt))) {
226 if (!one_watch) watches[toInt(~c[0])].push(c[1]);
227 watches[toInt(~c[1])].push(c[0]);
228 if (!c.learnt) free(&c);
229 return;
230 }
231 if (!one_watch) watches[toInt(~c[0])].push(&c);
232 watches[toInt(~c[1])].push(&c);
233 if (c.learnt) learnts_literals += c.size();
234 else clauses_literals += c.size();
235 if (c.learnt) {
236 learnts.push(&c);
237 if (so.learnt_stats) {
238 std::set<int> levels;
239 for (int i = 0 ; i < c.size() ; i++) {
240 levels.insert(out_learnt_level[i]);
241 }
242 std::stringstream s;
243 // s << "learntclause,";
244 s << c.clauseID() << "," << c.size() << "," << levels.size();
245 if (so.learnt_stats_nogood) {
246 s << ",";
247 for (int i = 0 ; i < c.size() ; i++) {
248 s << (i == 0 ? "" : " ") << getLitString(toInt(c[i]));
249 // s << " (" << out_learnt_level[i] << ")";
250 }
251 }
252 //std::cerr << "\n";
253 learntClauseString[c.clauseID()] = s.str();
254 }
255 } else {
256 clauses.push(&c);
257 }
258 }
259
removeClause(Clause & c)260 void SAT::removeClause(Clause& c) {
261 assert(c.size() > 1);
262 watches[toInt(~c[0])].remove(&c);
263 watches[toInt(~c[1])].remove(&c);
264 if (c.learnt) learnts_literals -= c.size();
265 else clauses_literals -= c.size();
266
267 if (c.learnt) for (int i = 0; i < c.size(); i++) decVarUse(var(c[i]));
268
269 if (c.learnt) {
270 // learntClauseScore[c.clauseID()] = c.rawActivity();
271 /* if (so.debug) { */
272 if (so.learnt_stats) {
273 int id = c.clauseID();
274 learntStatsStream << learntClauseString[id];
275 learntStatsStream << ",";
276 learntStatsStream << c.rawActivity();
277 learntStatsStream << "\n";
278 /* std::cerr << "clausescore," << << "," << c.rawActivity() << "\n"; */
279 }
280 /* } */
281 }
282
283 free(&c);
284 }
285
286
topLevelCleanUp()287 void SAT::topLevelCleanUp() {
288 assert(decisionLevel() == 0);
289
290 for (int i = rtrail[0].size(); i-- > 0; ) free(rtrail[0][i]);
291 rtrail[0].clear();
292
293 if (so.sat_simplify && propagations >= next_simp_db) simplifyDB();
294
295 for (int i = 0; i < trail[0].size(); i++) {
296 if (so.debug) {
297 std::cerr << "setting true at top-level: " << getLitString(toInt(trail[0][i])) << "\n";
298 }
299 seen[var(trail[0][i])] = true;
300 trailpos[var(trail[0][i])] = -1;
301 }
302 trail[0].clear();
303 qhead[0] = 0;
304
305 }
306
simplifyDB()307 void SAT::simplifyDB() {
308 int i, j;
309 for (i = j = 0; i < learnts.size(); i++) {
310 if (simplify(*learnts[i])) removeClause(*learnts[i]);
311 else learnts[j++] = learnts[i];
312 }
313 learnts.resize(j);
314 next_simp_db = propagations + clauses_literals + learnts_literals;
315 }
316
simplify(Clause & c)317 bool SAT::simplify(Clause& c) {
318 if (value(c[0]) == l_True) return true;
319 if (value(c[1]) == l_True) return true;
320 int i, j;
321 for (i = j = 2; i < c.size(); i++) {
322 if (value(c[i]) == l_True) return true;
323 if (value(c[i]) == l_Undef) c[j++] = c[i];
324 }
325 c.resize(j);
326 return false;
327 }
328
showReason(Reason r)329 string showReason(Reason r) {
330 std::stringstream ss;
331 switch (r.d.type) {
332 case 0:
333 if (r.pt == NULL) {
334 ss << "no reason";
335 } else {
336 Clause& c = *r.pt;
337 ss << "clause";
338 for (int i = 0 ; i < c.size() ; i++) {
339 ss << " " << getLitString(toInt(~c[i]));
340 }
341 }
342 break;
343 case 1: ss << "absorbed binary clause?"; break;
344 case 2: ss << "single literal " << getLitString(toInt(~toLit(r.d.d1))); break;
345 case 3: ss << "two literals " << getLitString(toInt(~toLit((r.d.d1)))) << " & " << getLitString(toInt(~toLit((r.d.d2)))); break;
346 }
347 return ss.str();
348 }
349
350 // Use cases:
351 // enqueue from decision , value(p) = u , r = NULL , channel
352 // enqueue from analyze , value(p) = u , r != NULL, channel
353 // enqueue from unit prop , value(p) = u , r != NULL, channel
354
enqueue(Lit p,Reason r)355 void SAT::enqueue(Lit p, Reason r) {
356 /* if (so.debug) { */
357 /* std::cerr << "enqueue literal " << getLitString(toInt(p)) << " because " << showReason(r) << "\n"; */
358 /* } */
359 assert(value(p) == l_Undef);
360 int v = var(p);
361 assigns [v] = toInt(lbool(!sign(p)));
362 trailpos[v] = engine.trailPos();
363 reason [v] = r;
364 trail.last().push(p);
365 ChannelInfo& ci = c_info[v];
366 if (ci.cons_type == 1) engine.vars[ci.cons_id]->channel(ci.val, ci.val_type, sign(p));
367 }
368
369 // enqueue from FD variable, value(p) = u/f, r = ?, don't channel
370
cEnqueue(Lit p,Reason r)371 void SAT::cEnqueue(Lit p, Reason r) {
372 /* if (so.debug) { */
373 /* std::cerr << "c-enqueue literal " << getLitString(toInt(p)) << " because " << showReason(r) << "\n"; */
374 /* } */
375 assert(value(p) != l_True);
376 int v = var(p);
377 if (value(p) == l_False) {
378 if (so.lazy) {
379 if (r == NULL) {
380 assert(decisionLevel() == 0);
381 setConfl();
382 } else {
383 confl = getConfl(r, p);
384 (*confl)[0] = p;
385 }
386 } else setConfl();
387 return;
388 }
389 assigns [v] = toInt(lbool(!sign(p)));
390 trailpos[v] = engine.trailPos();
391 reason [v] = r;
392 trail.last().push(p);
393 }
394
395
aEnqueue(Lit p,Reason r,int l)396 void SAT::aEnqueue(Lit p, Reason r, int l) {
397 if (so.debug) {
398 std::cerr << "a-enqueue literal " << getLitString(toInt(p)) << " because " << showReason(r) << " and l=" << l << "\n";
399 }
400 assert(value(p) == l_Undef);
401 int v = var(p);
402 assigns [v] = toInt(lbool(!sign(p)));
403 trailpos[v] = engine.trail_lim[l]-1;
404 reason [v] = r;
405 trail[l].push(p);
406 }
407
btToLevel(int level)408 void SAT::btToLevel(int level) {
409 #if DEBUG_VERBOSE
410 std::cerr << "SAT::btToLevel( " << level << ")\n";
411 #endif
412 if (decisionLevel() <= level) return;
413
414 for (int l = trail.size(); l-- > level+1; ) {
415 untrailToPos(trail[l], 0);
416 for (int i = rtrail[l].size(); i--; ) {
417 free(rtrail[l][i]);
418 }
419 }
420 trail.resize(level+1);
421 qhead.resize(level+1);
422 rtrail.resize(level+1);
423
424 engine.btToLevel(level);
425 if (so.mip) mip->btToLevel(level);
426
427 }
428
btToPos(int sat_pos,int core_pos)429 void SAT::btToPos(int sat_pos, int core_pos) {
430 untrailToPos(trail.last(), sat_pos);
431 engine.btToPos(core_pos);
432 }
433
434
435 // Propagator methods:
436
propagate()437 bool SAT::propagate() {
438 int num_props = 0;
439
440 int& qhead = this->qhead.last();
441 vec<Lit>& trail = this->trail.last();
442
443 while (qhead < trail.size()) {
444 num_props++;
445
446 Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate.
447 vec<WatchElem>& ws = watches[toInt(p)];
448
449 if (ws.size() == 0) continue;
450
451 WatchElem *i, *j, *end;
452
453 for (i = j = ws, end = i + ws.size(); i != end; ) {
454 WatchElem& we = *i;
455 switch (we.d.type) {
456 case 1: {
457 // absorbed binary clause
458 *j++ = *i++;
459 Lit q = toLit(we.d.d2);
460 switch (toInt(value(q))) {
461 case 0: enqueue(q, ~p); break;
462 case -1:
463 setConfl(q, ~p);
464 qhead = trail.size();
465 while (i < end) *j++ = *i++;
466 break;
467 default:;
468 }
469 continue;
470 }
471 case 2: {
472 // wake up FD propagator
473 *j++ = *i++;
474 engine.propagators[we.d.d2]->wakeup(we.d.d1, 0);
475 continue;
476 }
477 default:
478 Clause& c = *we.pt;
479 i++;
480
481 // Check if already satisfied
482 if (value(c[0]) == l_True || value(c[1]) == l_True) {
483 *j++ = &c;
484 continue;
485 }
486
487 Lit false_lit = ~p;
488
489 // Make sure the false literal is data[1]:
490 if (c[0] == false_lit) c[0] = c[1], c[1] = false_lit;
491
492 // Look for new watch:
493 for (int k = 2; k < c.size(); k++)
494 if (value(c[k]) != l_False) {
495 c[1] = c[k]; c[k] = false_lit;
496 watches[toInt(~c[1])].push(&c);
497 goto FoundWatch;
498 }
499
500 // Did not find watch -- clause is unit under assignment:
501 *j++ = &c;
502 if (value(c[0]) == l_False) {
503 confl = &c;
504 qhead = trail.size();
505 while (i < end) *j++ = *i++;
506 } else {
507 enqueue(c[0], &c);
508 }
509 FoundWatch:;
510 }
511 }
512 ws.shrink(i-j);
513 }
514 propagations += num_props;
515
516 return (confl == NULL);
517 }
518
operator ()activity_lt519 struct activity_lt { bool operator() (Clause* x, Clause* y) { return x->activity() < y->activity(); } };
reduceDB()520 void SAT::reduceDB() {
521 int i, j;
522
523 std::sort((Clause**) learnts, (Clause**) learnts + learnts.size(), activity_lt());
524
525 for (i = j = 0; i < learnts.size()/2; i++) {
526 if (!locked(*learnts[i])) removeClause(*learnts[i]);
527 else learnts[j++] = learnts[i];
528 }
529 for (; i < learnts.size(); i++) {
530 learnts[j++] = learnts[i];
531 }
532 learnts.resize(j);
533
534 if (so.verbosity >= 1) printf("%% Pruned %d learnt clauses\n", i-j);
535 }
536
showClause(Clause & c)537 std::string showClause(Clause& c) {
538 std::stringstream ss;
539 for (int i = 0 ; i < c.size() ; i++)
540 ss << " " << getLitString(toInt(c[i]));
541 return ss.str();
542 }
543
operator ()raw_activity_gt544 struct raw_activity_gt { bool operator() (Clause* x, Clause* y) { return x->rawActivity() > y->rawActivity(); } };
545 // This is wrong, because probably most of the clauses have been
546 // removed by the time we do this.
printLearntStats()547 void SAT::printLearntStats() {
548 /* std::ofstream clausefile("clause-info.csv"); */
549 /* for (int i = 0 ; i < learnts.size() ; i++) { */
550 /* clausefile << learnts[i]->clauseID() << "," << learnts[i]->rawActivity() << "," << showClause(*learnts[i]) << "\n"; */
551 /* } */
552
553 std::sort((Clause**) learnts, (Clause**) learnts + learnts.size(), raw_activity_gt());
554 std::cerr << "top ten clauses:\n";
555 for (int i = 0 ; i < 10 && i < learnts.size() ; i++) {
556 std::cerr << i << ": " << learnts[i]->rawActivity() << " " << showClause(*learnts[i]) << "\n";
557 }
558
559 }
560
printStats()561 void SAT::printStats() {
562 printf("%%%%%%mzn-stat: binClauses=%d\n", bin_clauses);
563 printf("%%%%%%mzn-stat: ternClauses=%d\n", tern_clauses);
564 printf("%%%%%%mzn-stat: longClauses=%d\n", long_clauses);
565 printf("%%%%%%mzn-stat: avgLongClauseLen=%.2f\n", long_clauses ? (double) (clauses_literals - 3*tern_clauses) / long_clauses : 0);
566 printf("%%%%%%mzn-stat: learntClauses=%d\n", learnts.size());
567 printf("%%%%%%mzn-stat: avgLearntClauseLen=%.2f\n", learnts.size() ? (double) learnts_literals / learnts.size() : 0);
568 printf("%%%%%%mzn-stat: satPropagations=%lld\n", propagations);
569 printf("%%%%%%mzn-stat: naturalRestarts=%lld\n", nrestarts);
570 if (so.ldsb) {
571 printf("%%%%%%mzn-stat: pushbackTime=%.3f\n", to_sec(pushback_time));
572 }
573 }
574
575
576 //-----
577 // Branching methods
578
finished()579 bool SAT::finished() {
580 assert(so.vsids);
581 while (!order_heap.empty()) {
582 int x = order_heap[0];
583 if (!assigns[x] && flags[x].decidable) return false;
584 order_heap.removeMin();
585 }
586 return true;
587 }
588
branch()589 DecInfo* SAT::branch() {
590 if (!so.vsids) return NULL;
591
592 assert(!order_heap.empty());
593
594 int next = order_heap.removeMin();
595
596 assert(!assigns[next]);
597 assert(flags[next].decidable);
598
599 return new DecInfo(NULL, 2*next+polarity[next]);
600 }
601
602 //-----
603 // Parallel methods
604
updateShareParam()605 void SAT::updateShareParam() {
606 so.share_param = 16;
607 /*
608 double bmax = so.bandwidth / so.num_threads;
609 double bsum = 0;
610 // printf("Update share param\n");
611 double factor = learnt_len_el * (ll_inc-0.5);
612 for (int i = 0; i < MAX_SHARE_LEN; i++) {
613 double lps = learnt_len_occ[i]/factor*i;
614 // printf("%.3f, ", lps);
615 if (bsum + lps > bmax) {
616 so.share_param = i-1 + (bmax - bsum) / lps;
617 if (so.share_param < 1) so.share_param = 1;
618 return;
619 }
620 bsum += lps;
621 }
622 so.share_param = MAX_SHARE_LEN;
623 // if (rand()%100 == 0) printf("share param = %.1f\n", so.share_param);
624 */
625 }
626