1 /******************************************
2 Copyright (c) 2020, Mate Soos
3 Originally from CaDiCaL's "lucky.cpp" by Armin Biere, 2019
4
5 Permission is hereby granted, free of charge, to any person obtaining a copy
6 of this software and associated documentation files (the "Software"), to deal
7 in the Software without restriction, including without limitation the rights
8 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
9 copies of the Software, and to permit persons to whom the Software is
10 furnished to do so, subject to the following conditions:
11
12 The above copyright notice and this permission notice shall be included in
13 all copies or substantial portions of the Software.
14
15 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
16 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
17 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
18 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
19 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
20 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
21 THE SOFTWARE.
22 ***********************************************/
23
24 #include "lucky.h"
25 #include "solver.h"
26 #include "sqlstats.h"
27 #include "time_mem.h"
28
29 using namespace CMSat;
30
31
Lucky(Solver * _solver)32 Lucky::Lucky(Solver* _solver) :
33 solver(_solver)
34 {
35 }
36
doit()37 bool CMSat::Lucky::doit()
38 {
39 assert(solver->okay());
40 assert(solver->decisionLevel() == 0);
41
42 bool ret = false;
43 double myTime = cpuTime();
44
45 if (check_all(true)) {
46 ret = true;
47 goto end;
48 }
49
50 if (check_all(false)) {
51 ret = true;
52 goto end;
53 }
54
55 if (search_fwd_sat(true)) {
56 ret = true;
57 goto end;
58 }
59
60 if (search_fwd_sat(false)) {
61 ret = true;
62 goto end;
63 }
64
65 if (search_backw_sat(true)) {
66 ret = true;
67 goto end;
68 }
69 if (search_backw_sat(false)) {
70 ret = true;
71 goto end;
72 }
73
74 if (horn_sat(true)) {
75 ret = true;
76 goto end;
77 }
78
79 if (horn_sat(false)) {
80 ret = true;
81 goto end;
82 }
83
84 end:
85 double time_used = cpuTime() - myTime;
86 if (solver->conf.verbosity) {
87 cout << "c [lucky] finished "
88 << solver->conf.print_times(time_used)
89 << endl;
90 }
91 if (solver->sqlStats) {
92 solver->sqlStats->time_passed_min(
93 solver
94 , "lucky"
95 , time_used
96 );
97 }
98 assert(solver->decisionLevel() == 0);
99 return ret;
100 }
101
check_all(bool polar)102 bool CMSat::Lucky::check_all(bool polar)
103 {
104 for(uint32_t i = 0; i < solver->nVars()*2; i++) {
105 Lit lit = Lit::toLit(i);
106
107 if (solver->value(lit) == l_True) {
108 continue;
109 }
110 if (!lit.sign() == polar) {
111 continue;
112 }
113 for(const auto& w: solver->watches[lit]) {
114 if (w.isBin() && solver->value(w.lit2()) == l_True)
115 continue;
116 if (w.isBin() && solver->value(w.lit2()) == l_False)
117 return false;
118 if (w.isBin() && !w.lit2().sign() != polar)
119 return false;
120 }
121 }
122
123 for(const auto off: solver->longIrredCls) {
124 Clause* cl = solver->cl_alloc.ptr(off);
125 bool ok = false;
126 for(const Lit l: *cl) {
127 if (solver->value(l) == l_True) {
128 ok = true;
129 break;
130 }
131 if (!l.sign() == polar) {
132 ok = true;
133 break;
134 }
135 }
136 if (!ok) {
137 return false;
138 }
139 }
140
141 if (solver->conf.verbosity) {
142 cout << "c [lucky] all " << (int)polar << " worked. Saving phases." << endl;
143 }
144 for(auto& x: solver->varData) {
145 x.polarity = polar;
146 x.best_polarity = polar;
147 }
148 solver->longest_trail_ever = solver->nVarsOuter();
149 return true;
150 }
151
152
set_polarities_to_enq_val()153 void Lucky::set_polarities_to_enq_val()
154 {
155 for(uint32_t i = 0; i < solver->nVars(); i++) {
156 solver->varData[i].polarity = solver->value(i) == l_True;
157 solver->varData[i].best_polarity = solver->varData[i].polarity;
158 }
159 solver->longest_trail_ever = solver->nVarsOuter();
160 }
161
search_fwd_sat(bool polar)162 bool CMSat::Lucky::search_fwd_sat(bool polar)
163 {
164 for(uint32_t i = 0; i < solver->nVars(); i++) {
165 if (solver->varData[i].removed != Removed::none) {
166 continue;
167 }
168
169 if (solver->value(i) != l_Undef) {
170 continue;
171 }
172 solver->new_decision_level();
173
174 Lit lit = Lit(i, !polar);
175 solver->enqueue<true>(lit);
176 auto p = solver->propagate<true>();
177 if (!p.isNULL()) {
178 solver->cancelUntil<false, true>(0);
179 return false;
180 }
181 }
182
183 if (solver->conf.verbosity) {
184 cout << "c [lucky] Forward polar " << (int)polar << " worked. Saving phases." << endl;
185 }
186
187 set_polarities_to_enq_val();
188 solver->cancelUntil<false, true>(0);
189
190 return true;
191 }
192
enqueue_and_prop_assumptions()193 bool CMSat::Lucky::enqueue_and_prop_assumptions()
194 {
195 assert(solver->decisionLevel() == 0);
196 while (solver->decisionLevel() < solver->assumptions.size()) {
197 const Lit p = solver->map_outer_to_inter(
198 solver->assumptions[solver->decisionLevel()].lit_outer);
199
200 if (solver->value(p) == l_True) {
201 // Dummy decision level:
202 solver->new_decision_level();
203 continue;
204 } else if (solver->value(p) == l_False) {
205 solver->cancelUntil<false, true>(0);
206 return false;
207 } else {
208 assert(p.var() < solver->nVars());
209 solver->new_decision_level();
210 solver->enqueue<true>(p);
211 auto prop = solver->propagate<true>();
212 if (!prop.isNULL()) {
213 solver->cancelUntil<false, true>(0);
214 return false;
215 }
216 }
217 }
218 return true;
219 }
220
search_backw_sat(bool polar)221 bool CMSat::Lucky::search_backw_sat(bool polar)
222 {
223 if (!enqueue_and_prop_assumptions()) {
224 return false;
225 }
226
227 for(int i = (int)solver->nVars() - 1; i >= 0; i--) {
228 if (solver->varData[i].removed != Removed::none) {
229 continue;
230 }
231
232 if (solver->value(i) != l_Undef) {
233 continue;
234 }
235 solver->new_decision_level();
236
237 Lit lit = Lit(i, !polar);
238 solver->enqueue<true>(lit);
239 auto p = solver->propagate<true>();
240 if (!p.isNULL()) {
241 solver->cancelUntil<false, true>(0);
242 return false;
243 }
244 }
245
246 if (solver->conf.verbosity) {
247 cout << "c [lucky] Backward polar " << (int)polar << " worked. Saving phases." << endl;
248 }
249
250 set_polarities_to_enq_val();
251 solver->cancelUntil<false, true>(0);
252 return true;
253 }
254
horn_sat(bool polar)255 bool CMSat::Lucky::horn_sat(bool polar)
256 {
257 if (!enqueue_and_prop_assumptions()) {
258 return false;
259 }
260
261 for(const auto off: solver->longIrredCls) {
262 Clause* cl = solver->cl_alloc.ptr(off);
263 bool satisfied = false;
264 Lit to_set = lit_Undef;
265 for(const Lit l: *cl) {
266 if (!l.sign() == polar && solver->value(l) == l_Undef) {
267 to_set = l;
268 }
269 if (solver->value(l) == l_True) {
270 satisfied = true;
271 break;
272 }
273 }
274 if (satisfied) {
275 continue;
276 }
277
278 if (to_set == lit_Undef) {
279 //no unassigned literal of correct polarity
280 solver->cancelUntil<false, true>(0);
281 return false;
282 }
283 solver->new_decision_level();
284 solver->enqueue<true>(to_set);
285 auto p = solver->propagate<true>();
286 if (!p.isNULL()) {
287 solver->cancelUntil<false, true>(0);
288 return false;
289 }
290 }
291
292 //NOTE: propagating WHILE going through a watchlist will SEGFAULT
293 vector<Lit> toset;
294 for(uint32_t i = 0; i < solver->nVars()*2; i++) {
295 Lit lit = Lit::toLit(i);
296 if (solver->value(lit) == l_True) {
297 continue;
298 }
299 if (!lit.sign() == polar) {
300 bool must_set = false;
301 for(const auto& w: solver->watches[lit]) {
302 if (w.isBin() &&
303 solver->value(w.lit2()) != l_True)
304 {
305 must_set = true;
306 break;
307 }
308 }
309 if (must_set) {
310 solver->new_decision_level();
311 solver->enqueue<true>(lit);
312 auto p = solver->propagate<true>();
313 if (!p.isNULL()) {
314 solver->cancelUntil<false, true>(0);
315 return false;
316 }
317 }
318 } else {
319 toset.clear();
320 bool ok = true;
321 for(const auto& w: solver->watches[lit]) {
322 if (w.isBin() &&
323 solver->value(w.lit2()) != l_True)
324 {
325 if (w.lit2().sign() != polar) {
326 ok = false;
327 break;
328 } else {
329 toset.push_back(w.lit2());
330 }
331 }
332 }
333 if (!ok) {
334 solver->cancelUntil<false, true>(0);
335 return false;
336 }
337 for(const auto& x: toset) {
338 if (solver->value(x) == l_False) {
339 solver->cancelUntil<false, true>(0);
340 return false;
341 }
342 if (solver->value(x) == l_True) {
343 continue;
344 }
345 solver->new_decision_level();
346 solver->enqueue<true>(x);
347 auto p = solver->propagate<true>();
348 if (!p.isNULL()) {
349 solver->cancelUntil<false, true>(0);
350 return false;
351 }
352 }
353 }
354 }
355
356 if (solver->conf.verbosity) {
357 cout << "c [lucky] Horn polar " << (int)polar << " worked. Saving phases." << endl;
358 }
359
360 set_polarities_to_enq_val();
361 solver->cancelUntil<false, true>(0);
362 return true;
363 }
364