1 /******************************************
2 Copyright (c) 2018 Mate Soos
3 Copyright (c) 2012 Cheng-Shen Han
4 Copyright (c) 2012 Jie-Hong Roland Jiang
5
6 For more information, see " When Boolean Satisfiability Meets Gaussian
7 Elimination in a Simplex Way." by Cheng-Shen Han and Jie-Hong Roland Jiang
8 in CAV (Computer Aided Verification), 2012: 410-426
9
10
11 Permission is hereby granted, free of charge, to any person obtaining a copy
12 of this software and associated documentation files (the "Software"), to deal
13 in the Software without restriction, including without limitation the rights
14 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
15 copies of the Software, and to permit persons to whom the Software is
16 furnished to do so, subject to the following conditions:
17
18 The above copyright notice and this permission notice shall be included in
19 all copies or substantial portions of the Software.
20
21 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
22 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
23 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
24 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
25 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
26 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
27 THE SOFTWARE.
28 ***********************************************/
29
30 #include "packedrow.h"
31
32 // #define VERBOSE_DEBUG
33 // #define SLOW_DEBUG
34
35 using namespace CMSat;
36
37 #ifdef _MSC_VER
scan_fwd_64b(int64_t value)38 inline int scan_fwd_64b(int64_t value)
39 {
40 unsigned long at;
41 unsigned char ret = _BitScanForward64(&at, value);
42 at++;
43 if (!ret) at = 0;
44 return at;
45 }
46 #else
scan_fwd_64b(uint64_t value)47 inline int scan_fwd_64b(uint64_t value)
48 {
49 return __builtin_ffsll(value);
50 }
51 #endif
52
53 ///returns popcnt
find_watchVar(vector<Lit> & tmp_clause,const vector<uint32_t> & col_to_var,vector<char> & var_has_resp_row,uint32_t & non_resp_var)54 uint32_t PackedRow::find_watchVar(
55 vector<Lit>& tmp_clause,
56 const vector<uint32_t>& col_to_var,
57 vector<char> &var_has_resp_row,
58 uint32_t& non_resp_var
59 ) {
60 uint32_t popcnt = 0;
61 non_resp_var = std::numeric_limits<uint32_t>::max();
62 tmp_clause.clear();
63
64 for(int i = 0; i < size*64; i++) {
65 if (this->operator[](i)){
66 popcnt++;
67 uint32_t var = col_to_var[i];
68 tmp_clause.push_back(Lit(var, false));
69
70 if (!var_has_resp_row[var]) {
71 non_resp_var = var;
72 } else {
73 //What??? WARNING
74 //This var already has a responsible for it...
75 //How can it be 1???
76 std::swap(tmp_clause[0], tmp_clause.back());
77 }
78 }
79 }
80 assert(tmp_clause.size() == popcnt);
81 assert( popcnt == 0 || var_has_resp_row[ tmp_clause[0].var() ]) ;
82 return popcnt;
83 }
84
get_reason(vector<Lit> & tmp_clause,const vector<lbool> & assigns,const vector<uint32_t> & col_to_var,PackedRow & cols_vals,PackedRow & tmp_col2,Lit prop)85 void PackedRow::get_reason(
86 vector<Lit>& tmp_clause,
87 const vector<lbool>& assigns,
88 const vector<uint32_t>& col_to_var,
89 PackedRow& cols_vals,
90 PackedRow& tmp_col2,
91 Lit prop
92 ) {
93 tmp_col2.set_and(*this, cols_vals);
94 for (int i = 0; i < size; i++) if (mp[i]) {
95 int64_t tmp = mp[i];
96 unsigned long at;
97 at = scan_fwd_64b(tmp);
98 int extra = 0;
99 while (at != 0) {
100 uint32_t col = extra + at-1 + i*64;
101 #ifdef SLOW_DEBUG
102 assert(this->operator[](col) == 1);
103 #endif
104 const uint32_t var = col_to_var[col];
105 if (var == prop.var()) {
106 tmp_clause.push_back(prop);
107 std::swap(tmp_clause[0], tmp_clause.back());
108 } else {
109 const bool val_bool = tmp_col2[col];
110 tmp_clause.push_back(Lit(var, val_bool));
111 }
112
113 extra += at;
114 if (extra == 64)
115 break;
116
117 tmp >>= at;
118 at = scan_fwd_64b(tmp);
119 }
120 }
121
122 #ifdef SLOW_DEBUG
123 for(uint32_t i = 1; i < tmp_clause.size(); i++) {
124 assert(assigns[tmp_clause[i].var()] != l_Undef);
125 }
126 #endif
127 }
128
propGause(const vector<lbool> & assigns,const vector<uint32_t> & col_to_var,vector<char> & var_has_resp_row,uint32_t & new_resp_var,PackedRow & tmp_col,PackedRow & tmp_col2,PackedRow & cols_vals,PackedRow & cols_unset,Lit & ret_lit_prop)129 gret PackedRow::propGause(
130 const vector<lbool>& assigns,
131 const vector<uint32_t>& col_to_var,
132 vector<char> &var_has_resp_row,
133 uint32_t& new_resp_var,
134 PackedRow& tmp_col,
135 PackedRow& tmp_col2,
136 PackedRow& cols_vals,
137 PackedRow& cols_unset,
138 Lit& ret_lit_prop
139 ) {
140 //cout << "start" << endl;
141 //cout << "line: " << *this << endl;
142 uint32_t pop = tmp_col.set_and_until_popcnt_atleast2(*this, cols_unset);
143 #ifdef VERBOSE_DEBUG
144 cout << "POP in GausE: " << pop << " row: " << endl;
145 cout << *this << endl;
146 cout << " cols_unset: " << endl;
147 cout << cols_unset << endl;
148 #endif
149
150 //Find new watch
151 if (pop >= 2) {
152 for (int i = 0; i < size; i++) if (tmp_col.mp[i]) {
153 int64_t tmp = tmp_col.mp[i];
154 unsigned long at;
155 at = scan_fwd_64b(tmp);
156 int extra = 0;
157 while (at != 0) {
158 uint32_t col = extra + at-1 + i*64;
159 #ifdef SLOW_DEBUG
160 assert(tmp_col[col] == 1);
161 #endif
162 const uint32_t var = col_to_var[col];
163
164 #ifdef SLOW_DEBUG
165 const lbool val = assigns[var];
166 assert(val == l_Undef);
167 #endif
168
169 // found new non-basic variable, let's watch it
170 if (!var_has_resp_row[var]) {
171 new_resp_var = var;
172 return gret::nothing_fnewwatch;
173 }
174
175 extra += at;
176 if (extra == 64)
177 break;
178
179 tmp >>= at;
180 at = scan_fwd_64b(tmp);
181 }
182 }
183 assert(false && "Should have found a new watch!");
184 }
185
186 //Calc value of row
187 tmp_col2.set_and(*this, cols_vals);
188 const uint32_t pop_t = tmp_col2.popcnt() + rhs();
189
190 //Lazy prop
191 if (pop == 1) {
192 for (int i = 0; i < size; i++) if (tmp_col.mp[i]) {
193 int at = scan_fwd_64b(tmp_col.mp[i]);
194
195 // found prop
196 uint32_t col = at-1 + i*64;
197 #ifdef SLOW_DEBUG
198 assert(tmp_col[col] == 1);
199 #endif
200 const uint32_t var = col_to_var[col];
201 assert(assigns[var] == l_Undef);
202 ret_lit_prop = Lit(var, !(pop_t % 2));
203 return gret::prop;
204 }
205 assert(false && "Should have found the propagating literal!");
206 }
207
208 //Only SAT & UNSAT left.
209 assert(pop == 0);
210
211 //Satisfied
212 if (pop_t % 2 == 0) {
213 return gret::nothing_satisfied;
214 }
215
216 //Conflict
217 return gret::confl;
218 }
219