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 MaxWatchPbLong extends WatchPbLong {
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 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 * 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 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>(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 @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 // compute the new value for watchCumul
187 long coefP;
188 if (this.litToCoeffs == null) {
189 // finding the index for p in the array of literals
190 int indiceP = 0;
191 while ((this.lits[indiceP] ^ 1) != p) {
192 indiceP++;
193 }
194
195 // compute the new value for watchCumul
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 // there is a conflict
204 assert !isSatisfiable();
205 return false;
206 }
207
208 // if no conflict, not(p) can be propagated
209 // allow a later un-assignation
210 this.voc.undos(p).push(this);
211 // really update watchCumul
212 this.watchCumul = newcumul;
213
214 // propagation
215 int ind = 0;
216 // limit is the margin between the sum of the coefficients of the
217 // satisfied+unassigned literals
218 // and the degree of the constraint
219 long limit = this.watchCumul - this.degree;
220 // for each coefficient greater than limit
221 while (ind < this.coefs.length && limit < this.coefs[ind]) {
222 // its corresponding literal is implied
223 if (this.voc.isUnassigned(this.lits[ind])
224 && !s.enqueue(this.lits[ind], this)) {
225 // if it is not possible then there is a conflict
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 * Remove a constraint from the solver
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 * this method is called during backtrack
251 *
252 * @param p
253 * an unassigned literal
254 */
255 @Override
256 public void undo(int p) {
257 long coefP;
258 if (this.litToCoeffs == null) {
259 // finding the index for p in the array of literals
260 int indiceP = 0;
261 while ((this.lits[indiceP] ^ 1) != p) {
262 indiceP++;
263 }
264
265 // compute the new value for watchCumul
266 coefP = this.coefs[indiceP];
267 } else {
268 Long coefL = this.litToCoeffs.get(p ^ 1);
269 if (coefL != null) {
270 coefP = coefL.longValue();
271 } else {
272 coefP = 0L;
273 }
274 }
275 this.watchCumul = this.watchCumul + coefP;
276 }
277
278 /**
279 * build a pseudo boolean constraint. Coefficients are positive integers
280 * less than or equal to the degree (this is called a normalized
281 * constraint).
282 *
283 * @param s
284 * a unit propagation listener (usually the solver)
285 * @param voc
286 * the vocabulary
287 * @param lits
288 * the literals of the constraint
289 * @param coefs
290 * the coefficients of the constraint
291 * @param degree
292 * the degree of the constraint
293 * @return a new PB constraint or null if a trivial inconsistency is
294 * detected.
295 */
296 public static MaxWatchPbLong normalizedMaxWatchPbNew(
297 UnitPropagationListener s, ILits voc, int[] lits,
298 BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
299 throws ContradictionException {
300 // Parameters must not be modified
301 MaxWatchPbLong outclause = new MaxWatchPbLong(voc, lits, coefs, degree,
302 sumCoefs);
303
304 if (outclause.degree <= 0) {
305 return null;
306 }
307
308 outclause.computeWatches();
309
310 outclause.computePropagation(s);
311
312 return outclause;
313
314 }
315
316 /**
317 * build a pseudo boolean constraint from a specific data structure. For
318 * learnt constraints.
319 *
320 * @param s
321 * a unit propagation listener (usually the solver)
322 * @param mpb
323 * data structure which contains literals of the constraint,
324 * coefficients (a0, a1, ... an), and the degree of the
325 * constraint (k). The constraint is a "more than" constraint.
326 * @return a new PB constraint or null if a trivial inconsistency is
327 * detected.
328 */
329 public static WatchPbLong normalizedWatchPbNew(ILits voc,
330 IDataStructurePB mpb) {
331 return new MaxWatchPbLong(voc, mpb);
332 }
333
334 }