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