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