1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30 package org.sat4j.pb.constraints.pb;
31
32 import java.math.BigInteger;
33 import java.util.HashMap;
34 import java.util.Map;
35
36 import org.sat4j.minisat.core.ILits;
37 import org.sat4j.minisat.core.UnitPropagationListener;
38 import org.sat4j.specs.ContradictionException;
39
40
41
42
43
44
45
46
47
48 public final class MaxWatchPbLong extends WatchPbLong {
49
50 private static final long serialVersionUID = 1L;
51
52
53
54
55 private long watchCumul = 0;
56
57 private final Map<Integer, Long> litToCoeffs;
58
59
60
61
62
63
64
65
66
67
68
69
70
71 private MaxWatchPbLong(ILits voc, IDataStructurePB mpb) {
72
73 super(mpb);
74 this.voc = voc;
75
76 this.activity = 0;
77 this.watchCumul = 0;
78 if (this.coefs.length > MaxWatchPb.LIMIT_FOR_MAP) {
79 this.litToCoeffs = new HashMap<Integer, Long>(this.coefs.length);
80 for (int i = 0; i < this.coefs.length; i++) {
81 this.litToCoeffs.put(this.lits[i], this.coefs[i]);
82 }
83 } else {
84 this.litToCoeffs = null;
85 }
86 }
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101 private MaxWatchPbLong(ILits voc, int[] lits, BigInteger[] coefs,
102 BigInteger degree, BigInteger sumCoefs) {
103
104 super(lits, coefs, degree, sumCoefs);
105 this.voc = voc;
106
107 this.activity = 0;
108 this.watchCumul = 0;
109 if (coefs.length > MaxWatchPb.LIMIT_FOR_MAP) {
110 this.litToCoeffs = new HashMap<Integer, Long>(coefs.length);
111 for (int i = 0; i < coefs.length; i++) {
112 this.litToCoeffs.put(lits[i], this.coefs[i]);
113 }
114 } else {
115 this.litToCoeffs = null;
116 }
117 }
118
119
120
121
122
123
124 @Override
125 protected void computeWatches() throws ContradictionException {
126 assert this.watchCumul == 0;
127 for (int i = 0; i < this.lits.length; i++) {
128 if (this.voc.isFalsified(this.lits[i])) {
129 if (this.learnt) {
130 this.voc.undos(this.lits[i] ^ 1).push(this);
131 this.voc.watch(this.lits[i] ^ 1, this);
132 }
133 } else {
134
135 this.voc.watch(this.lits[i] ^ 1, this);
136 this.watchCumul = this.watchCumul + this.coefs[i];
137 }
138 }
139
140 assert this.watchCumul >= computeLeftSide();
141 if (!this.learnt && this.watchCumul < this.degree) {
142 throw new ContradictionException("non satisfiable constraint");
143 }
144 }
145
146
147
148
149
150
151
152
153 @Override
154 protected void computePropagation(UnitPropagationListener s)
155 throws ContradictionException {
156
157 int ind = 0;
158 while (ind < this.coefs.length
159 && this.watchCumul - this.coefs[ind] < this.degree) {
160 if (this.voc.isUnassigned(this.lits[ind])
161 && !s.enqueue(this.lits[ind], this)) {
162
163 throw new ContradictionException("non satisfiable constraint");
164 }
165 ind++;
166 }
167 assert this.watchCumul >= computeLeftSide();
168 }
169
170
171
172
173
174
175
176
177
178
179 @Override
180 public boolean propagate(UnitPropagationListener s, int p) {
181 this.voc.watch(p, this);
182
183 assert this.watchCumul >= computeLeftSide() : "" + this.watchCumul
184 + "/" + computeLeftSide() + ":" + this.learnt;
185
186
187 long coefP;
188 if (this.litToCoeffs == null) {
189
190 int indiceP = 0;
191 while ((this.lits[indiceP] ^ 1) != p) {
192 indiceP++;
193 }
194
195
196 coefP = this.coefs[indiceP];
197 } else {
198 coefP = this.litToCoeffs.get(p ^ 1);
199 }
200 long newcumul = this.watchCumul - coefP;
201
202 if (newcumul < this.degree) {
203
204 assert !isSatisfiable();
205 return false;
206 }
207
208
209
210 this.voc.undos(p).push(this);
211
212 this.watchCumul = newcumul;
213
214
215 int ind = 0;
216
217
218
219 long limit = this.watchCumul - this.degree;
220
221 while (ind < this.coefs.length && limit < this.coefs[ind]) {
222
223 if (this.voc.isUnassigned(this.lits[ind])
224 && !s.enqueue(this.lits[ind], this)) {
225
226 assert !isSatisfiable();
227 return false;
228 }
229 ind++;
230 }
231
232 assert this.learnt || this.watchCumul >= computeLeftSide();
233 assert this.watchCumul >= computeLeftSide();
234 return true;
235 }
236
237
238
239
240 @Override
241 public void remove(UnitPropagationListener upl) {
242 for (int i = 0; i < this.lits.length; i++) {
243 if (!this.voc.isFalsified(this.lits[i])) {
244 this.voc.watches(this.lits[i] ^ 1).remove(this);
245 }
246 }
247 }
248
249
250
251
252
253
254
255 @Override
256 public void undo(int p) {
257 long coefP;
258 if (this.litToCoeffs == null) {
259
260 int indiceP = 0;
261 while ((this.lits[indiceP] ^ 1) != p) {
262 indiceP++;
263 }
264
265
266 coefP = this.coefs[indiceP];
267 } else {
268 coefP = this.litToCoeffs.get(p ^ 1);
269 }
270 this.watchCumul = this.watchCumul + coefP;
271 }
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291 public static MaxWatchPbLong normalizedMaxWatchPbNew(
292 UnitPropagationListener s, ILits voc, int[] lits,
293 BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
294 throws ContradictionException {
295
296 MaxWatchPbLong outclause = new MaxWatchPbLong(voc, lits, coefs, degree,
297 sumCoefs);
298
299 if (outclause.degree <= 0) {
300 return null;
301 }
302
303 outclause.computeWatches();
304
305 outclause.computePropagation(s);
306
307 return outclause;
308
309 }
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324 public static WatchPbLong normalizedWatchPbNew(ILits voc,
325 IDataStructurePB mpb) {
326 return new MaxWatchPbLong(voc, mpb);
327 }
328
329 }