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