1 /******************************************
2 Copyright (c) 2018, Mate Soos <soos.mate@gmail.com>
3
4 Permission is hereby granted, free of charge, to any person obtaining a copy
5 of this software and associated documentation files (the "Software"), to deal
6 in the Software without restriction, including without limitation the rights
7 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
8 copies of the Software, and to permit persons to whom the Software is
9 furnished to do so, subject to the following conditions:
10
11 The above copyright notice and this permission notice shall be included in
12 all copies or substantial portions of the Software.
13
14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
15 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
16 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
17 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
18 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
19 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
20 THE SOFTWARE.
21 ***********************************************/
22
23 #include "time_mem.h"
24 #include <limits>
25 #include <cstdio>
26 #include <cmath>
27 #include <cstdlib>
28 #include "constants.h"
29 #include "yalsat.h"
30 #include "solver.h"
31 #include "sqlstats.h"
32 extern "C" {
33 #include "yals.h"
34 }
35 //#define SLOW_DEBUG
36
37 using namespace CMSat;
38
Yalsat(Solver * _solver)39 Yalsat::Yalsat(Solver* _solver) :
40 solver(_solver)
41 {
42 yals = yals_new();
43 if (solver->conf.verbosity) {
44 yals_setopt (yals, "verbose", 1);
45 } else {
46 yals_setopt (yals, "verbose", 0);
47 }
48 //yals_setprefix (yals, "c 00 ");
49 }
50
~Yalsat()51 Yalsat::~Yalsat()
52 {
53 yals_del(yals);
54 }
55
main()56 lbool Yalsat::main()
57 {
58 //It might not work well with few number of variables
59 //rnovelty could also die/exit(-1), etc.
60 if (solver->nVars() < 50) {
61 if (solver->conf.verbosity) {
62 cout << "c [walksat] too few variables for walksat"
63 << endl;
64 }
65 return l_Undef;
66 }
67 double startTime = cpuTime();
68
69 if (!init_problem()) {
70 //it's actually l_False under assumptions
71 //but we'll set the real SAT solver deal with that
72 if (solver->conf.verbosity) {
73 cout << "c [walksat] problem UNSAT under assumptions, returning to main solver"
74 << endl;
75 }
76 return l_Undef;
77 }
78 //yals_setflipslimit(yals, 5*1000*1000);
79 uint64_t mils = solver->conf.yalsat_max_mems*solver->conf.global_timeout_multiplier;
80 if (solver->conf.verbosity) {
81 cout << "c [yalsat] mems limit M: " << mils << endl;
82 }
83 yals_setmemslimit(yals, mils*1000*1000);
84 yals_srand(yals, solver->mtrand.randInt() % 1000);
85 for(int i = 0; i < (int)solver->nVars(); i++) {
86 int v = i+1;
87 if (solver->value(i) != l_Undef) {
88 if (solver->value(i) == l_False) {
89 v *= -1;
90 }
91 } else {
92 if (!solver->varData[i].polarity) {
93 v *= -1;
94 }
95 }
96 yals_setphase(yals, v);
97 }
98 //yals_srand(yals, 0);
99 //yals_setopt (yals, "hitlim", 5*1000*1000); //every time the minimum (or lower) is hit
100 //yals_setopt (yals, "hitlim", 50000000);
101
102 int res = yals_sat(yals);
103 lbool ret = deal_with_solution(res);
104
105 double time_used = cpuTime()-startTime;
106 if (solver->conf.verbosity) {
107 cout << "c [yalsat] time: " << time_used << endl;
108 }
109 if (solver->sqlStats) {
110 solver->sqlStats->time_passed_min(
111 solver
112 , "sls-yalsat"
113 , time_used
114 );
115 }
116 return ret;
117 }
118
119 template<class T>
add_this_clause(const T & cl)120 Yalsat::add_cl_ret Yalsat::add_this_clause(const T& cl)
121 {
122 uint32_t sz = 0;
123 bool sat = false;
124 yals_lits.clear();
125 for(size_t i3 = 0; i3 < cl.size(); i3++) {
126 Lit lit = cl[i3];
127 assert(solver->varData[lit.var()].removed == Removed::none);
128 lbool val = l_Undef;
129 if (solver->value(lit) != l_Undef) {
130 val = solver->value(lit);
131 } else {
132 val = solver->lit_inside_assumptions(lit);
133 }
134
135 if (val == l_True) {
136 //clause is SAT, skip!
137 sat = true;
138 continue;
139 } else if (val == l_False) {
140 continue;
141 }
142 int l = lit.var()+1;
143 l *= lit.sign() ? -1 : 1;
144 yals_lits.push_back(l);
145 sz++;
146 }
147 if (sat) {
148 return add_cl_ret::skipped_cl;
149 }
150 if (sz == 0) {
151 //it's unsat because of assumptions
152 if (solver->conf.verbosity) {
153 cout << "c [walksat] UNSAT because of assumptions in clause: " << cl << endl;
154 }
155 return add_cl_ret::unsat;
156 }
157
158 for(int i: yals_lits) {
159 yals_add(yals, i);
160 }
161 yals_add(yals, 0);
162 yals_lits.clear();
163
164 return add_cl_ret::added_cl;
165 }
166
init_problem()167 bool Yalsat::init_problem()
168 {
169 if (solver->check_assumptions_contradict_foced_assignment())
170 {
171 return false;
172 }
173 #ifdef SLOWDEBUG
174 solver->check_stats();
175 #endif
176
177 //where all clauses' literals are
178 vector<Lit> this_clause;
179 for(size_t i2 = 0; i2 < solver->nVars()*2; i2++) {
180 Lit lit = Lit::toLit(i2);
181 for(const Watched& w: solver->watches[lit]) {
182 if (w.isBin() && !w.red() && lit < w.lit2()) {
183 this_clause.clear();
184 this_clause.push_back(lit);
185 this_clause.push_back(w.lit2());
186
187 if (add_this_clause(this_clause) == add_cl_ret::unsat) {
188 return false;
189 }
190 }
191 }
192 }
193 for(ClOffset offs: solver->longIrredCls) {
194 const Clause* cl = solver->cl_alloc.ptr(offs);
195 assert(!cl->freed());
196 assert(!cl->getRemoved());
197
198 if (add_this_clause(*cl) == add_cl_ret::unsat) {
199 return false;
200 }
201 }
202
203 return true;
204 }
205
deal_with_solution(int res)206 lbool Yalsat::deal_with_solution(int res)
207 {
208 if (res == 20) {
209 if (solver->conf.verbosity) {
210 cout << "c [yalsat] says UNSAT -- strange" << endl;
211 }
212 return l_Undef;
213 }
214
215 if (solver->conf.sls_get_phase || res == 10) {
216 if (solver->conf.verbosity) {
217 cout << "c [yalsat] saving best assignment phase -- it had " << yals_minimum(yals) << " clauses unsatisfied" << endl;
218 }
219
220 for(size_t i = 0; i < solver->nVars(); i++) {
221 solver->varData[i].polarity = (yals_deref(yals, i+1) >= 0);
222 }
223 }
224
225 if (res != 10) {
226 if (solver->conf.verbosity >= 2) {
227 cout << "c [yalsat] ASSIGNMENT NOT FOUND" << endl;
228 }
229 return l_Undef;
230 }
231
232 if (solver->conf.verbosity) {
233 cout << "c [yalsat] ASSIGNMENT FOUND" << endl;
234 }
235
236 return l_Undef;
237 }
238