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 import java.util.Map;
34
35 import org.sat4j.specs.ContradictionException;
36 import org.sat4j.specs.IConstr;
37 import org.sat4j.specs.IVec;
38 import org.sat4j.specs.IVecInt;
39 import org.sat4j.specs.IteratorInt;
40 import org.sat4j.tools.DimacsStringSolver;
41
42
43
44
45
46
47
48 public class UserFriendlyPBStringSolver<T> extends DimacsStringSolver implements
49 IPBSolver {
50
51 private static final String FAKE_I_CONSTR_MSG = "Fake IConstr";
52
53
54
55
56 private static final long serialVersionUID = 1L;
57
58 private int indxConstrObj;
59
60 private int nbOfConstraints;
61
62 private ObjectiveFunction obj;
63
64 private boolean inserted = false;
65
66 private static final IConstr FAKE_CONSTR = new IConstr() {
67
68 public int size() {
69 throw new UnsupportedOperationException(FAKE_I_CONSTR_MSG);
70 }
71
72 public boolean learnt() {
73 throw new UnsupportedOperationException(FAKE_I_CONSTR_MSG);
74 }
75
76 public double getActivity() {
77 throw new UnsupportedOperationException(FAKE_I_CONSTR_MSG);
78 }
79
80 public int get(int i) {
81 throw new UnsupportedOperationException(FAKE_I_CONSTR_MSG);
82 }
83
84 public boolean canBePropagatedMultipleTimes() {
85 throw new UnsupportedOperationException(FAKE_I_CONSTR_MSG);
86 }
87 };
88
89 private Map<Integer, T> mapping;
90
91
92
93
94 public UserFriendlyPBStringSolver() {
95 }
96
97
98
99
100 public UserFriendlyPBStringSolver(int initSize) {
101 super(initSize);
102 }
103
104 public void setMapping(Map<Integer, T> mapping) {
105 this.mapping = mapping;
106 }
107
108 public IConstr addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs,
109 boolean moreThan, BigInteger d) throws ContradictionException {
110 StringBuffer out = getOut();
111 assert lits.size() == coeffs.size();
112 this.nbOfConstraints++;
113 if (moreThan) {
114 for (int i = 0; i < lits.size(); i++) {
115 out.append(coeffs.get(i) + " " + this.mapping.get(lits.get(i))
116 + " + ");
117 }
118 out.append(">= " + d + " ;\n");
119 } else {
120 for (int i = 0; i < lits.size(); i++) {
121 out.append(coeffs.get(i) + " " + this.mapping.get(lits.get(i))
122 + " + ");
123 }
124 out.append("<= " + d + " ;\n");
125 }
126 return FAKE_CONSTR;
127 }
128
129 public void setObjectiveFunction(ObjectiveFunction obj) {
130 this.obj = obj;
131 }
132
133 @Override
134 public IConstr addAtLeast(IVecInt literals, int degree)
135 throws ContradictionException {
136 StringBuffer out = getOut();
137 this.nbOfConstraints++;
138 for (IteratorInt iterator = literals.iterator(); iterator.hasNext();) {
139 out.append(this.mapping.get(iterator.next()));
140 out.append(" ");
141 if (iterator.hasNext()) {
142 out.append("+ ");
143 }
144 }
145 out.append(">= " + degree + " ;\n");
146 return FAKE_CONSTR;
147 }
148
149 @Override
150 public IConstr addAtMost(IVecInt literals, int degree)
151 throws ContradictionException {
152 StringBuffer out = getOut();
153 this.nbOfConstraints++;
154 for (IteratorInt iterator = literals.iterator(); iterator.hasNext();) {
155 out.append(this.mapping.get(iterator.next()));
156 out.append(" ");
157 if (iterator.hasNext()) {
158 out.append("+ ");
159 }
160 }
161 out.append("<= " + degree + " ;\n");
162 return FAKE_CONSTR;
163 }
164
165 @Override
166 public IConstr addClause(IVecInt literals) throws ContradictionException {
167 StringBuffer out = getOut();
168 this.nbOfConstraints++;
169 int lit;
170 boolean beginning = true;
171 for (IteratorInt iterator = literals.iterator(); iterator.hasNext();) {
172 lit = iterator.next();
173 if (lit > 0) {
174 if (beginning) {
175 out.append("-> ");
176 beginning = false;
177 }
178 out.append(this.mapping.get(lit));
179 } else {
180 if (!beginning) {
181 out.append(" NOT ");
182 }
183 out.append(this.mapping.get(-lit));
184 }
185 out.append(" ");
186 if (iterator.hasNext() && !beginning) {
187 out.append("OR ");
188 }
189 }
190 if (beginning) {
191 out.append("-> false");
192 }
193 out.append(" ;\n");
194 return FAKE_CONSTR;
195 }
196
197
198
199
200
201
202 public String getExplanation() {
203
204 return null;
205 }
206
207
208
209
210
211
212
213
214 public void setListOfVariablesForExplanation(IVecInt listOfVariables) {
215
216
217 }
218
219 @Override
220 public String toString() {
221 StringBuffer out = getOut();
222 if (!this.inserted) {
223 StringBuffer tmp = new StringBuffer();
224 tmp.append("* #variable= ");
225 tmp.append(nVars());
226 tmp.append(" #constraint= ");
227 tmp.append(this.nbOfConstraints);
228 tmp.append(" \n");
229 if (this.obj != null) {
230 tmp.append("min: ");
231 tmp.append(decode(this.obj));
232 tmp.append(" ;\n");
233 }
234 out.insert(this.indxConstrObj, tmp.toString());
235 this.inserted = true;
236 }
237 return out.toString();
238 }
239
240 private Object decode(ObjectiveFunction obj2) {
241 StringBuffer stb = new StringBuffer();
242 IVecInt vars = obj2.getVars();
243 IVec<BigInteger> coeffs = obj2.getCoeffs();
244 int lit;
245 for (int i = 0; i < vars.size(); i++) {
246 stb.append(coeffs.get(i));
247 stb.append(" ");
248 lit = vars.get(i);
249 if (lit > 0) {
250 stb.append(this.mapping.get(lit));
251 } else {
252 stb.append("~");
253 stb.append(this.mapping.get(-lit));
254 }
255 stb.append(" ");
256 }
257
258 return stb.toString();
259 }
260
261 @Override
262 public String toString(String prefix) {
263 return "OPB output solver";
264 }
265
266 @Override
267 public int newVar(int howmany) {
268 StringBuffer out = getOut();
269 setNbVars(howmany);
270
271 this.indxConstrObj = out.length();
272 out.append("\n");
273 return howmany;
274 }
275
276 @Override
277 public void setExpectedNumberOfClauses(int nb) {
278 }
279
280 public ObjectiveFunction getObjectiveFunction() {
281 return this.obj;
282 }
283
284 public IConstr addAtMost(IVecInt literals, IVecInt coeffs, int degree)
285 throws ContradictionException {
286 StringBuffer out = getOut();
287 assert literals.size() == coeffs.size();
288 this.nbOfConstraints++;
289 for (int i = 0; i < literals.size(); i++) {
290 out.append(coeffs.get(i) + " " + this.mapping.get(literals.get(i))
291 + " + ");
292 }
293 out.append("<= " + degree + " ;\n");
294 return FAKE_CONSTR;
295 }
296
297 public IConstr addAtMost(IVecInt literals, IVec<BigInteger> coeffs,
298 BigInteger degree) throws ContradictionException {
299 StringBuffer out = getOut();
300 assert literals.size() == coeffs.size();
301 this.nbOfConstraints++;
302 for (int i = 0; i < literals.size(); i++) {
303 out.append(coeffs.get(i) + " " + this.mapping.get(literals.get(i))
304 + " + ");
305 }
306 out.append("<= " + degree + " ;\n");
307 return FAKE_CONSTR;
308 }
309
310 public IConstr addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
311 throws ContradictionException {
312 StringBuffer out = getOut();
313 assert literals.size() == coeffs.size();
314 this.nbOfConstraints++;
315 for (int i = 0; i < literals.size(); i++) {
316 out.append(coeffs.get(i) + " " + this.mapping.get(literals.get(i))
317 + " + ");
318 }
319 out.append(">= " + degree + " ;\n");
320 return FAKE_CONSTR;
321 }
322
323 public IConstr addAtLeast(IVecInt literals, IVec<BigInteger> coeffs,
324 BigInteger degree) throws ContradictionException {
325 StringBuffer out = getOut();
326 assert literals.size() == coeffs.size();
327 this.nbOfConstraints++;
328 for (int i = 0; i < literals.size(); i++) {
329 out.append(coeffs.get(i) + " " + this.mapping.get(literals.get(i))
330 + " + ");
331 }
332 out.append(">= " + degree + " ;\n");
333 return FAKE_CONSTR;
334 }
335
336 public IConstr addExactly(IVecInt literals, IVecInt coeffs, int weight)
337 throws ContradictionException {
338 StringBuffer out = getOut();
339 assert literals.size() == coeffs.size();
340 this.nbOfConstraints++;
341 for (int i = 0; i < literals.size(); i++) {
342 out.append(coeffs.get(i) + " " + this.mapping.get(literals.get(i))
343 + " + ");
344 }
345 out.append("= " + weight + " ;\n");
346 return FAKE_CONSTR;
347 }
348
349 public IConstr addExactly(IVecInt literals, IVec<BigInteger> coeffs,
350 BigInteger weight) throws ContradictionException {
351 StringBuffer out = getOut();
352 assert literals.size() == coeffs.size();
353 this.nbOfConstraints++;
354 for (int i = 0; i < literals.size(); i++) {
355 out.append(coeffs.get(i) + " " + this.mapping.get(literals.get(i))
356 + " + ");
357 }
358 out.append("= " + weight + " ;\n");
359 return FAKE_CONSTR;
360 }
361
362 }