1 /*******************************************************************************
2 * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
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 pseudo boolean algorithms described in:
20 * A fast pseudo-Boolean constraint solver Chai, D.; Kuehlmann, A.
21 * Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
22 * Volume 24, Issue 3, March 2005 Page(s): 305 - 317
23 *
24 * and
25 * Heidi E. Dixon, 2004. Automating Pseudo-Boolean Inference within a DPLL
26 * Framework. Ph.D. Dissertation, University of Oregon.
27 *******************************************************************************/
28 package org.sat4j.pb.constraints.pb;
29
30 import java.math.BigInteger;
31 import java.util.HashMap;
32 import java.util.Map;
33
34 import org.sat4j.minisat.core.ILits;
35 import org.sat4j.minisat.core.UnitPropagationListener;
36 import org.sat4j.specs.ContradictionException;
37
38 /**
39 * Data structure for pseudo-boolean constraint with watched literals.
40 *
41 * All literals are watched. The sum of the literals satisfied or unvalued is
42 * always memorized, to detect conflict.
43 *
44 *
45 */
46 public final class MaxWatchPbLong extends WatchPbLong {
47
48 private static final long serialVersionUID = 1L;
49
50 /**
51 * sum of the coefficients of the literals satisfied or unvalued
52 */
53 private long watchCumul = 0;
54
55 private final Map<Integer, Long> litToCoeffs;
56
57 /**
58 * Builds a PB constraint for a0.x0 + a1.x1 + ... + an.xn >= k
59 *
60 * This constructor is called for learnt pseudo boolean constraints.
61 *
62 * @param voc
63 * all the possible variables (vocabulary)
64 * @param mpb
65 * data structure which contains literals of the constraint,
66 * coefficients (a0, a1, ... an), and the degree of the
67 * constraint (k). The constraint is a "more than" constraint.
68 */
69 private MaxWatchPbLong(ILits voc, IDataStructurePB mpb) {
70
71 super(mpb);
72 this.voc = voc;
73
74 activity = 0;
75 watchCumul = 0;
76 if (coefs.length > MaxWatchPb.LIMIT_FOR_MAP) {
77 litToCoeffs = new HashMap<Integer, Long>(coefs.length);
78 for (int i = 0; i < coefs.length; i++) {
79 litToCoeffs.put(lits[i], coefs[i]);
80 }
81 } else
82 litToCoeffs = null;
83 }
84
85 /**
86 * Builds a PB constraint for a0.x0 + a1.x1 + ... + an.xn >= k
87 *
88 * @param voc
89 * all the possible variables (vocabulary)
90 * @param lits
91 * literals of the constraint (x0,x1, ... xn)
92 * @param coefs
93 * coefficients of the left side of the constraint (a0, a1, ...
94 * an)
95 * @param degree
96 * degree of the constraint (k)
97 */
98 private MaxWatchPbLong(ILits voc, int[] lits, BigInteger[] coefs,
99 BigInteger degree) {
100
101 super(lits, coefs, degree);
102 this.voc = voc;
103
104 activity = 0;
105 watchCumul = 0;
106 if (coefs.length > MaxWatchPb.LIMIT_FOR_MAP) {
107 litToCoeffs = new HashMap<Integer, Long>(coefs.length);
108 for (int i = 0; i < coefs.length; i++) {
109 litToCoeffs.put(lits[i], this.coefs[i]);
110 }
111 } else
112 litToCoeffs = null;
113 }
114
115 /**
116 * All the literals are watched.
117 *
118 * @see org.sat4j.pb.constraints.pb.WatchPbLong#computeWatches()
119 */
120 @Override
121 protected void computeWatches() throws ContradictionException {
122 assert watchCumul == 0;
123 for (int i = 0; i < lits.length; i++) {
124 if (voc.isFalsified(lits[i])) {
125 if (learnt) {
126 voc.undos(lits[i] ^ 1).push(this);
127 voc.watch(lits[i] ^ 1, this);
128 }
129 } else {
130 // updating of the initial value for the counter
131 voc.watch(lits[i] ^ 1, this);
132 watchCumul = watchCumul + coefs[i];
133 }
134 }
135
136 assert watchCumul >= computeLeftSide();
137 if (!learnt && watchCumul < degree) {
138 throw new ContradictionException("non satisfiable constraint");
139 }
140 }
141
142 /*
143 * This method propagates any possible value.
144 *
145 * This method is only called in the factory methods.
146 *
147 * @see org.sat4j.minisat.constraints.WatchPb#computePropagation()
148 */
149 @Override
150 protected void computePropagation(UnitPropagationListener s)
151 throws ContradictionException {
152 // propagate any possible value
153 int ind = 0;
154 while (ind < coefs.length && (watchCumul - coefs[ind]) < degree) {
155 if (voc.isUnassigned(lits[ind]) && !s.enqueue(lits[ind], this))
156 // because this happens during the building of a constraint.
157 throw new ContradictionException("non satisfiable constraint");
158 ind++;
159 }
160 assert watchCumul >= computeLeftSide();
161 }
162
163 /**
164 * Propagation of a falsified literal
165 *
166 * @param s
167 * the solver
168 * @param p
169 * the propagated literal (it must be falsified)
170 * @return false iff there is a conflict
171 */
172 @Override
173 public boolean propagate(UnitPropagationListener s, int p) {
174 voc.watch(p, this);
175
176 assert watchCumul >= computeLeftSide() : "" + watchCumul + "/"
177 + computeLeftSide() + ":" + learnt;
178
179 // compute the new value for watchCumul
180 long coefP;
181 if (litToCoeffs == null) {
182 // finding the index for p in the array of literals
183 int indiceP = 0;
184 while ((lits[indiceP] ^ 1) != p)
185 indiceP++;
186
187 // compute the new value for watchCumul
188 coefP = coefs[indiceP];
189 } else {
190 coefP = litToCoeffs.get(p ^ 1);
191 }
192 long newcumul = watchCumul - coefP;
193
194 if (newcumul < degree) {
195 // there is a conflict
196 assert !isSatisfiable();
197 return false;
198 }
199
200 // if no conflict, not(p) can be propagated
201 // allow a later un-assignation
202 voc.undos(p).push(this);
203 // really update watchCumul
204 watchCumul = newcumul;
205
206 // propagation
207 int ind = 0;
208 // limit is the margin between the sum of the coefficients of the
209 // satisfied+unassigned literals
210 // and the degree of the constraint
211 long limit = watchCumul - degree;
212 // for each coefficient greater than limit
213 while (ind < coefs.length && limit < coefs[ind]) {
214 // its corresponding literal is implied
215 if (voc.isUnassigned(lits[ind]) && (!s.enqueue(lits[ind], this))) {
216 // if it is not possible then there is a conflict
217 assert !isSatisfiable();
218 return false;
219 }
220 ind++;
221 }
222
223 assert learnt || watchCumul >= computeLeftSide();
224 assert watchCumul >= computeLeftSide();
225 return true;
226 }
227
228 /**
229 * Remove a constraint from the solver
230 */
231 @Override
232 public void remove(UnitPropagationListener upl) {
233 for (int i = 0; i < lits.length; i++) {
234 if (!voc.isFalsified(lits[i])) {
235 voc.watches(lits[i] ^ 1).remove(this);
236 }
237 if (voc.isSatisfied(lits[i])) {
238 // must be on the trail !!!!
239 upl.unset(lits[i]);
240 }
241 }
242 }
243
244 /**
245 * this method is called during backtrack
246 *
247 * @param p
248 * an unassigned literal
249 */
250 @Override
251 public void undo(int p) {
252 long coefP;
253 if (litToCoeffs == null) {
254 // finding the index for p in the array of literals
255 int indiceP = 0;
256 while ((lits[indiceP] ^ 1) != p)
257 indiceP++;
258
259 // compute the new value for watchCumul
260 coefP = coefs[indiceP];
261 } else {
262 coefP = litToCoeffs.get(p ^ 1);
263 }
264 watchCumul = watchCumul + coefP;
265 }
266
267 /**
268 * build a pseudo boolean constraint. Coefficients are positive integers
269 * less than or equal to the degree (this is called a normalized
270 * constraint).
271 *
272 * @param s
273 * a unit propagation listener (usually the solver)
274 * @param voc
275 * the vocabulary
276 * @param lits
277 * the literals of the constraint
278 * @param coefs
279 * the coefficients of the constraint
280 * @param degree
281 * the degree of the constraint
282 * @return a new PB constraint or null if a trivial inconsistency is
283 * detected.
284 */
285 public static MaxWatchPbLong normalizedMaxWatchPbNew(
286 UnitPropagationListener s, ILits voc, int[] lits,
287 BigInteger[] coefs, BigInteger degree)
288 throws ContradictionException {
289 // Parameters must not be modified
290 MaxWatchPbLong outclause = new MaxWatchPbLong(voc, lits, coefs, degree);
291
292 if (outclause.degree <= 0) {
293 return null;
294 }
295
296 outclause.computeWatches();
297
298 outclause.computePropagation(s);
299
300 return outclause;
301
302 }
303
304 /**
305 * build a pseudo boolean constraint from a specific data structure. For
306 * learnt constraints.
307 *
308 * @param s
309 * a unit propagation listener (usually the solver)
310 * @param mpb
311 * data structure which contains literals of the constraint,
312 * coefficients (a0, a1, ... an), and the degree of the
313 * constraint (k). The constraint is a "more than" constraint.
314 * @return a new PB constraint or null if a trivial inconsistency is
315 * detected.
316 */
317 public static WatchPbLong normalizedWatchPbNew(ILits voc,
318 IDataStructurePB mpb) {
319 return new MaxWatchPbLong(voc, mpb);
320 }
321
322 }