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.minisat.constraints.card;
31
32 import java.io.Serializable;
33
34 import org.sat4j.minisat.constraints.cnf.Lits;
35 import org.sat4j.minisat.constraints.cnf.UnitClauses;
36 import org.sat4j.minisat.core.Constr;
37 import org.sat4j.minisat.core.ILits;
38 import org.sat4j.minisat.core.Propagatable;
39 import org.sat4j.minisat.core.Undoable;
40 import org.sat4j.minisat.core.UnitPropagationListener;
41 import org.sat4j.specs.ContradictionException;
42 import org.sat4j.specs.IVecInt;
43
44 /**
45 * @author leberre Contrainte de cardinalit?
46 */
47 public class AtLeast implements Propagatable, Constr, Undoable, Serializable {
48
49 private static final long serialVersionUID = 1L;
50
51 /** number of allowed falsified literal */
52 protected int maxUnsatisfied;
53
54 /** current number of falsified literals */
55 private int counter;
56
57 /**
58 * constraint literals
59 */
60 protected final int[] lits;
61
62 protected final ILits voc;
63
64 /**
65 * @param ps
66 * a vector of literals
67 * @param degree
68 * the minimal number of satisfied literals
69 */
70 protected AtLeast(ILits voc, IVecInt ps, int degree) {
71 this.maxUnsatisfied = ps.size() - degree;
72 this.voc = voc;
73 this.counter = 0;
74 this.lits = new int[ps.size()];
75 ps.moveTo(this.lits);
76 for (int q : this.lits) {
77 voc.watch(q ^ 1, this);
78 }
79 }
80
81 protected static int niceParameters(UnitPropagationListener s, ILits voc,
82 IVecInt ps, int deg) throws ContradictionException {
83
84 if (ps.size() < deg) {
85 throw new ContradictionException();
86 }
87 int degree = deg;
88 for (int i = 0; i < ps.size();) {
89 // on verifie si le litteral est affecte
90 if (voc.isUnassigned(ps.get(i))) {
91 // go to next literal
92 i++;
93 } else {
94 // Si le litteral est satisfait,
95 // ?a revient ? baisser le degr?
96 if (voc.isSatisfied(ps.get(i))) {
97 degree--;
98 }
99 // dans tous les cas, s'il est assign?,
100 // on enleve le ieme litteral
101 ps.delete(i);
102 }
103 }
104
105 // on trie le vecteur ps
106 ps.sortUnique();
107 // ?limine les clauses tautologiques
108 // deux litt?raux de signe oppos?s apparaissent dans la m?me
109 // clause
110
111 if (ps.size() == degree) {
112 for (int i = 0; i < ps.size(); i++) {
113 if (!s.enqueue(ps.get(i))) {
114 throw new ContradictionException();
115 }
116 }
117 return 0;
118 }
119
120 if (ps.size() < degree) {
121 throw new ContradictionException();
122 }
123 return degree;
124
125 }
126
127 /**
128 * @since 2.1
129 */
130 public static Constr atLeastNew(UnitPropagationListener s, ILits voc,
131 IVecInt ps, int n) throws ContradictionException {
132 int degree = niceParameters(s, voc, ps, n);
133 if (degree == 0) {
134 return new UnitClauses(ps);
135 }
136 return new AtLeast(voc, ps, degree);
137 }
138
139 /**
140 * @since 2.1
141 */
142 public void remove(UnitPropagationListener upl) {
143 for (int q : this.lits) {
144 this.voc.watches(q ^ 1).remove(this);
145 }
146 }
147
148 /*
149 * (non-Javadoc)
150 *
151 * @see Constr#propagate(Solver, Lit)
152 */
153 public boolean propagate(UnitPropagationListener s, int p) {
154 // remet la clause dans la liste des clauses regardees
155 this.voc.watch(p, this);
156
157 if (this.counter == this.maxUnsatisfied) {
158 return false;
159 }
160
161 this.counter++;
162 this.voc.undos(p).push(this);
163
164 // If no more can be false, enqueue the rest:
165 if (this.counter == this.maxUnsatisfied) {
166 for (int q : this.lits) {
167 if (this.voc.isUnassigned(q) && !s.enqueue(q, this)) {
168 return false;
169 }
170 }
171 }
172 return true;
173 }
174
175 /*
176 * (non-Javadoc)
177 *
178 * @see Constr#simplify(Solver)
179 */
180 public boolean simplify() {
181 return false;
182 }
183
184 /*
185 * (non-Javadoc)
186 *
187 * @see Constr#undo(Solver, Lit)
188 */
189 public void undo(int p) {
190 this.counter--;
191 }
192
193 /*
194 * (non-Javadoc)
195 *
196 * @see Constr#calcReason(Solver, Lit, Vec)
197 */
198 public void calcReason(int p, IVecInt outReason) {
199 int c = p == ILits.UNDEFINED ? -1 : 0;
200 for (int q : this.lits) {
201 if (this.voc.isFalsified(q)) {
202 outReason.push(q ^ 1);
203 if (++c == this.maxUnsatisfied) {
204 return;
205 }
206 }
207 }
208 }
209
210 /*
211 * (non-Javadoc)
212 *
213 * @see org.sat4j.minisat.datatype.Constr#learnt()
214 */
215 public boolean learnt() {
216 // Ces contraintes ne sont pas apprises pour le moment.
217 return false;
218 }
219
220 /*
221 * (non-Javadoc)
222 *
223 * @see org.sat4j.minisat.datatype.Constr#getActivity()
224 */
225 public double getActivity() {
226 return 0;
227 }
228
229 public void setActivity(double d) {
230 }
231
232 /*
233 * (non-Javadoc)
234 *
235 * @see org.sat4j.minisat.datatype.Constr#incActivity(double)
236 */
237 public void incActivity(double claInc) {
238 }
239
240 /*
241 * For learnt clauses only @author leberre
242 */
243 public boolean locked() {
244 // FIXME need to be adapted to AtLeast
245 // return lits[0].getReason() == this;
246 return true;
247 }
248
249 public void setLearnt() {
250 throw new UnsupportedOperationException();
251 }
252
253 public void register() {
254 throw new UnsupportedOperationException();
255 }
256
257 public int size() {
258 return this.lits.length;
259 }
260
261 public int get(int i) {
262 return this.lits[i];
263 }
264
265 public void rescaleBy(double d) {
266 throw new UnsupportedOperationException();
267 }
268
269 public void assertConstraint(UnitPropagationListener s) {
270 throw new UnsupportedOperationException();
271 }
272
273 /**
274 * Textual representation of the constraint
275 *
276 * @return a string representing the constraint.
277 */
278 @Override
279 public String toString() {
280 StringBuffer stb = new StringBuffer();
281 stb.append("Card (" + this.lits.length + ") : ");
282 for (int lit : this.lits) {
283 // if (voc.isUnassigned(lits[i])) {
284 stb.append(" + "); //$NON-NLS-1$
285 stb.append(Lits.toString(lit));
286 stb.append("[");
287 stb.append(this.voc.valueToString(lit));
288 stb.append("@");
289 stb.append(this.voc.getLevel(lit));
290 stb.append("] ");
291 }
292 stb.append(">= "); //$NON-NLS-1$
293 stb.append(size() - this.maxUnsatisfied);
294
295 return stb.toString();
296 }
297
298 /**
299 * @since 2.1
300 */
301 public void forwardActivity(double claInc) {
302 // TODO Auto-generated method stub
303
304 }
305
306 public boolean canBePropagatedMultipleTimes() {
307 return true;
308 }
309
310 public Constr toConstraint() {
311 return this;
312 }
313 }