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