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 MaxWatchPbLongCP extends WatchPbLongCP {
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 MaxWatchPbLongCP(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 MaxWatchPbLongCP(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 public boolean propagate(UnitPropagationListener s, int p) {
180 this.voc.watch(p, this);
181
182 assert this.watchCumul >= computeLeftSide() : "" + this.watchCumul
183 + "/" + computeLeftSide() + ":" + this.learnt;
184
185
186 long coefP;
187 if (this.litToCoeffs == null) {
188
189 int indiceP = 0;
190 while ((this.lits[indiceP] ^ 1) != p) {
191 indiceP++;
192 }
193
194
195 coefP = this.coefs[indiceP];
196 } else {
197 coefP = this.litToCoeffs.get(p ^ 1);
198 }
199 long newcumul = this.watchCumul - coefP;
200
201 if (newcumul < this.degree) {
202
203 assert !isSatisfiable();
204 return false;
205 }
206
207
208
209 this.voc.undos(p).push(this);
210
211 this.watchCumul = newcumul;
212
213
214 int ind = 0;
215
216
217
218 long limit = this.watchCumul - this.degree;
219
220 while (ind < this.coefs.length && limit < this.coefs[ind]) {
221
222 if (this.voc.isUnassigned(this.lits[ind])
223 && !s.enqueue(this.lits[ind], this)) {
224
225 assert !isSatisfiable();
226 return false;
227 }
228 ind++;
229 }
230
231 assert this.learnt || this.watchCumul >= computeLeftSide();
232 assert this.watchCumul >= computeLeftSide();
233 return true;
234 }
235
236
237
238
239 public void remove(UnitPropagationListener upl) {
240 for (int i = 0; i < this.lits.length; i++) {
241 if (!this.voc.isFalsified(this.lits[i])) {
242 this.voc.watches(this.lits[i] ^ 1).remove(this);
243 }
244 }
245
246 }
247
248
249
250
251
252
253
254 public void undo(int p) {
255 long coefP;
256 if (this.litToCoeffs == null) {
257
258 int indiceP = 0;
259 while ((this.lits[indiceP] ^ 1) != p) {
260 indiceP++;
261 }
262
263
264 coefP = this.coefs[indiceP];
265 } else {
266 coefP = this.litToCoeffs.get(p ^ 1);
267 }
268 this.watchCumul = this.watchCumul + coefP;
269 }
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289 public static MaxWatchPbLongCP normalizedMaxWatchPbNew(
290 UnitPropagationListener s, ILits voc, int[] lits,
291 BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
292 throws ContradictionException {
293
294 MaxWatchPbLongCP outclause = new MaxWatchPbLongCP(voc, lits, coefs,
295 degree, sumCoefs);
296
297 if (outclause.degree <= 0) {
298 return null;
299 }
300
301 outclause.computeWatches();
302
303 outclause.computePropagation(s);
304
305 return outclause;
306
307 }
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322 public static WatchPbLongCP normalizedWatchPbNew(ILits voc,
323 IDataStructurePB mpb) {
324 return new MaxWatchPbLongCP(voc, mpb);
325 }
326
327 }