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