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;
31
32 import java.math.BigInteger;
33
34 import org.sat4j.core.VecInt;
35 import org.sat4j.specs.ContradictionException;
36 import org.sat4j.specs.IConstr;
37 import org.sat4j.specs.IOptimizationProblem;
38 import org.sat4j.specs.IVecInt;
39 import org.sat4j.specs.TimeoutException;
40
41
42
43
44
45
46
47 public class PseudoOptDecorator extends PBSolverDecorator implements
48 IOptimizationProblem {
49
50
51
52
53 private static final long serialVersionUID = 1L;
54
55 private BigInteger objectiveValue;
56
57 private int[] prevmodel;
58 private int[] prevmodelwithadditionalvars;
59
60 private boolean[] prevfullmodel;
61
62 private IConstr previousPBConstr;
63
64 private boolean isSolutionOptimal;
65
66 private final boolean nonOptimalMeansSatisfiable;
67
68 private final boolean useAnImplicantForEvaluation;
69
70 private int solverTimeout = Integer.MAX_VALUE;
71
72 private int optimizationTimeout = -1;
73
74
75
76
77
78
79
80
81 public PseudoOptDecorator(IPBSolver solver) {
82 this(solver, true);
83 }
84
85
86
87
88
89
90
91
92
93
94
95 public PseudoOptDecorator(IPBSolver solver,
96 boolean nonOptimalMeansSatisfiable) {
97 this(solver, nonOptimalMeansSatisfiable, false);
98 }
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114 public PseudoOptDecorator(IPBSolver solver,
115 boolean nonOptimalMeansSatisfiable,
116 boolean useAnImplicantForEvaluation) {
117 super(solver);
118 this.nonOptimalMeansSatisfiable = nonOptimalMeansSatisfiable;
119 this.useAnImplicantForEvaluation = useAnImplicantForEvaluation;
120 }
121
122 @Override
123 public boolean isSatisfiable() throws TimeoutException {
124 return isSatisfiable(VecInt.EMPTY);
125 }
126
127 @Override
128 public boolean isSatisfiable(boolean global) throws TimeoutException {
129 return isSatisfiable(VecInt.EMPTY, global);
130 }
131
132 @Override
133 public boolean isSatisfiable(IVecInt assumps, boolean global)
134 throws TimeoutException {
135 boolean result = super.isSatisfiable(assumps, true);
136 if (result) {
137 this.prevmodel = super.model();
138 this.prevmodelwithadditionalvars = super
139 .modelWithInternalVariables();
140 this.prevfullmodel = new boolean[nVars()];
141 for (int i = 0; i < nVars(); i++) {
142 this.prevfullmodel[i] = decorated().model(i + 1);
143 }
144 if (optimizationTimeout > 0) {
145 super.expireTimeout();
146 super.setTimeout(optimizationTimeout);
147 }
148
149 } else {
150 if (this.previousPBConstr != null) {
151 decorated().removeConstr(this.previousPBConstr);
152 this.previousPBConstr = null;
153 }
154 super.setTimeout(solverTimeout);
155 }
156 return result;
157 }
158
159 @Override
160 public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
161 return isSatisfiable(assumps, true);
162 }
163
164 @Override
165 public void setObjectiveFunction(ObjectiveFunction objf) {
166 decorated().setObjectiveFunction(objf);
167 }
168
169 public boolean admitABetterSolution() throws TimeoutException {
170 return admitABetterSolution(VecInt.EMPTY);
171 }
172
173 public boolean admitABetterSolution(IVecInt assumps)
174 throws TimeoutException {
175 try {
176 this.isSolutionOptimal = false;
177 boolean result = super.isSatisfiable(assumps, true);
178 if (result) {
179 if (this.useAnImplicantForEvaluation) {
180 this.prevmodel = modelWithAdaptedNonPrimeLiterals();
181
182 } else {
183 this.prevmodel = super.model();
184 }
185 this.prevmodelwithadditionalvars = super
186 .modelWithInternalVariables();
187 this.prevfullmodel = new boolean[nVars()];
188 for (int i = 0; i < nVars(); i++) {
189 this.prevfullmodel[i] = decorated().model(i + 1);
190 }
191 if (decorated().getObjectiveFunction() != null) {
192 calculateObjective();
193 }
194 if (optimizationTimeout > 0) {
195 super.expireTimeout();
196 super.setTimeout(optimizationTimeout);
197 }
198 } else {
199 this.isSolutionOptimal = true;
200 if (this.previousPBConstr != null) {
201 decorated().removeConstr(this.previousPBConstr);
202 this.previousPBConstr = null;
203 }
204 }
205 return result;
206 } catch (TimeoutException te) {
207 if (this.previousPBConstr != null) {
208 decorated().removeConstr(this.previousPBConstr);
209 this.previousPBConstr = null;
210 }
211 throw te;
212 }
213 }
214
215 private int[] modelWithAdaptedNonPrimeLiterals() {
216
217 int[] completeModel = new int[nVars()];
218 int var;
219 for (int i = 0; i < nVars(); i++) {
220 var = i + 1;
221 completeModel[i] = super.model(var) ? var : -var;
222 }
223 primeImplicant();
224 ObjectiveFunction obj = getObjectiveFunction();
225 for (int i = 0; i < obj.getVars().size(); i++) {
226 int d = obj.getVars().get(i);
227 BigInteger coeff = obj.getCoeffs().get(i);
228 if (d <= nVars() && !primeImplicant(d) && !primeImplicant(-d)) {
229
230
231 assert Math.abs(completeModel[Math.abs(d) - 1]) == d;
232 if (coeff.signum() * d < 0) {
233 completeModel[Math.abs(d) - 1] = Math.abs(d);
234 } else {
235 completeModel[Math.abs(d) - 1] = -Math.abs(d);
236 }
237 }
238 }
239 return completeModel;
240 }
241
242 public boolean hasNoObjectiveFunction() {
243 return decorated().getObjectiveFunction() == null;
244 }
245
246 public boolean nonOptimalMeansSatisfiable() {
247 return nonOptimalMeansSatisfiable;
248 }
249
250 public Number calculateObjective() {
251 if (decorated().getObjectiveFunction() == null) {
252 throw new UnsupportedOperationException(
253 "The problem does not contain an objective function");
254 }
255 if (this.useAnImplicantForEvaluation) {
256 this.objectiveValue = decorated().getObjectiveFunction()
257 .calculateDegreeImplicant(decorated());
258 } else {
259 this.objectiveValue = decorated().getObjectiveFunction()
260 .calculateDegree(decorated());
261 }
262 return getObjectiveValue();
263 }
264
265 public void discardCurrentSolution() throws ContradictionException {
266 if (this.previousPBConstr != null) {
267 super.removeSubsumedConstr(this.previousPBConstr);
268 }
269 if (decorated().getObjectiveFunction() != null
270 && this.objectiveValue != null) {
271 this.previousPBConstr = super.addPseudoBoolean(decorated()
272 .getObjectiveFunction().getVars(), decorated()
273 .getObjectiveFunction().getCoeffs(), false,
274 this.objectiveValue.subtract(BigInteger.ONE));
275 }
276 }
277
278 @Override
279 public void reset() {
280 this.previousPBConstr = null;
281 super.reset();
282 }
283
284 @Override
285 public int[] model() {
286
287 return this.prevmodel;
288 }
289
290 @Override
291 public boolean model(int var) {
292 return this.prevfullmodel[var - 1];
293 }
294
295 @Override
296 public String toString(String prefix) {
297 return prefix
298 + "Pseudo Boolean Optimization by upper bound\n"
299 + prefix
300 + (useAnImplicantForEvaluation ? "using prime implicants for evaluating the objective function\n"
301 : "") + super.toString(prefix);
302 }
303
304 public Number getObjectiveValue() {
305 return this.objectiveValue.add(decorated().getObjectiveFunction()
306 .getCorrection());
307 }
308
309 public void discard() throws ContradictionException {
310 discardCurrentSolution();
311 }
312
313 public void forceObjectiveValueTo(Number forcedValue)
314 throws ContradictionException {
315 super.addPseudoBoolean(decorated().getObjectiveFunction().getVars(),
316 decorated().getObjectiveFunction().getCoeffs(), false,
317 (BigInteger) forcedValue);
318 }
319
320 public boolean isOptimal() {
321 return this.isSolutionOptimal;
322 }
323
324 @Override
325 public int[] modelWithInternalVariables() {
326 return this.prevmodelwithadditionalvars;
327 }
328
329 public void setTimeoutForFindingBetterSolution(int seconds) {
330 optimizationTimeout = seconds;
331 }
332
333 @Override
334 public void setTimeout(int t) {
335 solverTimeout = t;
336 super.setTimeout(t);
337 }
338 }