所在文件propagate.cpp
传播函数代码分析
1 static Clause decision_reason_clause;
2 static Clause * decision_reason = &decision_reason_clause; //注意此处声明了两个静态量
3
4 inline int Internal::assignment_level (int lit, Clause * reason) {
5 assert (opts.chrono);
6 if (!reason) return level;
7
8 int res = 0;
9
10 for (const auto & other : *reason) {
11 if (other == lit) continue;
12 assert (val (other));
13 int tmp = var (other).level;
14 if (tmp > res) res = tmp;
15 }
16 return res;
17 }
18
19 /*------------------------------------------------------------------------*/
20
21 inline void Internal::search_assign (int lit, Clause * reason) {
22
23 if (level) require_mode (SEARCH);
24
25 const int idx = vidx (lit);
26 assert (!vals[idx]);
27 assert (!flags (idx).eliminated () || reason == decision_reason);
28 Var & v = var (idx);
29 int lit_level;
30
31 if (!reason) lit_level = 0; // unit
32 else if (reason == decision_reason) lit_level = level, reason = 0;
33 else if (opts.chrono) lit_level = assignment_level (lit, reason);
34 else lit_level = level;
35 if (!lit_level) reason = 0;
36
37 v.level = lit_level;
38 v.trail = (int) trail.size ();
39 v.reason = reason;
40 if (!lit_level) learn_unit_clause (lit); // increases 'stats.fixed'
41 const signed char tmp = sign (lit);
42 vals[idx] = tmp;
43 vals[-idx] = -tmp;
44 assert (val (lit) > 0);
45 assert (val (-lit) < 0);
46 if (!searching_lucky_phases)
47 phases.saved[idx] = tmp; // phase saving during search
48 trail.push_back (lit);
49 #ifdef LOGGING
50 if (!lit_level) LOG ("root-level unit assign %d @ 0", lit);
51 else LOG (reason, "search assign %d @ %d", lit, lit_level);
52 #endif
53
54 if (watching ()) {
55 const Watches & ws = watches (-lit);
56 if (!ws.empty ()) {
57 const Watch & w = ws[0];
58 __builtin_prefetch (&w, 0, 1);
59 }
60 }
61 }
62 /*------------------------------------------------------------------------*/
63 void Internal::assign_unit (int lit) {
64 assert (!level);
65 search_assign (lit, 0);
66 }
67
68 void Internal::search_assume_decision (int lit) {
69 require_mode (SEARCH);
70 assert (propagated == trail.size ());
71 level++;
72 control.push_back (Level (lit, trail.size ()));
73 LOG ("search decide %d", lit);
74 search_assign (lit, decision_reason);
75 }
76
77 void Internal::search_assign_driving (int lit, Clause * c) {
78 require_mode (SEARCH);
79 search_assign (lit, c);
80 }
81 /*------------------------------------------------------------------------*/
82 bool Internal::propagate () {
83
84 if (level) require_mode (SEARCH);
85 assert (!unsat);
86
87 START (propagate);
88 //
89 int64_t before = propagated;
90
91 while (!conflict && propagated != trail.size ()) {
92
93 const int lit = -trail[propagated++];
94 LOG ("propagating %d", -lit);
95 Watches & ws = watches (lit);
96
97 const const_watch_iterator eow = ws.end ();
98 watch_iterator j = ws.begin ();
99 const_watch_iterator i = j;
100
101 while (i != eow) {
102 const Watch w = *j++ = *i++;
103 const signed char b = val (w.blit);
104
105 if (b > 0) continue; // blocking literal satisfied
106
107 if (w.binary ()) {
108 if (b < 0) conflict = w.clause; // but continue ...
109 else search_assign (w.blit, w.clause);
110
111 } else {
112
113 if (conflict) break; // Stop if there was a binary conflict already.
114
115 if (w.clause->garbage) { j--; continue; }
116
117 literal_iterator lits = w.clause->begin ();
118
119 const int other = lits[0] ^ lits[1] ^ lit;
120 const signed char u = val (other); // value of the other watch
121
122 if (u > 0) j[-1].blit = other; // satisfied, just replace blit
123 else {
124 const int size = w.clause->size;
125 const literal_iterator middle = lits + w.clause->pos;
126 const const_literal_iterator end = lits + size;
127 literal_iterator k = middle;
128
129 // Find replacement watch 'r' at position 'k' with value 'v'.
130
131 int r = 0;
132 signed char v = -1;
133
134 while (k != end && (v = val (r = *k)) < 0)
135 k++;
136
137 if (v < 0) { // need second search starting at the head?
138 k = lits + 2;
139 assert (w.clause->pos <= size);
140 while (k != middle && (v = val (r = *k)) < 0)
141 k++;
142 }
143
144 w.clause->pos = k - lits; // always save position
145
146 assert (lits + 2 <= k), assert (k <= w.clause->end ());
147
148 if (v > 0) {
149 j[-1].blit = r;
150
151 } else if (!v) {
152
153 // Found new unassigned replacement literal to be watched.
154
155 LOG (w.clause, "unwatch %d in", lit);
156
157 lits[0] = other;
158 lits[1] = r;
159 *k = lit;
160
161 watch_literal (r, lit, w.clause);
162
163 j--; // Drop this watch from the watch list of 'lit'.
164
165 } else if (!u) {
166
167 assert (v < 0);
168
169 search_assign (other, w.clause);
170
171 if (opts.chrono > 1) {
172
173 const int other_level = var (other).level;
174
175 if (other_level > var (lit).level) {
176
177 assert (size > 2);
178
179 int pos, s = 0;
180
181 for (pos = 2; pos < size; pos++)
182 if (var (s = lits[pos]).level == other_level)
183 break;
184
185 assert (s);
186 assert (pos < size);
187
188 LOG (w.clause, "unwatch %d in", lit);
189 lits[pos] = lit;
190 lits[0] = other;
191 lits[1] = s;
192 watch_literal (s, other, w.clause);
193
194 j--; // Drop this watch from the watch list of 'lit'.
195 }
196 }
197 } else {
198
199 assert (u < 0);
200 assert (v < 0);
201
202 conflict = w.clause;
203 break;
204 }
205 }
206 }
207 }
208
209 if (j != i) {
210
211 while (i != eow)
212 *j++ = *i++;
213
214 ws.resize (j - ws.begin ());
215 }
216 }
217
218 if (searching_lucky_phases) {
219
220 if (conflict)
221 LOG (conflict, "ignoring lucky conflict");
222
223 } else {
224
225 stats.propagations.search += propagated - before;
226
227 if (!conflict) no_conflict_until = propagated;
228 else {
229 if (stable) stats.stabconflicts++;
230 stats.conflicts++;
231 LOG (conflict, "conflict");
232 no_conflict_until = control[level].trail;
233 }
234 }
235
236 STOP (propagate);
237 return !conflict;
238 }
标签：02,lit,const,level,int,assert,解读,reason,cadical From： https://www.cnblogs.com/yuweng1689/p/17353523.html