-
Notifications
You must be signed in to change notification settings - Fork 121
/
propagate.cpp
568 lines (442 loc) · 17.5 KB
/
propagate.cpp
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
#include "internal.hpp"
namespace CaDiCaL {
/*------------------------------------------------------------------------*/
// We are using the address of 'decision_reason' as pseudo reason for
// decisions to distinguish assignment decisions from other assignments.
// Before we added chronological backtracking all learned units were
// assigned at decision level zero ('Solver.level == 0') and we just used a
// zero pointer as reason. After allowing chronological backtracking units
// were also assigned at higher decision level (but with assignment level
// zero), and it was not possible anymore to just distinguish the case
// 'unit' versus 'decision' by just looking at the current level. Both had
// a zero pointer as reason. Now only units have a zero reason and
// decisions need to use the pseudo reason 'decision_reason'.
// External propagation steps use the pseudo reason 'external_reason'.
// The corresponding actual reason clauses are learned only when they are
// relevant in conflict analysis or in root-level fixing steps.
static Clause decision_reason_clause;
static Clause *decision_reason = &decision_reason_clause;
// If chronological backtracking is used the actual assignment level might
// be lower than the current decision level. In this case the assignment
// level is defined as the maximum level of the literals in the reason
// clause except the literal for which the clause is a reason. This
// function determines this assignment level. For non-chronological
// backtracking as in classical CDCL this function always returns the
// current decision level, the concept of assignment level does not make
// sense, and accordingly this function can be skipped.
// In case of external propagation, it is implicitly assumed that the
// assignment level is the level of the literal (since the reason clause,
// i.e., the set of other literals, is unknown).
inline int Internal::assignment_level (int lit, Clause *reason) {
assert (opts.chrono || external_prop);
if (!reason || reason == external_reason)
return level;
int res = 0;
for (const auto &other : *reason) {
if (other == lit)
continue;
assert (val (other));
int tmp = var (other).level;
if (tmp > res)
res = tmp;
}
return res;
}
// calculate lrat_chain
//
void Internal::build_chain_for_units (int lit, Clause *reason,
bool forced) {
if (!lrat)
return;
if (opts.chrono && assignment_level (lit, reason) && !forced)
return;
else if (!opts.chrono && level && !forced)
return; // not decision level 0
assert (lrat_chain.empty ());
for (auto &reason_lit : *reason) {
if (lit == reason_lit)
continue;
assert (val (reason_lit));
if (!val (reason_lit))
continue;
const unsigned uidx = vlit (val (reason_lit) * reason_lit);
uint64_t id = unit_clauses[uidx];
lrat_chain.push_back (id);
}
lrat_chain.push_back (reason->id);
}
// same code as above but reason is assumed to be conflict and lit is not
// needed
//
void Internal::build_chain_for_empty () {
if (!lrat || !lrat_chain.empty ())
return;
assert (!level);
assert (lrat_chain.empty ());
assert (conflict);
LOG (conflict, "lrat for global empty clause with conflict");
for (auto &lit : *conflict) {
assert (val (lit) < 0);
const unsigned uidx = vlit (-lit);
uint64_t id = unit_clauses[uidx];
lrat_chain.push_back (id);
}
lrat_chain.push_back (conflict->id);
}
/*------------------------------------------------------------------------*/
inline void Internal::search_assign (int lit, Clause *reason) {
if (level)
require_mode (SEARCH);
const int idx = vidx (lit);
const bool from_external = reason == external_reason;
assert (!val (idx));
assert (!flags (idx).eliminated () || reason == decision_reason ||
reason == external_reason);
Var &v = var (idx);
int lit_level;
assert (!lrat || level || reason == external_reason ||
reason == decision_reason || !lrat_chain.empty ());
// The following cases are explained in the two comments above before
// 'decision_reason' and 'assignment_level'.
//
// External decision reason means that the propagation was done by
// an external propagation and the reason clause not known (yet).
// In that case it is assumed that the propagation is NOT out of
// order (i.e. lit_level = level), because due to lazy explanation,
// we can not calculate the real assignment level.
// The function assignment_level () will also assign the current level
// to literals with external reason.
if (!reason)
lit_level = 0; // unit
else if (reason == decision_reason)
lit_level = level, reason = 0;
else if (opts.chrono)
lit_level = assignment_level (lit, reason);
else
lit_level = level;
if (!lit_level)
reason = 0;
v.level = lit_level;
v.trail = trail.size ();
v.reason = reason;
assert ((int) num_assigned < max_var);
assert (num_assigned == trail.size ());
num_assigned++;
if (!lit_level && !from_external)
learn_unit_clause (lit); // increases 'stats.fixed'
assert (lit_level || !from_external);
const signed char tmp = sign (lit);
set_val (idx, tmp);
assert (val (lit) > 0); // Just a bit paranoid but useful.
assert (val (-lit) < 0); // Ditto.
if (!searching_lucky_phases)
phases.saved[idx] = tmp; // phase saving during search
trail.push_back (lit);
#ifdef LOGGING
if (!lit_level)
LOG ("root-level unit assign %d @ 0", lit);
else
LOG (reason, "search assign %d @ %d", lit, lit_level);
#endif
if (watching ()) {
const Watches &ws = watches (-lit);
if (!ws.empty ()) {
const Watch &w = ws[0];
__builtin_prefetch (&w, 0, 1);
}
}
lrat_chain.clear ();
}
/*------------------------------------------------------------------------*/
// External versions of 'search_assign' which are not inlined. They either
// are used to assign unit clauses on the root-level, in 'decide' to assign
// a decision or in 'analyze' to assign the literal 'driven' by a learned
// clause. This happens far less frequently than the 'search_assign' above,
// which is called directly in 'propagate' below and thus is inlined.
void Internal::assign_unit (int lit) {
assert (!level);
search_assign (lit, 0);
}
// Just assume the given literal as decision (increase decision level and
// assign it). This is used below in 'decide'.
void Internal::search_assume_decision (int lit) {
require_mode (SEARCH);
assert (propagated == trail.size ());
new_trail_level (lit);
notify_decision ();
LOG ("search decide %d", lit);
search_assign (lit, decision_reason);
}
void Internal::search_assign_driving (int lit, Clause *c) {
require_mode (SEARCH);
search_assign (lit, c);
notify_assignments ();
}
void Internal::search_assign_external (int lit) {
require_mode (SEARCH);
search_assign (lit, external_reason);
notify_assignments ();
}
/*------------------------------------------------------------------------*/
// The 'propagate' function is usually the hot-spot of a CDCL SAT solver.
// The 'trail' stack saves assigned variables and is used here as BFS queue
// for checking clauses with the negation of assigned variables for being in
// conflict or whether they produce additional assignments.
// This version of 'propagate' uses lazy watches and keeps two watched
// literals at the beginning of the clause. We also use 'blocking literals'
// to reduce the number of times clauses have to be visited (2008 JSAT paper
// by Chu, Harwood and Stuckey). The watches know if a watched clause is
// binary, in which case it never has to be visited. If a binary clause is
// falsified we continue propagating.
// Finally, for long clauses we save the position of the last watch
// replacement in 'pos', which in turn reduces certain quadratic accumulated
// propagation costs (2013 JAIR article by Ian Gent) at the expense of four
// more bytes for each clause.
bool Internal::propagate () {
if (level)
require_mode (SEARCH);
assert (!unsat);
START (propagate);
// Updating statistics counter in the propagation loops is costly so we
// delay until propagation ran to completion.
//
int64_t before = propagated;
while (!conflict && propagated != trail.size ()) {
const int lit = -trail[propagated++];
LOG ("propagating %d", -lit);
Watches &ws = watches (lit);
const const_watch_iterator eow = ws.end ();
watch_iterator j = ws.begin ();
const_watch_iterator i = j;
while (i != eow) {
const Watch w = *j++ = *i++;
const signed char b = val (w.blit);
if (b > 0)
continue; // blocking literal satisfied
if (w.binary ()) {
// assert (w.clause->redundant || !w.clause->garbage);
// In principle we can ignore garbage binary clauses too, but that
// would require to dereference the clause pointer all the time with
//
// if (w.clause->garbage) { j--; continue; } // (*)
//
// This is too costly. It is however necessary to produce correct
// proof traces if binary clauses are traced to be deleted ('d ...'
// line) immediately as soon they are marked as garbage. Actually
// finding instances where this happens is pretty difficult (six
// parallel fuzzing jobs in parallel took an hour), but it does
// occur. Our strategy to avoid generating incorrect proofs now is
// to delay tracing the deletion of binary clauses marked as garbage
// until they are really deleted from memory. For large clauses
// this is not necessary since we have to access the clause anyhow.
//
// Thanks go to Mathias Fleury, who wanted me to explain why the
// line '(*)' above was in the code. Removing it actually really
// improved running times and thus I tried to find concrete
// instances where this happens (which I found), and then
// implemented the described fix.
// Binary clauses are treated separately since they do not require
// to access the clause at all (only during conflict analysis, and
// there also only to simplify the code).
if (b < 0)
conflict = w.clause; // but continue ...
else {
build_chain_for_units (w.blit, w.clause, 0);
search_assign (w.blit, w.clause);
// lrat_chain.clear (); done in search_assign
}
} else {
assert (w.clause->size > 2);
if (conflict)
break; // Stop if there was a binary conflict already.
// The cache line with the clause data is forced to be loaded here
// and thus this first memory access below is the real hot-spot of
// the solver. Note, that this check is positive very rarely and
// thus branch prediction should be almost perfect here.
if (w.clause->garbage) {
j--;
continue;
}
literal_iterator lits = w.clause->begin ();
// Simplify code by forcing 'lit' to be the second literal in the
// clause. This goes back to MiniSAT. We use a branch-less version
// for conditionally swapping the first two literals, since it
// turned out to be substantially faster than this one
//
// if (lits[0] == lit) swap (lits[0], lits[1]);
//
// which achieves the same effect, but needs a branch.
//
const int other = lits[0] ^ lits[1] ^ lit;
const signed char u = val (other); // value of the other watch
if (u > 0)
j[-1].blit = other; // satisfied, just replace blit
else {
// This follows Ian Gent's (JAIR'13) idea of saving the position
// of the last watch replacement. In essence it needs two copies
// of the default search for a watch replacement (in essence the
// code in the 'if (v < 0) { ... }' block below), one starting at
// the saved position until the end of the clause and then if that
// one failed to find a replacement another one starting at the
// first non-watched literal until the saved position.
const int size = w.clause->size;
const literal_iterator middle = lits + w.clause->pos;
const const_literal_iterator end = lits + size;
literal_iterator k = middle;
// Find replacement watch 'r' at position 'k' with value 'v'.
int r = 0;
signed char v = -1;
while (k != end && (v = val (r = *k)) < 0)
k++;
if (v < 0) { // need second search starting at the head?
k = lits + 2;
assert (w.clause->pos <= size);
while (k != middle && (v = val (r = *k)) < 0)
k++;
}
w.clause->pos = k - lits; // always save position
assert (lits + 2 <= k), assert (k <= w.clause->end ());
if (v > 0) {
// Replacement satisfied, so just replace 'blit'.
j[-1].blit = r;
} else if (!v) {
// Found new unassigned replacement literal to be watched.
LOG (w.clause, "unwatch %d in", lit);
lits[0] = other;
lits[1] = r;
*k = lit;
watch_literal (r, lit, w.clause);
j--; // Drop this watch from the watch list of 'lit'.
} else if (!u) {
assert (v < 0);
// The other watch is unassigned ('!u') and all other literals
// assigned to false (still 'v < 0'), thus we found a unit.
//
build_chain_for_units (other, w.clause, 0);
search_assign (other, w.clause);
// lrat_chain.clear (); done in search_assign
// Similar code is in the implementation of the SAT'18 paper on
// chronological backtracking but in our experience, this code
// first does not really seem to be necessary for correctness,
// and further does not improve running time either.
//
if (opts.chrono > 1) {
const int other_level = var (other).level;
if (other_level > var (lit).level) {
// The assignment level of the new unit 'other' is larger
// than the assignment level of 'lit'. Thus we should find
// another literal in the clause at that higher assignment
// level and watch that instead of 'lit'.
assert (size > 2);
int pos, s = 0;
for (pos = 2; pos < size; pos++)
if (var (s = lits[pos]).level == other_level)
break;
assert (s);
assert (pos < size);
LOG (w.clause, "unwatch %d in", lit);
lits[pos] = lit;
lits[0] = other;
lits[1] = s;
watch_literal (s, other, w.clause);
j--; // Drop this watch from the watch list of 'lit'.
}
}
} else {
assert (u < 0);
assert (v < 0);
// The other watch is assigned false ('u < 0') and all other
// literals as well (still 'v < 0'), thus we found a conflict.
conflict = w.clause;
break;
}
}
}
}
if (j != i) {
while (i != eow)
*j++ = *i++;
ws.resize (j - ws.begin ());
}
}
if (searching_lucky_phases) {
if (conflict)
LOG (conflict, "ignoring lucky conflict");
} else {
// Avoid updating stats eagerly in the hot-spot of the solver.
//
stats.propagations.search += propagated - before;
if (!conflict)
no_conflict_until = propagated;
else {
if (stable)
stats.stabconflicts++;
stats.conflicts++;
LOG (conflict, "conflict");
// The trail before the current decision level was conflict free.
//
no_conflict_until = control[level].trail;
}
}
STOP (propagate);
return !conflict;
}
/*------------------------------------------------------------------------*/
void Internal::propergate () {
assert (!conflict);
assert (propagated == trail.size ());
while (propergated != trail.size ()) {
const int lit = -trail[propergated++];
LOG ("propergating %d", -lit);
Watches &ws = watches (lit);
const const_watch_iterator eow = ws.end ();
watch_iterator j = ws.begin ();
const_watch_iterator i = j;
while (i != eow) {
const Watch w = *j++ = *i++;
if (w.binary ()) {
assert (val (w.blit) > 0);
continue;
}
if (w.clause->garbage) {
j--;
continue;
}
literal_iterator lits = w.clause->begin ();
const int other = lits[0] ^ lits[1] ^ lit;
const signed char u = val (other);
if (u > 0)
continue;
assert (u < 0);
const int size = w.clause->size;
const literal_iterator middle = lits + w.clause->pos;
const const_literal_iterator end = lits + size;
literal_iterator k = middle;
int r = 0;
signed char v = -1;
while (k != end && (v = val (r = *k)) < 0)
k++;
if (v < 0) {
k = lits + 2;
assert (w.clause->pos <= size);
while (k != middle && (v = val (r = *k)) < 0)
k++;
}
assert (lits + 2 <= k), assert (k <= w.clause->end ());
w.clause->pos = k - lits;
assert (v > 0);
LOG (w.clause, "unwatch %d in", lit);
lits[0] = other;
lits[1] = r;
*k = lit;
watch_literal (r, lit, w.clause);
j--;
}
if (j != i) {
while (i != eow)
*j++ = *i++;
ws.resize (j - ws.begin ());
}
}
}
} // namespace CaDiCaL