1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30 package org.sat4j.pb.core;
31
32 import java.io.PrintStream;
33 import java.io.PrintWriter;
34 import java.math.BigInteger;
35 import java.util.ArrayList;
36 import java.util.HashSet;
37 import java.util.Iterator;
38 import java.util.List;
39 import java.util.Map;
40 import java.util.Set;
41
42 import org.sat4j.core.Vec;
43 import org.sat4j.core.VecInt;
44 import org.sat4j.pb.IPBSolver;
45 import org.sat4j.pb.ObjectiveFunction;
46 import org.sat4j.specs.ContradictionException;
47 import org.sat4j.specs.IConstr;
48 import org.sat4j.specs.ISolver;
49 import org.sat4j.specs.ISolverService;
50 import org.sat4j.specs.IVec;
51 import org.sat4j.specs.IVecInt;
52 import org.sat4j.specs.IteratorInt;
53 import org.sat4j.specs.SearchListener;
54 import org.sat4j.specs.TimeoutException;
55
56 public class ObjectiveReducerPBSolverDecorator implements IPBSolver {
57
58 private static final long serialVersionUID = -1637773414229087105L;
59
60 private final IPBSolver decorated;
61
62 private final List<IVecInt> atMostOneCstrs = new ArrayList<IVecInt>();
63
64 public ObjectiveReducerPBSolverDecorator(IPBSolver decorated) {
65 this.decorated = decorated;
66 }
67
68 public int[] model() {
69 return decorated.model();
70 }
71
72 @SuppressWarnings("deprecation")
73 public int newVar() {
74 return decorated.newVar();
75 }
76
77 public IConstr addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs,
78 boolean moreThan, BigInteger d) throws ContradictionException {
79 return decorated.addPseudoBoolean(lits, coeffs, moreThan, d);
80 }
81
82 public boolean model(int var) {
83 return decorated.model(var);
84 }
85
86 public int nextFreeVarId(boolean reserve) {
87 return decorated.nextFreeVarId(reserve);
88 }
89
90 public int[] primeImplicant() {
91 return decorated.primeImplicant();
92 }
93
94 public boolean primeImplicant(int p) {
95 return decorated.primeImplicant(p);
96 }
97
98 public IConstr addAtMost(IVecInt literals, IVecInt coeffs, int degree)
99 throws ContradictionException {
100 for (IteratorInt it = coeffs.iterator(); it.hasNext();) {
101 if (it.next() != degree) {
102 return decorated.addAtMost(literals, coeffs, degree);
103 }
104 }
105 this.atMostOneCstrs.add(literals);
106 return decorated.addAtMost(literals, coeffs, degree);
107 }
108
109 public boolean isSatisfiable() throws TimeoutException {
110 return decorated.isSatisfiable();
111 }
112
113 public boolean isSatisfiable(IVecInt assumps, boolean globalTimeout)
114 throws TimeoutException {
115 return decorated.isSatisfiable(assumps, globalTimeout);
116 }
117
118 public void registerLiteral(int p) {
119 decorated.registerLiteral(p);
120 }
121
122 public void setExpectedNumberOfClauses(int nb) {
123 decorated.setExpectedNumberOfClauses(nb);
124 }
125
126 public IConstr addAtMost(IVecInt literals, IVec<BigInteger> coeffs,
127 BigInteger degree) throws ContradictionException {
128 for (Iterator<BigInteger> it = coeffs.iterator(); it.hasNext();) {
129 if (!it.next().equals(degree)) {
130 return decorated.addAtMost(literals, coeffs, degree);
131 }
132 }
133 this.atMostOneCstrs.add(literals);
134 return decorated.addAtMost(literals, coeffs, degree);
135 }
136
137 public boolean isSatisfiable(boolean globalTimeout) throws TimeoutException {
138 return decorated.isSatisfiable(globalTimeout);
139 }
140
141 public IConstr addClause(IVecInt literals) throws ContradictionException {
142 return decorated.addClause(literals);
143 }
144
145 public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
146 return decorated.isSatisfiable(assumps);
147 }
148
149 public IConstr addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
150 throws ContradictionException {
151 return decorated.addAtLeast(literals, coeffs, degree);
152 }
153
154 public int[] findModel() throws TimeoutException {
155 return decorated.findModel();
156 }
157
158 public IConstr addBlockingClause(IVecInt literals)
159 throws ContradictionException {
160 return decorated.addBlockingClause(literals);
161 }
162
163 public boolean removeConstr(IConstr c) {
164 return decorated.removeConstr(c);
165 }
166
167 public int[] findModel(IVecInt assumps) throws TimeoutException {
168 return decorated.findModel(assumps);
169 }
170
171 public IConstr addAtLeast(IVecInt literals, IVec<BigInteger> coeffs,
172 BigInteger degree) throws ContradictionException {
173 return decorated.addAtLeast(literals, coeffs, degree);
174 }
175
176 public boolean removeSubsumedConstr(IConstr c) {
177 return decorated.removeSubsumedConstr(c);
178 }
179
180 public int nConstraints() {
181 return decorated.nConstraints();
182 }
183
184 public int newVar(int howmany) {
185 return decorated.newVar(howmany);
186 }
187
188 public void addAllClauses(IVec<IVecInt> clauses)
189 throws ContradictionException {
190 for (Iterator<IVecInt> it = clauses.iterator(); it.hasNext();) {
191 addClause(it.next());
192 }
193 }
194
195 public IConstr addExactly(IVecInt literals, IVecInt coeffs, int weight)
196 throws ContradictionException {
197 return decorated.addExactly(literals, coeffs, weight);
198 }
199
200 public int nVars() {
201 return decorated.nVars();
202 }
203
204 @SuppressWarnings("deprecation")
205 public void printInfos(PrintWriter out, String prefix) {
206 decorated.printInfos(out, prefix);
207 }
208
209 public IConstr addAtMost(IVecInt literals, int degree)
210 throws ContradictionException {
211 if (degree == 1) {
212 this.atMostOneCstrs.add(literals);
213 }
214 return decorated.addAtMost(literals, degree);
215 }
216
217 public IConstr addExactly(IVecInt literals, IVec<BigInteger> coeffs,
218 BigInteger weight) throws ContradictionException {
219 return decorated.addExactly(literals, coeffs, weight);
220 }
221
222 public void printInfos(PrintWriter out) {
223 decorated.printInfos(out);
224 }
225
226 public IConstr addAtLeast(IVecInt literals, int degree)
227 throws ContradictionException {
228 return decorated.addAtLeast(literals, degree);
229 }
230
231 public void setObjectiveFunction(ObjectiveFunction obj) {
232 if (obj != null) {
233 IVecInt newVars = new VecInt();
234 IVec<BigInteger> newCoeffs = new Vec<BigInteger>();
235 Set<Integer> oldVarsToIgnore = new HashSet<Integer>();
236 IVecInt oldObjVars = obj.getVars();
237 IVec<BigInteger> oldObjCoeffs = obj.getCoeffs();
238 int nbReduc;
239 nbReduc = processAtMostOneCstrs(obj, newVars, newCoeffs,
240 oldVarsToIgnore);
241 System.out.println("c " + nbReduc
242 + " reductions due to atMostOne constraints");
243 for (int i = 0; i < oldObjVars.size(); ++i) {
244 if (!oldVarsToIgnore.contains(oldObjVars.get(i))) {
245 newVars.push(oldObjVars.get(i));
246 newCoeffs.push(oldObjCoeffs.get(i));
247 }
248 }
249 obj = new ObjectiveFunction(newVars, newCoeffs);
250 }
251 decorated.setObjectiveFunction(obj);
252 }
253
254 private int processAtMostOneCstrs(ObjectiveFunction obj, IVecInt newVars,
255 IVec<BigInteger> newCoeffs, Set<Integer> oldVarsToIgnore) {
256 System.out.println("c " + this.atMostOneCstrs.size()
257 + " atMostOne constraints found");
258 int nbReduc = 0;
259 IVecInt oldObjVars = obj.getVars();
260 IVec<BigInteger> oldObjCoeffs = obj.getCoeffs();
261 for (IVecInt lits : this.atMostOneCstrs) {
262 boolean allLitsIn = true;
263 for (IteratorInt it = lits.iterator(); it.hasNext();) {
264 int next = it.next();
265 if (oldVarsToIgnore.contains(next)) {
266 allLitsIn = false;
267 break;
268 }
269 int indexOf = oldObjVars.indexOf(next);
270 if (indexOf == -1
271 || !oldObjCoeffs.get(indexOf).equals(BigInteger.ONE)) {
272 allLitsIn = false;
273 break;
274 }
275 }
276 if (allLitsIn) {
277 int newObjVar = nextFreeVarId(true);
278 try {
279 for (IteratorInt it = lits.iterator(); it.hasNext();) {
280 int nextInt = it.next();
281 this.decorated.addClause(new VecInt(new int[] {
282 nextInt, newObjVar }));
283 oldVarsToIgnore.add(Integer.valueOf(nextInt));
284 ++nbReduc;
285 }
286 } catch (ContradictionException e) {
287
288 e.printStackTrace();
289 }
290
291 newVars.push(newObjVar);
292 newCoeffs.push(BigInteger.ONE);
293 --nbReduc;
294 }
295 }
296 return nbReduc;
297 }
298
299 public ObjectiveFunction getObjectiveFunction() {
300 return decorated.getObjectiveFunction();
301 }
302
303 public IConstr addExactly(IVecInt literals, int n)
304 throws ContradictionException {
305 return decorated.addExactly(literals, n);
306 }
307
308 public void setTimeout(int t) {
309 decorated.setTimeout(t);
310 }
311
312 public void setTimeoutOnConflicts(int count) {
313 decorated.setTimeoutOnConflicts(count);
314 }
315
316 public void setTimeoutMs(long t) {
317 decorated.setTimeoutMs(t);
318 }
319
320 public int getTimeout() {
321 return decorated.getTimeout();
322 }
323
324 public long getTimeoutMs() {
325 return decorated.getTimeoutMs();
326 }
327
328 public void expireTimeout() {
329 decorated.expireTimeout();
330 }
331
332 public void reset() {
333 decorated.reset();
334 }
335
336 @SuppressWarnings("deprecation")
337 public void printStat(PrintStream out, String prefix) {
338 decorated.printStat(out, prefix);
339 }
340
341 @SuppressWarnings("deprecation")
342 public void printStat(PrintWriter out, String prefix) {
343 decorated.printStat(out, prefix);
344 }
345
346 public void printStat(PrintWriter out) {
347 decorated.printStat(out);
348 }
349
350 public Map<String, Number> getStat() {
351 return decorated.getStat();
352 }
353
354 public String toString(String prefix) {
355 return decorated.toString(prefix);
356 }
357
358 public void clearLearntClauses() {
359 decorated.clearLearntClauses();
360 }
361
362 public void setDBSimplificationAllowed(boolean status) {
363 decorated.setDBSimplificationAllowed(status);
364 }
365
366 public boolean isDBSimplificationAllowed() {
367 return decorated.isDBSimplificationAllowed();
368 }
369
370 public <S extends ISolverService> void setSearchListener(
371 SearchListener<S> sl) {
372 decorated.setSearchListener(sl);
373 }
374
375 public <S extends ISolverService> SearchListener<S> getSearchListener() {
376 return decorated.getSearchListener();
377 }
378
379 public boolean isVerbose() {
380 return decorated.isVerbose();
381 }
382
383 public void setVerbose(boolean value) {
384 decorated.setVerbose(value);
385 }
386
387 public void setLogPrefix(String prefix) {
388 decorated.setLogPrefix(prefix);
389 }
390
391 public String getLogPrefix() {
392 return decorated.getLogPrefix();
393 }
394
395 public IVecInt unsatExplanation() {
396 return decorated.unsatExplanation();
397 }
398
399 public int[] modelWithInternalVariables() {
400 return decorated.modelWithInternalVariables();
401 }
402
403 public int realNumberOfVariables() {
404 return decorated.realNumberOfVariables();
405 }
406
407 public boolean isSolverKeptHot() {
408 return decorated.isSolverKeptHot();
409 }
410
411 public void setKeepSolverHot(boolean keepHot) {
412 decorated.setKeepSolverHot(keepHot);
413 }
414
415 public ISolver getSolvingEngine() {
416 return decorated.getSolvingEngine();
417 }
418
419 }