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
#ifndef _watch_hpp_INCLUDED
#define _watch_hpp_INCLUDED
#include <cassert>
#include <vector>
#include "clause.hpp"
namespace CaDiCaL {
// Watch lists for CDCL search. The blocking literal (see also comments
// related to 'propagate') is a must and thus combining that with a 64 bit
// pointer will give a 16 byte (8 byte aligned) structure anyhow, which
// means the additional 4 bytes for the size come for free. As alternative
// one could use a 32-bit reference instead of the pointer which would
// however limit the number of clauses to '2^32 - 1'. One would also need
// to use at least one more bit (either taken away from the variable space
// or the clauses) to denote whether the watch is binary.
// in fashion of Intel Sat 10.4230/LIPIcs.SAT.2022.8 we try to
// guarantee the following invariant:
// For both watches:
// if the watched literal is negatively assigned
// either it will be propagated in the future
// or the corresponding blocking literal is positively assigned
// and its level is smaller than the level of the watched literal
//
struct Clause;
struct Watch {
Clause *clause;
int blit;
int size;
Watch (int b, Clause *c) : clause (c), blit (b), size (c->size) {}
Watch (bool, int b, Clause *c) : clause (c), blit (b), size (2) {
assert (c->size == 2);
}
Watch () {}
bool binary () const { return size == 2; }
};
typedef vector<Watch> Watches; // of one literal
typedef Watches::iterator watch_iterator;
typedef Watches::const_iterator const_watch_iterator;
inline void remove_watch (Watches &ws, Clause *clause) {
const auto end = ws.end ();
auto i = ws.begin ();
for (auto j = i; j != end; j++) {
const Watch &w = *i++ = *j;
if (w.clause == clause)
i--;
}
assert (i + 1 == end);
ws.resize (i - ws.begin ());
}
// search for the clause and updates the size marked in the watch lists
inline void update_watch_size (Watches &ws, int blit, Clause *conflict) {
bool found = false;
const int size = conflict->size;
for (Watch &w : ws) {
if (w.clause == conflict)
w.size = size, w.blit = blit, found = true;
assert (w.clause->garbage || w.size == 2 || w.clause->size != 2);
}
assert (found), (void) found;
}
} // namespace CaDiCaL
#endif