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.minisat.core.UnitPropagationListener;
38 import org.sat4j.specs.ContradictionException;
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 * @author anne
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 * sum of the coefficients of the literals satisfied or unvalued
57 */
58 private BigInteger watchCumul = BigInteger.ZERO;
59
60 private final Map<Integer, BigInteger> litToCoeffs;
61
62 /**
63 * Builds a PB constraint for a0.x0 + a1.x1 + ... + an.xn >= k
64 *
65 * This constructor is called for learnt pseudo boolean constraints.
66 *
67 * @param voc
68 * all the possible variables (vocabulary)
69 * @param mpb
70 * data structure which contains literals of the constraint,
71 * coefficients (a0, a1, ... an), and the degree of the
72 * constraint (k). The constraint is a "more than" constraint.
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 * Builds a PB constraint for a0.x0 + a1.x1 + ... + an.xn >= k
94 *
95 * @param voc
96 * all the possible variables (vocabulary)
97 * @param lits
98 * literals of the constraint (x0,x1, ... xn)
99 * @param coefs
100 * coefficients of the left side of the constraint (a0, a1, ...
101 * an)
102 * @param degree
103 * degree of the constraint (k)
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 * All the literals are watched.
126 *
127 * @see org.sat4j.pb.constraints.pb.WatchPb#computeWatches()
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 // updating of the initial value for the counter
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 * This method propagates any possible value.
153 *
154 * This method is only called in the factory methods.
155 *
156 * @see org.sat4j.minisat.constraints.WatchPb#computePropagation()
157 */
158 @Override
159 protected void computePropagation(UnitPropagationListener s)
160 throws ContradictionException {
161 // propagate any possible value
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 // because this happens during the building of a constraint.
169 throw new ContradictionException("non satisfiable constraint");
170 }
171 ind++;
172 }
173 assert this.watchCumul.compareTo(computeLeftSide()) >= 0;
174 }
175
176 /**
177 * Propagation of a falsified literal
178 *
179 * @param s
180 * the solver
181 * @param p
182 * the propagated literal (it must be falsified)
183 * @return false iff there is a conflict
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 // compute the new value for watchCumul
192 BigInteger coefP;
193 if (this.litToCoeffs == null) {
194 // finding the index for p in the array of literals
195 int indiceP = 0;
196 while ((this.lits[indiceP] ^ 1) != p) {
197 indiceP++;
198 }
199
200 // compute the new value for watchCumul
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 // there is a conflict
210 assert !isSatisfiable();
211 return false;
212 }
213
214 // if no conflict, not(p) can be propagated
215 // allow a later un-assignation
216 this.voc.undos(p).push(this);
217 // really update watchCumul
218 this.watchCumul = newcumul;
219
220 // propagation
221 int ind = 0;
222 // limit is the margin between the sum of the coefficients of the
223 // satisfied+unassigned literals
224 // and the degree of the constraint
225 BigInteger limit = this.watchCumul.subtract(this.degree);
226 // for each coefficient greater than limit
227 while (ind < this.coefs.length && limit.compareTo(this.coefs[ind]) < 0) {
228 // its corresponding literal is implied
229 if (this.voc.isUnassigned(this.lits[ind])
230 && !s.enqueue(this.lits[ind], this)) {
231 // if it is not possible then there is a conflict
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 * Remove a constraint from the solver
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 * this method is called during backtrack
256 *
257 * @param p
258 * an unassigned literal
259 */
260 public void undo(int p) {
261 BigInteger coefP;
262 if (this.litToCoeffs == null) {
263 // finding the index for p in the array of literals
264 int indiceP = 0;
265 while ((this.lits[indiceP] ^ 1) != p) {
266 indiceP++;
267 }
268
269 // compute the new value for watchCumul
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 * 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 MaxWatchPb normalizedMaxWatchPbNew(UnitPropagationListener s,
297 ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree,
298 BigInteger sumCoefs) throws ContradictionException {
299 // Parameters must not be modified
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 * build a pseudo boolean constraint from a specific data structure. For
317 * learnt constraints.
318 *
319 * @param s
320 * a unit propagation listener (usually the solver)
321 * @param mpb
322 * data structure which contains literals of the constraint,
323 * coefficients (a0, a1, ... an), and the degree of the
324 * constraint (k). The constraint is a "more than" constraint.
325 * @return a new PB constraint or null if a trivial inconsistency is
326 * detected.
327 */
328 public static WatchPb normalizedWatchPbNew(ILits voc, IDataStructurePB mpb) {
329 return new MaxWatchPb(voc, mpb);
330 }
331
332 }