1 /*
2 * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3 *
4 * Based on the original minisat specification from:
5 *
6 * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7 * Sixth International Conference on Theory and Applications of Satisfiability
8 * Testing, LNCS 2919, pp 502-518, 2003.
9 *
10 * This library is free software; you can redistribute it and/or modify it under
11 * the terms of the GNU Lesser General Public License as published by the Free
12 * Software Foundation; either version 2.1 of the License, or (at your option)
13 * any later version.
14 *
15 * This library is distributed in the hope that it will be useful, but WITHOUT
16 * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17 * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18 * details.
19 *
20 * You should have received a copy of the GNU Lesser General Public License
21 * along with this library; if not, write to the Free Software Foundation, Inc.,
22 * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
23 *
24 */
25
26 package org.sat4j.minisat.constraints.card;
27
28 import java.io.Serializable;
29
30 import org.sat4j.minisat.constraints.cnf.Lits;
31 import org.sat4j.minisat.core.Constr;
32 import org.sat4j.minisat.core.ILits;
33 import org.sat4j.minisat.core.Undoable;
34 import org.sat4j.minisat.core.UnitPropagationListener;
35 import org.sat4j.specs.ContradictionException;
36 import org.sat4j.specs.IVecInt;
37
38 /*
39 * Created on 8 janv. 2004 To change the template for this generated file go to
40 * Window>Preferences>Java>Code Generation>Code and Comments
41 */
42
43 /**
44 * @author leberre Contrainte de cardinalit?
45 */
46 public class AtLeast implements Constr, Undoable, Serializable {
47
48 private static final long serialVersionUID = 1L;
49
50 /** number of allowed falsified literal */
51 protected int maxUnsatisfied;
52
53 /** current number of falsified literals */
54 private int counter;
55
56 /**
57 * constraint literals
58 */
59 protected final int[] lits;
60
61 protected final ILits voc;
62
63 /**
64 * @param ps
65 * a vector of literals
66 * @param degree
67 * the minimal number of satisfied literals
68 */
69 protected AtLeast(ILits voc, IVecInt ps, int degree) {
70 maxUnsatisfied = ps.size() - degree;
71 this.voc = voc;
72 counter = 0;
73 lits = new int[ps.size()];
74 ps.moveTo(lits);
75 for (int q : lits) {
76 voc.watch(q ^ 1, this);
77 }
78 }
79
80 protected static int niceParameters(UnitPropagationListener s, ILits voc,
81 IVecInt ps, int deg) throws ContradictionException {
82
83 if (ps.size() < deg)
84 throw new ContradictionException();
85 int degree = deg;
86 for (int i = 0; i < ps.size();) {
87 // on verifie si le litteral est affecte
88 if (voc.isUnassigned(ps.get(i))) {
89 // go to next literal
90 i++;
91 } else {
92 // Si le litteral est satisfait,
93 // ?a revient ? baisser le degr?
94 if (voc.isSatisfied(ps.get(i))) {
95 degree--;
96 }
97 // dans tous les cas, s'il est assign?,
98 // on enleve le ieme litteral
99 ps.delete(i);
100 }
101 }
102
103 // on trie le vecteur ps
104 ps.sortUnique();
105 // ?limine les clauses tautologiques
106 // deux litt?raux de signe oppos?s apparaissent dans la m?me
107 // clause
108
109 if (ps.size() == degree) {
110 for (int i = 0; i < ps.size(); i++) {
111 if (!s.enqueue(ps.get(i))) {
112 throw new ContradictionException();
113 }
114 }
115 return 0;
116 }
117
118 if (ps.size() < degree)
119 throw new ContradictionException();
120 return degree;
121
122 }
123
124 public static AtLeast atLeastNew(UnitPropagationListener s, ILits voc,
125 IVecInt ps, int n) throws ContradictionException {
126 int degree = niceParameters(s, voc, ps, n);
127 if (degree == 0)
128 return null;
129 return new AtLeast(voc, ps, degree);
130 }
131
132 /*
133 * (non-Javadoc)
134 *
135 * @see Constr#remove(Solver)
136 */
137 public void remove() {
138 for (int q : lits) {
139 voc.watches(q ^ 1).remove(this);
140 }
141 }
142
143 /*
144 * (non-Javadoc)
145 *
146 * @see Constr#propagate(Solver, Lit)
147 */
148 public boolean propagate(UnitPropagationListener s, int p) {
149 // remet la clause dans la liste des clauses regardees
150 voc.watch(p, this);
151
152 if (counter == maxUnsatisfied)
153 return false;
154
155 counter++;
156 voc.undos(p).push(this);
157
158 // If no more can be false, enqueue the rest:
159 if (counter == maxUnsatisfied)
160 for (int q : lits) {
161 if (voc.isUnassigned(q) && !s.enqueue(q, this)) {
162 return false;
163 }
164 }
165 return true;
166 }
167
168 /*
169 * (non-Javadoc)
170 *
171 * @see Constr#simplify(Solver)
172 */
173 public boolean simplify() {
174 return false;
175 }
176
177 /*
178 * (non-Javadoc)
179 *
180 * @see Constr#undo(Solver, Lit)
181 */
182 public void undo(int p) {
183 counter--;
184 }
185
186 /*
187 * (non-Javadoc)
188 *
189 * @see Constr#calcReason(Solver, Lit, Vec)
190 */
191 public void calcReason(int p, IVecInt outReason) {
192 int c = (p == ILits.UNDEFINED) ? -1 : 0;
193 for (int q : lits) {
194 if (voc.isFalsified(q)) {
195 outReason.push(q ^ 1);
196 if (++c == maxUnsatisfied)
197 return;
198 }
199 }
200 }
201
202 /*
203 * (non-Javadoc)
204 *
205 * @see org.sat4j.minisat.datatype.Constr#learnt()
206 */
207 public boolean learnt() {
208 // Ces contraintes ne sont pas apprises pour le moment.
209 return false;
210 }
211
212 /*
213 * (non-Javadoc)
214 *
215 * @see org.sat4j.minisat.datatype.Constr#getActivity()
216 */
217 public double getActivity() {
218 // TODO Auto-generated method stub
219 return 0;
220 }
221
222 /*
223 * (non-Javadoc)
224 *
225 * @see org.sat4j.minisat.datatype.Constr#incActivity(double)
226 */
227 public void incActivity(double claInc) {
228 // TODO Auto-generated method stub
229
230 }
231
232 /*
233 * For learnt clauses only @author leberre
234 */
235 public boolean locked() {
236 // FIXME need to be adapted to AtLeast
237 // return lits[0].getReason() == this;
238 return true;
239 }
240
241 public void setLearnt() {
242 throw new UnsupportedOperationException();
243 }
244
245 public void register() {
246 throw new UnsupportedOperationException();
247 }
248
249 public int size() {
250 return lits.length;
251 }
252
253 public int get(int i) {
254 return lits[i];
255 }
256
257 public void rescaleBy(double d) {
258 throw new UnsupportedOperationException();
259 }
260
261 public void assertConstraint(UnitPropagationListener s) {
262 throw new UnsupportedOperationException();
263 }
264
265 /**
266 * Cha?ne repr?sentant la contrainte
267 *
268 * @return Cha?ne repr?sentant la contrainte
269 */
270 @Override
271 public String toString() {
272 StringBuffer stb = new StringBuffer();
273 stb.append("Card (" + lits.length + ") : ");
274 for (int i = 0; i < lits.length; i++) {
275 // if (voc.isUnassigned(lits[i])) {
276 stb.append(" + "); //$NON-NLS-1$
277 stb.append(Lits.toString(this.lits[i]));
278 stb.append("[");
279 stb.append(voc.valueToString(lits[i]));
280 stb.append("@");
281 stb.append(voc.getLevel(lits[i]));
282 stb.append("]");
283 stb.append(" ");
284 stb.append(" "); //$NON-NLS-1$
285 }
286 stb.append(">= "); //$NON-NLS-1$
287 stb.append(size() - maxUnsatisfied);
288
289 return stb.toString();
290 }
291
292 }