1 #include "internal.hpp"
2
3 namespace CaDiCaL {
4
push_zero_on_extension_stack()5 void External::push_zero_on_extension_stack () {
6 extension.push_back (0);
7 LOG ("pushing 0 on extension stack");
8 }
9
push_clause_literal_on_extension_stack(int ilit)10 void External::push_clause_literal_on_extension_stack (int ilit) {
11 assert (ilit);
12 const int elit = internal->externalize (ilit);
13 assert (elit);
14 extension.push_back (elit);
15 LOG ("pushing clause literal %d on extension stack (internal %d)",
16 elit, ilit);
17 }
18
push_witness_literal_on_extension_stack(int ilit)19 void External::push_witness_literal_on_extension_stack (int ilit) {
20 assert (ilit);
21 const int elit = internal->externalize (ilit);
22 assert (elit);
23 extension.push_back (elit);
24 LOG ("pushing witness literal %d on extension stack (internal %d)",
25 elit, ilit);
26 if (marked (witness, elit)) return;
27 LOG ("marking witness %d", elit);
28 mark (witness, elit);
29 }
30
31 // The extension stack allows to reconstruct a satisfying assignment for the
32 // original formula after removing eliminated clauses. This was pioneered
33 // by Niklas Soerensson in MiniSAT and for instance is described in our
34 // inprocessing paper, published at IJCAR'12. This first function adds a
35 // clause to this stack. First the blocking or eliminated literal is added,
36 // and then the rest of the clause.
37
push_clause_on_extension_stack(Clause * c,int pivot)38 void External::push_clause_on_extension_stack (Clause * c, int pivot) {
39 internal->stats.weakened++;
40 internal->stats.weakenedlen += c->size;
41 push_zero_on_extension_stack ();
42 push_witness_literal_on_extension_stack (pivot);
43 push_zero_on_extension_stack ();
44 for (const auto & lit : *c)
45 push_clause_literal_on_extension_stack (lit);
46 }
47
48 void
push_binary_clause_on_extension_stack(int pivot,int other)49 External::push_binary_clause_on_extension_stack (int pivot, int other) {
50 internal->stats.weakened++;
51 internal->stats.weakenedlen += 2;
52 push_zero_on_extension_stack ();
53 push_witness_literal_on_extension_stack (pivot);
54 push_zero_on_extension_stack ();
55 push_clause_literal_on_extension_stack (pivot);
56 push_clause_literal_on_extension_stack (other);
57 }
58
59 /*------------------------------------------------------------------------*/
60
push_external_clause_and_witness_on_extension_stack(const vector<int> & c,const vector<int> & w)61 void External::push_external_clause_and_witness_on_extension_stack (
62 const vector<int> & c, const vector<int> & w) {
63 extension.push_back (0);
64 for (const auto & elit : w) {
65 assert (elit != INT_MIN);
66 init (abs (elit));
67 extension.push_back (elit);
68 mark (witness, elit);
69 }
70 extension.push_back (0);
71 for (const auto & elit : c) {
72 assert (elit != INT_MIN);
73 init (abs (elit));
74 extension.push_back (elit);
75 }
76 }
77
78 /*------------------------------------------------------------------------*/
79
80 // This is the actual extension process. It goes backward over the clauses
81 // on the extension stack and flips the assignment of one of the blocking
82 // literals in the conditional autarky stored before the clause. In the
83 // original algorithm for witness construction for variable elimination and
84 // blocked clause removal the conditional autarky consists of a single
85 // literal from the removed clause, while in general the autarky witness can
86 // contain an arbitrary set of literals. We are using the more general
87 // witness reconstruction here which for instance would also work for
88 // super-blocked or set-blocked clauses.
89
extend()90 void External::extend () {
91
92 assert (!extended);
93 START (extend);
94 internal->stats.extensions++;
95
96 PHASE ("extend", internal->stats.extensions,
97 "mapping internal %d assignments to %d assignments",
98 internal->max_var, max_var);
99
100 int64_t updated = 0;
101 for (unsigned i = 1; i <= (unsigned) max_var; i++) {
102 const int ilit = e2i[i];
103 if (!ilit) continue;
104 while (i >= vals.size ())
105 vals.push_back (false);
106 vals[i] = (internal->val (ilit) > 0);
107 updated++;
108 }
109 PHASE ("extend", internal->stats.extensions,
110 "updated %" PRId64 " external assignments", updated);
111 PHASE ("extend", internal->stats.extensions,
112 "extending through extension stack of size %zd",
113 extension.size ());
114 const auto begin = extension.begin ();
115 auto i = extension.end ();
116 int64_t flipped = 0;
117 while (i != begin) {
118 bool satisfied = false;
119 int lit;
120 assert (i != begin);
121 while ((lit = *--i)) {
122 if (satisfied) continue;
123 if (val (lit) > 0) satisfied = true;
124 assert (i != begin);
125 }
126 assert (i != begin);
127 if (satisfied)
128 while (*--i)
129 assert (i != begin);
130 else {
131 while ((lit = *--i)) {
132 const int tmp = val (lit);
133 if (tmp < 0) {
134 LOG ("flipping blocking literal %d", lit);
135 assert (lit);
136 assert (lit != INT_MIN);
137 int idx = abs (lit);
138 while ((size_t) idx >= vals.size ())
139 vals.push_back (false);
140 vals[idx] = !vals[idx];
141 internal->stats.extended++;
142 flipped++;
143 }
144 assert (i != begin);
145 }
146 }
147 }
148 PHASE ("extend", internal->stats.extensions,
149 "flipped %" PRId64 " literals during extension", flipped);
150 extended = true;
151 LOG ("extended");
152 STOP (extend);
153 }
154
155 /*------------------------------------------------------------------------*/
156
traverse_witnesses_backward(WitnessIterator & it)157 bool External::traverse_witnesses_backward (WitnessIterator & it) {
158 if (internal->unsat) return true;
159 vector<int> clause, witness;
160 const auto begin = extension.begin ();
161 auto i = extension.end ();
162 while (i != begin) {
163 int lit;
164 while ((lit = *--i))
165 clause.push_back (lit);
166 while ((lit = *--i))
167 witness.push_back (lit);
168 reverse (clause.begin (), clause.end ());
169 reverse (witness.begin (), witness.end ());
170 if (!it.witness (clause, witness))
171 return false;
172 clause.clear ();
173 witness.clear ();
174 }
175 return true;
176 }
177
traverse_witnesses_forward(WitnessIterator & it)178 bool External::traverse_witnesses_forward (WitnessIterator & it) {
179 if (internal->unsat) return true;
180 vector<int> clause, witness;
181 const auto end = extension.end ();
182 auto i = extension.begin ();
183 if (i != end) {
184 int lit = *i++;
185 do {
186 assert (!lit);
187 while ((lit = *i++))
188 witness.push_back (lit);
189 assert (!lit);
190 assert (i != end);
191 while (i != end && (lit = *i++))
192 clause.push_back (lit);
193 if (!it.witness (clause, witness))
194 return false;
195 clause.clear ();
196 witness.clear ();
197 } while (i != end);
198 }
199 return true;
200 }
201
202 /*------------------------------------------------------------------------*/
203
204 }
205