1 /*******************************************************************************
2 * SAT4J: a SATisfiability library for Java Copyright (C) 2004, 2012 Artois University and CNRS
3 *
4 * All rights reserved. This program and the accompanying materials
5 * are made available under the terms of the Eclipse Public License v1.0
6 * which accompanies this distribution, and is available at
7 * http://www.eclipse.org/legal/epl-v10.html
8 *
9 * Alternatively, the contents of this file may be used under the terms of
10 * either the GNU Lesser General Public License Version 2.1 or later (the
11 * "LGPL"), in which case the provisions of the LGPL are applicable instead
12 * of those above. If you wish to allow use of your version of this file only
13 * under the terms of the LGPL, and not to allow others to use your version of
14 * this file under the terms of the EPL, indicate your decision by deleting
15 * the provisions above and replace them with the notice and other provisions
16 * required by the LGPL. If you do not delete the provisions above, a recipient
17 * may use your version of this file under the terms of the EPL or the LGPL.
18 *
19 * Based on the original MiniSat specification from:
20 *
21 * An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
22 * Sixth International Conference on Theory and Applications of Satisfiability
23 * Testing, LNCS 2919, pp 502-518, 2003.
24 *
25 * See www.minisat.se for the original solver in C++.
26 *
27 * Contributors:
28 * CRIL - initial API and implementation
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 * Data structure for pseudo-boolean constraint with watched literals.
42 *
43 * All literals are watched. The sum of the literals satisfied or unvalued is
44 * always memorized, to detect conflict.
45 *
46 *
47 */
48 public final class MaxWatchPbLongCP extends WatchPbLongCP {
49
50 private static final long serialVersionUID = 1L;
51
52 /**
53 * sum of the coefficients of the literals satisfied or unvalued
54 */
55 private long watchCumul = 0;
56
57 private final Map<Integer, Long> litToCoeffs;
58
59 /**
60 * Builds a PB constraint for a0.x0 + a1.x1 + ... + an.xn >= k
61 *
62 * This constructor is called for learnt pseudo boolean constraints.
63 *
64 * @param voc
65 * all the possible variables (vocabulary)
66 * @param mpb
67 * data structure which contains literals of the constraint,
68 * coefficients (a0, a1, ... an), and the degree of the
69 * constraint (k). The constraint is a "more than" constraint.
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 * Builds a PB constraint for a0.x0 + a1.x1 + ... + an.xn >= k
90 *
91 * @param voc
92 * all the possible variables (vocabulary)
93 * @param lits
94 * literals of the constraint (x0,x1, ... xn)
95 * @param coefs
96 * coefficients of the left side of the constraint (a0, a1, ...
97 * an)
98 * @param degree
99 * degree of the constraint (k)
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>(this.coefs.length);
111 for (int i = 0; i < this.coefs.length; i++) {
112 this.litToCoeffs.put(this.lits[i], this.coefs[i]);
113 }
114 } else {
115 this.litToCoeffs = null;
116 }
117 }
118
119 /**
120 * All the literals are watched.
121 *
122 * @see org.sat4j.pb.constraints.pb.WatchPbLong#computeWatches()
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 // updating of the initial value for the counter
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 * This method propagates any possible value.
148 *
149 * This method is only called in the factory methods.
150 *
151 * @see org.sat4j.minisat.constraints.WatchPb#computePropagation()
152 */
153 @Override
154 protected void computePropagation(UnitPropagationListener s)
155 throws ContradictionException {
156 // propagate any possible value
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 // because this happens during the building of a constraint.
163 throw new ContradictionException("non satisfiable constraint");
164 }
165 ind++;
166 }
167 assert this.watchCumul >= computeLeftSide();
168 }
169
170 /**
171 * Propagation of a falsified literal
172 *
173 * @param s
174 * the solver
175 * @param p
176 * the propagated literal (it must be falsified)
177 * @return false iff there is a conflict
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 // compute the new value for watchCumul
186 long coefP;
187 if (this.litToCoeffs == null) {
188 // finding the index for p in the array of literals
189 int indiceP = 0;
190 while ((this.lits[indiceP] ^ 1) != p) {
191 indiceP++;
192 }
193
194 // compute the new value for watchCumul
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 // there is a conflict
203 assert !isSatisfiable();
204 return false;
205 }
206
207 // if no conflict, not(p) can be propagated
208 // allow a later un-assignation
209 this.voc.undos(p).push(this);
210 // really update watchCumul
211 this.watchCumul = newcumul;
212
213 // propagation
214 int ind = 0;
215 // limit is the margin between the sum of the coefficients of the
216 // satisfied+unassigned literals
217 // and the degree of the constraint
218 long limit = this.watchCumul - this.degree;
219 // for each coefficient greater than limit
220 while (ind < this.coefs.length && limit < this.coefs[ind]) {
221 // its corresponding literal is implied
222 if (this.voc.isUnassigned(this.lits[ind])
223 && !s.enqueue(this.lits[ind], this)) {
224 // if it is not possible then there is a conflict
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 * Remove a constraint from the solver
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 * this method is called during backtrack
250 *
251 * @param p
252 * an unassigned literal
253 */
254 public void undo(int p) {
255 long coefP;
256 if (this.litToCoeffs == null) {
257 // finding the index for p in the array of literals
258 int indiceP = 0;
259 while ((this.lits[indiceP] ^ 1) != p) {
260 indiceP++;
261 }
262
263 // compute the new value for watchCumul
264 coefP = this.coefs[indiceP];
265 } else {
266 Long coefL = this.litToCoeffs.get(p ^ 1);
267 if (coefL != null) {
268 coefP = this.litToCoeffs.get(p ^ 1);
269 } else {
270 coefP = 0L;
271 }
272 }
273 this.watchCumul = this.watchCumul + coefP;
274 }
275
276 /**
277 * build a pseudo boolean constraint. Coefficients are positive integers
278 * less than or equal to the degree (this is called a normalized
279 * constraint).
280 *
281 * @param s
282 * a unit propagation listener (usually the solver)
283 * @param voc
284 * the vocabulary
285 * @param lits
286 * the literals of the constraint
287 * @param coefs
288 * the coefficients of the constraint
289 * @param degree
290 * the degree of the constraint
291 * @return a new PB constraint or null if a trivial inconsistency is
292 * detected.
293 */
294 public static MaxWatchPbLongCP normalizedMaxWatchPbNew(
295 UnitPropagationListener s, ILits voc, int[] lits,
296 BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
297 throws ContradictionException {
298 // Parameters must not be modified
299 MaxWatchPbLongCP outclause = new MaxWatchPbLongCP(voc, lits, coefs,
300 degree, sumCoefs);
301
302 if (outclause.degree <= 0) {
303 return null;
304 }
305
306 outclause.computeWatches();
307
308 outclause.computePropagation(s);
309
310 return outclause;
311
312 }
313
314 /**
315 * build a pseudo boolean constraint from a specific data structure. For
316 * learnt constraints.
317 *
318 * @param s
319 * a unit propagation listener (usually the solver)
320 * @param mpb
321 * data structure which contains literals of the constraint,
322 * coefficients (a0, a1, ... an), and the degree of the
323 * constraint (k). The constraint is a "more than" constraint.
324 * @return a new PB constraint or null if a trivial inconsistency is
325 * detected.
326 */
327 public static WatchPbLongCP normalizedWatchPbNew(ILits voc,
328 IDataStructurePB mpb) {
329 return new MaxWatchPbLongCP(voc, mpb);
330 }
331
332 }