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
32 import org.sat4j.minisat.core.ILits;
33 import org.sat4j.minisat.core.UnitPropagationListener;
34 import org.sat4j.specs.ContradictionException;
35
36 /**
37 * Data structure for pseudo-boolean constraint with watched literals.
38 *
39 * All literals are watched. The sum of the literals satisfied or unvalued is
40 * always memorized, to detect conflict.
41 *
42 * @author anne
43 *
44 */
45 public final class MaxWatchPb extends WatchPb {
46
47 private static final long serialVersionUID = 1L;
48
49 /**
50 * sum of the coefficients of the literals satisfied or unvalued
51 */
52 private BigInteger watchCumul = BigInteger.ZERO;
53
54 /**
55 * Builds a PB constraint for a0.x0 + a1.x1 + ... + an.xn >= k
56 *
57 * This constructor is called for learnt pseudo boolean constraints.
58 *
59 * @param voc
60 * all the possible variables (vocabulary)
61 * @param mpb
62 * data structure which contains literals of the constraint,
63 * coefficients (a0, a1, ... an), and the degree of the
64 * constraint (k). The constraint is a "more than" constraint.
65 */
66 private MaxWatchPb(ILits voc, IDataStructurePB mpb) {
67
68 super(mpb);
69 this.voc = voc;
70
71 activity = 0;
72 watchCumul = BigInteger.ZERO;
73 }
74
75 /**
76 * Builds a PB constraint for a0.x0 + a1.x1 + ... + an.xn >= k
77 *
78 * @param voc
79 * all the possible variables (vocabulary)
80 * @param lits
81 * literals of the constraint (x0,x1, ... xn)
82 * @param coefs
83 * coefficients of the left side of the constraint (a0, a1, ...
84 * an)
85 * @param degree
86 * degree of the constraint (k)
87 */
88 private MaxWatchPb(ILits voc, int[] lits, BigInteger[] coefs,
89 BigInteger degree) {
90
91 super(lits, coefs, degree);
92 this.voc = voc;
93
94 activity = 0;
95 watchCumul = BigInteger.ZERO;
96 }
97
98 /**
99 * All the literals are watched.
100 *
101 * @see org.sat4j.pb.constraints.pb.WatchPb#computeWatches()
102 */
103 @Override
104 protected void computeWatches() throws ContradictionException {
105 assert watchCumul.equals(BigInteger.ZERO);
106 for (int i = 0; i < lits.length; i++) {
107 if (voc.isFalsified(lits[i])) {
108 if (learnt) {
109 voc.undos(lits[i] ^ 1).push(this);
110 voc.watch(lits[i] ^ 1, this);
111 }
112 } else {
113 // updating of the initial value for the counter
114 voc.watch(lits[i] ^ 1, this);
115 watchCumul = watchCumul.add(coefs[i]);
116 }
117 }
118
119 assert watchCumul.compareTo(computeLeftSide()) >= 0;
120 if (!learnt && watchCumul.compareTo(degree) < 0) {
121 throw new ContradictionException("non satisfiable constraint");
122 }
123 }
124
125 /*
126 * This method propagates any possible value.
127 *
128 * This method is only called in the factory methods.
129 *
130 * @see org.sat4j.minisat.constraints.WatchPb#computePropagation()
131 */
132 @Override
133 protected void computePropagation(UnitPropagationListener s)
134 throws ContradictionException {
135 // propagate any possible value
136 int ind = 0;
137 while (ind < coefs.length
138 && watchCumul.subtract(coefs[ind]).compareTo(degree) < 0) {
139 if (voc.isUnassigned(lits[ind]) && !s.enqueue(lits[ind], this))
140 // because this happens during the building of a constraint.
141 throw new ContradictionException("non satisfiable constraint");
142 ind++;
143 }
144 assert watchCumul.compareTo(computeLeftSide()) >= 0;
145 }
146
147 /**
148 * Propagation of a falsified literal
149 *
150 * @param s
151 * the solver
152 * @param p
153 * the propagated literal (it must be falsified)
154 * @return false iff there is a conflict
155 */
156 public boolean propagate(UnitPropagationListener s, int p) {
157 voc.watch(p, this);
158
159 assert watchCumul.compareTo(computeLeftSide()) >= 0 : "" + watchCumul
160 + "/" + computeLeftSide() + ":" + learnt;
161
162 // finding the index for p in the array of literals
163 int indiceP = 0;
164 while ((lits[indiceP] ^ 1) != p)
165 indiceP++;
166
167 // compute the new value for watchCumul
168 BigInteger coefP = coefs[indiceP];
169 BigInteger newcumul = watchCumul.subtract(coefP);
170
171 if (newcumul.compareTo(degree) < 0) {
172 // there is a conflict
173 assert !isSatisfiable();
174 return false;
175 }
176
177 // if no conflict, not(p) can be propagated
178 // allow a later un-assignation
179 voc.undos(p).push(this);
180 // really update watchCumul
181 watchCumul = newcumul;
182
183 // propagation
184 int ind = 0;
185 // limit is the margin between the sum of the coefficients of the
186 // satisfied+unassigned literals
187 // and the degree of the constraint
188 BigInteger limit = watchCumul.subtract(degree);
189 // for each coefficient greater than limit
190 while (ind < coefs.length && limit.compareTo(coefs[ind]) < 0) {
191 // its corresponding literal is implied
192 if (voc.isUnassigned(lits[ind]) && (!s.enqueue(lits[ind], this))) {
193 // if it is not possible then there is a conflict
194 assert !isSatisfiable();
195 return false;
196 }
197 ind++;
198 }
199
200 assert learnt || watchCumul.compareTo(computeLeftSide()) >= 0;
201 assert watchCumul.compareTo(computeLeftSide()) >= 0;
202 return true;
203 }
204
205 /**
206 * Remove a constraint from the solver
207 */
208 public void remove(UnitPropagationListener upl) {
209 for (int i = 0; i < lits.length; i++) {
210 if (!voc.isFalsified(lits[i]))
211 voc.watches(lits[i] ^ 1).remove(this);
212 }
213 }
214
215 /**
216 * this method is called during backtrack
217 *
218 * @param p
219 * an unassigned literal
220 */
221 public void undo(int p) {
222 int indiceP = 0;
223 while ((lits[indiceP] ^ 1) != p)
224 indiceP++;
225
226 assert coefs[indiceP].signum() > 0;
227
228 watchCumul = watchCumul.add(coefs[indiceP]);
229 }
230
231 /**
232 * build a pseudo boolean constraint. Coefficients are positive integers
233 * less than or equal to the degree (this is called a normalized
234 * constraint).
235 *
236 * @param s
237 * a unit propagation listener (usually the solver)
238 * @param voc
239 * the vocabulary
240 * @param lits
241 * the literals of the constraint
242 * @param coefs
243 * the coefficients of the constraint
244 * @param degree
245 * the degree of the constraint
246 * @return a new PB constraint or null if a trivial inconsistency is
247 * detected.
248 */
249 public static MaxWatchPb normalizedMaxWatchPbNew(UnitPropagationListener s,
250 ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree)
251 throws ContradictionException {
252 // Parameters must not be modified
253 MaxWatchPb outclause = new MaxWatchPb(voc, lits, coefs, degree);
254
255 if (outclause.degree.signum() <= 0) {
256 return null;
257 }
258
259 outclause.computeWatches();
260
261 outclause.computePropagation(s);
262
263 return outclause;
264
265 }
266
267 /**
268 * build a pseudo boolean constraint from a specific data structure. For
269 * learnt constraints.
270 *
271 * @param s
272 * a unit propagation listener (usually the solver)
273 * @param mpb
274 * data structure which contains literals of the constraint,
275 * coefficients (a0, a1, ... an), and the degree of the
276 * constraint (k). The constraint is a "more than" constraint.
277 * @return a new PB constraint or null if a trivial inconsistency is
278 * detected.
279 */
280 public static WatchPb normalizedWatchPbNew(ILits voc, IDataStructurePB mpb) {
281 return new MaxWatchPb(voc, mpb);
282 }
283
284 }