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>(coefs.length);
115 for (int i = 0; i < coefs.length; i++) {
116 this.litToCoeffs.put(lits[i], this.coefs[i]);
117 }
118 } else {
119 this.litToCoeffs = null;
120 }
121 }
122
123 /**
124 * All the literals are watched.
125 *
126 * @see org.sat4j.pb.constraints.pb.WatchPb#computeWatches()
127 */
128 @Override
129 protected void computeWatches() throws ContradictionException {
130 assert this.watchCumul.equals(BigInteger.ZERO);
131 for (int i = 0; i < this.lits.length; i++) {
132 if (this.voc.isFalsified(this.lits[i])) {
133 if (this.learnt) {
134 this.voc.undos(this.lits[i] ^ 1).push(this);
135 this.voc.watch(this.lits[i] ^ 1, this);
136 }
137 } else {
138 // updating of the initial value for the counter
139 this.voc.watch(this.lits[i] ^ 1, this);
140 this.watchCumul = this.watchCumul.add(this.coefs[i]);
141 }
142 }
143
144 assert this.watchCumul.compareTo(computeLeftSide()) >= 0;
145 if (!this.learnt && this.watchCumul.compareTo(this.degree) < 0) {
146 throw new ContradictionException("non satisfiable constraint");
147 }
148 }
149
150 /*
151 * This method propagates any possible value.
152 *
153 * This method is only called in the factory methods.
154 *
155 * @see org.sat4j.minisat.constraints.WatchPb#computePropagation()
156 */
157 @Override
158 protected void computePropagation(UnitPropagationListener s)
159 throws ContradictionException {
160 // propagate any possible value
161 int ind = 0;
162 while (ind < this.coefs.length
163 && this.watchCumul.subtract(this.coefs[ind]).compareTo(
164 this.degree) < 0) {
165 if (this.voc.isUnassigned(this.lits[ind])
166 && !s.enqueue(this.lits[ind], this)) {
167 // because this happens during the building of a constraint.
168 throw new ContradictionException("non satisfiable constraint");
169 }
170 ind++;
171 }
172 assert this.watchCumul.compareTo(computeLeftSide()) >= 0;
173 }
174
175 /**
176 * Propagation of a falsified literal
177 *
178 * @param s
179 * the solver
180 * @param p
181 * the propagated literal (it must be falsified)
182 * @return false iff there is a conflict
183 */
184 public boolean propagate(UnitPropagationListener s, int p) {
185 this.voc.watch(p, this);
186
187 assert this.watchCumul.compareTo(computeLeftSide()) >= 0 : ""
188 + this.watchCumul + "/" + computeLeftSide() + ":" + this.learnt;
189
190 // compute the new value for watchCumul
191 BigInteger coefP;
192 if (this.litToCoeffs == null) {
193 // finding the index for p in the array of literals
194 int indiceP = 0;
195 while ((this.lits[indiceP] ^ 1) != p) {
196 indiceP++;
197 }
198
199 // compute the new value for watchCumul
200 coefP = this.coefs[indiceP];
201 } else {
202 coefP = this.litToCoeffs.get(p ^ 1);
203 }
204
205 BigInteger newcumul = this.watchCumul.subtract(coefP);
206
207 if (newcumul.compareTo(this.degree) < 0) {
208 // there is a conflict
209 assert !isSatisfiable();
210 return false;
211 }
212
213 // if no conflict, not(p) can be propagated
214 // allow a later un-assignation
215 this.voc.undos(p).push(this);
216 // really update watchCumul
217 this.watchCumul = newcumul;
218
219 // propagation
220 int ind = 0;
221 // limit is the margin between the sum of the coefficients of the
222 // satisfied+unassigned literals
223 // and the degree of the constraint
224 BigInteger limit = this.watchCumul.subtract(this.degree);
225 // for each coefficient greater than limit
226 while (ind < this.coefs.length && limit.compareTo(this.coefs[ind]) < 0) {
227 // its corresponding literal is implied
228 if (this.voc.isUnassigned(this.lits[ind])
229 && !s.enqueue(this.lits[ind], this)) {
230 // if it is not possible then there is a conflict
231 assert !isSatisfiable();
232 return false;
233 }
234 ind++;
235 }
236
237 assert this.learnt || this.watchCumul.compareTo(computeLeftSide()) >= 0;
238 assert this.watchCumul.compareTo(computeLeftSide()) >= 0;
239 return true;
240 }
241
242 /**
243 * Remove a constraint from the solver
244 */
245 public void remove(UnitPropagationListener upl) {
246 for (int i = 0; i < this.lits.length; i++) {
247 if (!this.voc.isFalsified(this.lits[i])) {
248 this.voc.watches(this.lits[i] ^ 1).remove(this);
249 }
250 }
251 }
252
253 /**
254 * this method is called during backtrack
255 *
256 * @param p
257 * an unassigned literal
258 */
259 public void undo(int p) {
260 BigInteger coefP;
261 if (this.litToCoeffs == null) {
262 // finding the index for p in the array of literals
263 int indiceP = 0;
264 while ((this.lits[indiceP] ^ 1) != p) {
265 indiceP++;
266 }
267
268 // compute the new value for watchCumul
269 coefP = this.coefs[indiceP];
270 } else {
271 coefP = this.litToCoeffs.get(p ^ 1);
272 }
273
274 this.watchCumul = this.watchCumul.add(coefP);
275 }
276
277 /**
278 * build a pseudo boolean constraint. Coefficients are positive integers
279 * less than or equal to the degree (this is called a normalized
280 * constraint).
281 *
282 * @param s
283 * a unit propagation listener (usually the solver)
284 * @param voc
285 * the vocabulary
286 * @param lits
287 * the literals of the constraint
288 * @param coefs
289 * the coefficients of the constraint
290 * @param degree
291 * the degree of the constraint
292 * @return a new PB constraint or null if a trivial inconsistency is
293 * detected.
294 */
295 public static MaxWatchPb normalizedMaxWatchPbNew(UnitPropagationListener s,
296 ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree,
297 BigInteger sumCoefs) throws ContradictionException {
298 // Parameters must not be modified
299 MaxWatchPb outclause = new MaxWatchPb(voc, lits, coefs, degree,
300 sumCoefs);
301
302 if (outclause.degree.signum() <= 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 WatchPb normalizedWatchPbNew(ILits voc, IDataStructurePB mpb) {
328 return new MaxWatchPb(voc, mpb);
329 }
330
331 }