View Javadoc

1   /*******************************************************************************
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le
3    *
4    * All rights reserved. This program and the accompanying materials
5    * are made available under the terms of the Eclipse Public License v1.0
6    * which accompanies this distribution, and is available at
7    * http://www.eclipse.org/legal/epl-v10.html
8    *
9    * Alternatively, the contents of this file may be used under the terms of
10   * either the GNU Lesser General Public License Version 2.1 or later (the
11   * "LGPL"), in which case the provisions of the LGPL are applicable instead
12   * of those above. If you wish to allow use of your version of this file only
13   * under the terms of the LGPL, and not to allow others to use your version of
14   * this file under the terms of the EPL, indicate your decision by deleting
15   * the provisions above and replace them with the notice and other provisions
16   * required by the LGPL. If you do not delete the provisions above, a recipient
17   * may use your version of this file under the terms of the EPL or the LGPL.
18   *******************************************************************************/
19  package org.sat4j.reader;
20  
21  import java.io.IOException;
22  import java.io.InputStream;
23  import java.io.InputStreamReader;
24  import java.io.LineNumberReader;
25  import java.io.PrintWriter;
26  import java.util.HashMap;
27  import java.util.LinkedHashMap;
28  import java.util.Map;
29  import java.util.Scanner;
30  
31  import org.sat4j.core.Vec;
32  import org.sat4j.csp.Clausifiable;
33  import org.sat4j.csp.Constant;
34  import org.sat4j.csp.Domain;
35  import org.sat4j.csp.EnumeratedDomain;
36  import org.sat4j.csp.Evaluable;
37  import org.sat4j.csp.Predicate;
38  import org.sat4j.csp.RangeDomain;
39  import org.sat4j.csp.Var;
40  import org.sat4j.csp.constraints.AllDiff;
41  import org.sat4j.csp.constraints.AllDiffCard;
42  import org.sat4j.csp.constraints.Nogoods;
43  import org.sat4j.csp.constraints.Relation;
44  import org.sat4j.csp.constraints.WalshSupports;
45  import org.sat4j.specs.ContradictionException;
46  import org.sat4j.specs.IProblem;
47  import org.sat4j.specs.ISolver;
48  import org.sat4j.specs.IVec;
49  
50  /**
51   * This class is a CSP to SAT translator that is able to read a CSP problem
52   * using the First CSP solver competition input format and that translates it
53   * into clausal and cardinality (equality) constraints.
54   * 
55   * That code has not been tested very thoroughly yet and was written very
56   * quickly to meet the competition deadline :=)) There is plenty of room for
57   * improvement.
58   * 
59   * @author leberre
60   * 
61   */
62  public class CSPReader extends Reader implements org.sat4j.csp.xml.ICSPCallback {
63  
64  	private final ISolver solver;
65  
66  	protected Relation[] relations;
67  
68  	private int valueindex;
69  
70  	private int relindex;
71  
72  	private int[] currentdomain;
73  
74  	private Domain rangedomain;
75  
76  	private String currentdomainid;
77  
78  	private int currentdomainsize;
79  
80  	private final Map<String, Domain> domainmapping = new HashMap<String, Domain>();
81  
82  	private final Map<String, Var> varmapping = new LinkedHashMap<String, Var>();
83  
84  	private final Map<String, Integer> relmapping = new HashMap<String, Integer>();
85  
86  	private final Map<String, Clausifiable> predmapping = new HashMap<String, Clausifiable>();
87  
88  	private int nbvarstocreate;
89  
90  	private int tupleindex;
91  
92  	private Clausifiable currentclausifiable;
93  
94  	private Predicate currentpredicate;
95  
96  	private final IVec<Evaluable> variables = new Vec<Evaluable>();
97  
98  	private final IVec<Var> scope = new Vec<Var>();
99  
100 	private int nbvars;
101 
102 	private int nbconstraints;
103 
104 	private int currentconstraint;
105 
106 	public CSPReader(ISolver solver, boolean allDiffCard) {
107 		this.solver = solver;
108 		Clausifiable allDiff = allDiffCard ? new AllDiffCard() : new AllDiff();
109 		predmapping.put("global:allDifferent", allDiff); // XCSP 2.0
110 															// compatibility
111 		predmapping.put("global:alldifferent", allDiff);
112 		if (solver.isVerbose()) {
113 			System.out.println("c " + allDiff);
114 		}
115 	}
116 
117 	@Override
118 	public final IProblem parseInstance(final java.io.Reader in)
119 			throws ParseFormatException, ContradictionException, IOException {
120 		return parseInstance(new LineNumberReader(in));
121 
122 	}
123 
124 	private IProblem parseInstance(LineNumberReader in)
125 			throws ParseFormatException {
126 		solver.reset();
127 		try {
128 			readProblem(in);
129 			return solver;
130 		} catch (NumberFormatException e) {
131 			throw new ParseFormatException("integer value expected on line "
132 					+ in.getLineNumber(), e);
133 		}
134 	}
135 
136 	@Override
137 	public void decode(int[] model, PrintWriter out) {
138 		// verifier que les variables sont bien dans le bon ordre !!!!
139 		for (Var v : varmapping.values()) {
140 			out.print(v.findValue(model));
141 			out.print(" ");
142 		}
143 	}
144 
145 	@Override
146 	public String decode(int[] model) {
147 		StringBuilder stb = new StringBuilder();
148 		// verifier que les variables sont bien dans le bon ordre !!!!
149 		for (Var v : varmapping.values()) {
150 			stb.append(v.findValue(model));
151 			stb.append(" ");
152 		}
153 		return stb.toString();
154 	}
155 
156 	private void readProblem(LineNumberReader in) {
157 		Scanner input = new Scanner(in);
158 		// discard problem name
159 		beginInstance(input.nextLine());
160 
161 		// read number of domain
162 		int nbdomain = input.nextInt();
163 		beginDomainsSection(nbdomain);
164 
165 		for (int i = 0; i < nbdomain; i++) {
166 			// read domain number
167 			int dnum = input.nextInt();
168 			assert dnum == i;
169 			// read domain
170 			int[] domain = readArrayOfInt(input);
171 			beginDomain("" + dnum, domain.length);
172 			for (int j = 0; j < domain.length; j++) {
173 				addDomainValue(domain[j]);
174 			}
175 			endDomain();
176 		}
177 		endDomainsSection();
178 		int nbvar = input.nextInt();
179 		beginVariablesSection(nbvar);
180 		for (int i = 0; i < nbvar; i++) {
181 			// read var number
182 			int varnum = input.nextInt();
183 			assert varnum == i;
184 			// read var domain
185 			int vardom = input.nextInt();
186 			addVariable("" + varnum, "" + vardom);
187 		}
188 		endVariablesSection();
189 
190 		// relation definition
191 		// read number of relations
192 		int nbrel = input.nextInt();
193 		beginRelationsSection(nbrel);
194 		for (int i = 0; i < nbrel; i++) {
195 
196 			// read relation number
197 			int relnum = input.nextInt();
198 			assert relnum == i;
199 
200 			boolean forbidden = input.nextInt() == 1 ? false : true;
201 			int[] rdomains = readArrayOfInt(input);
202 
203 			int nbtuples = input.nextInt();
204 
205 			beginRelation("" + relnum, rdomains.length, nbtuples, !forbidden);
206 
207 			for (int j = 0; j < nbtuples; j++) {
208 				int[] tuple = readArrayOfInt(input, relations[relnum].arity());
209 				// do something with tuple
210 				addRelationTuple(tuple);
211 			}
212 
213 			endRelation();
214 		}
215 		endRelationsSection();
216 		int nbconstr = input.nextInt();
217 		beginConstraintsSection(nbconstr);
218 		// constraint definition
219 		for (int i = 0; i < nbconstr; i++) {
220 			int[] theVariables = readArrayOfInt(input);
221 			beginConstraint("" + i, theVariables.length);
222 			int relnum = input.nextInt();
223 			// manage constraint
224 			constraintReference("" + relnum);
225 			for (int v : theVariables) {
226 				addEffectiveParameter("" + v);
227 			}
228 			endConstraint();
229 		}
230 		endConstraintsSection();
231 		endInstance();
232 	}
233 
234 	protected void manageAllowedTuples(int relnum, int arity, int nbtuples) {
235 		relations[relnum] = new WalshSupports(arity, nbtuples);
236 	}
237 
238 	private int[] readArrayOfInt(Scanner input) {
239 		int size = input.nextInt();
240 		return readArrayOfInt(input, size);
241 	}
242 
243 	private int[] readArrayOfInt(Scanner input, int size) {
244 		int[] tab = new int[size];
245 		for (int i = 0; i < size; i++)
246 			tab[i] = input.nextInt();
247 		return tab;
248 	}
249 
250 	public void beginInstance(String arg0) {
251 		System.out.println("c reading problem named " + arg0);
252 	}
253 
254 	public void beginDomainsSection(int nbdomain) {
255 		System.out.print("c reading domains");
256 	}
257 
258 	public void beginDomain(String id, int size) {
259 		currentdomainsize = size;
260 		currentdomain = null;
261 		valueindex = -1;
262 		currentdomainid = id;
263 		rangedomain = null;
264 	}
265 
266 	public void addDomainValue(int arg0) {
267 		if (currentdomain == null) {
268 			currentdomain = new int[currentdomainsize];
269 		}
270 		if (rangedomain != null) {
271 			for (int i = 0; i < rangedomain.size(); i++)
272 				currentdomain[++valueindex] = rangedomain.get(i);
273 			rangedomain = null;
274 		}
275 		currentdomain[++valueindex] = arg0;
276 	}
277 
278 	public void addDomainValue(int begin, int end) {
279 		if (currentdomainsize == end - begin + 1) {
280 			rangedomain = new RangeDomain(begin, end);
281 		} else {
282 			if (currentdomain == null) {
283 				currentdomain = new int[currentdomainsize];
284 			}
285 			for (int v = begin; v <= end; v++) {
286 				currentdomain[++valueindex] = v;
287 			}
288 		}
289 	}
290 
291 	public void endDomain() {
292 		assert rangedomain != null || valueindex == currentdomain.length - 1;
293 		if (rangedomain == null) {
294 			domainmapping.put(currentdomainid, new EnumeratedDomain(
295 					currentdomain));
296 		} else {
297 			domainmapping.put(currentdomainid, rangedomain);
298 		}
299 	}
300 
301 	public void endDomainsSection() {
302 		System.out.println(" done.");
303 	}
304 
305 	public void beginVariablesSection(int expectedNumberOfVariables) {
306 		System.out.print("c reading variables");
307 		nbvarstocreate = 0;
308 		this.nbvars = expectedNumberOfVariables;
309 	}
310 
311 	public void addVariable(String idvar, String iddomain) {
312 		Domain vardom = domainmapping.get(iddomain);
313 		varmapping.put(idvar, new Var(idvar, vardom, nbvarstocreate));
314 		nbvarstocreate += vardom.size();
315 		if (isVerbose()) {
316 			System.out.print("\rc reading variables " + varmapping.size() + "/"
317 					+ nbvars);
318 		}
319 
320 	}
321 
322 	public void endVariablesSection() {
323 		if (isVerbose()) {
324 			System.out.println("\rc reading variables (" + nbvars + ") done.");
325 		} else {
326 			System.out.println(" done.");
327 		}
328 		solver.newVar(nbvarstocreate);
329 		try {
330 			for (Evaluable v : varmapping.values()) {
331 				v.toClause(solver);
332 			}
333 		} catch (ContradictionException ce) {
334 			assert false;
335 		}
336 
337 	}
338 
339 	public void beginRelationsSection(int nbrel) {
340 		System.out.print("c reading relations");
341 		relations = new Relation[nbrel];
342 		relindex = -1;
343 	}
344 
345 	public void beginRelation(String name, int arity, int nbTuples,
346 			boolean isSupport) {
347 		relmapping.put(name, ++relindex);
348 		if (isVerbose()) {
349 			System.out.print("\rc reading relations " + relindex + "/"
350 					+ relations.length);
351 		}
352 		if (isSupport) {
353 			manageAllowedTuples(relindex, arity, nbTuples);
354 		} else {
355 			relations[relindex] = new Nogoods(arity, nbTuples);
356 		}
357 		tupleindex = -1;
358 	}
359 
360 	public void addRelationTuple(int[] tuple) {
361 		relations[relindex].addTuple(++tupleindex, tuple);
362 	}
363 
364 	public void endRelation() {
365 	}
366 
367 	public void endRelationsSection() {
368 		if (isVerbose()) {
369 			System.out.println("\rc reading relations (" + relations.length
370 					+ ") done.");
371 		} else {
372 			System.out.println(" done.");
373 		}
374 	}
375 
376 	public void beginPredicatesSection(int arg0) {
377 		System.out.print("c reading predicates ");
378 	}
379 
380 	public void beginPredicate(String name) {
381 		currentpredicate = new Predicate();
382 		predmapping.put(name, currentpredicate);
383 		if (isVerbose()) {
384 			System.out.print("\rc reading predicate " + predmapping.size());
385 		}
386 	}
387 
388 	public void addFormalParameter(String name, String type) {
389 		currentpredicate.addVariable(name);
390 	}
391 
392 	public void predicateExpression(String expr) {
393 		currentpredicate.setExpression(expr);
394 	}
395 
396 	public void endPredicate() {
397 		// TODO Auto-generated method stub
398 	}
399 
400 	public void endPredicatesSection() {
401 		if (isVerbose()) {
402 			System.out.println("\rc reading relations (" + predmapping.size()
403 					+ ") done.");
404 		} else {
405 			System.out.println(" done.");
406 		}
407 	}
408 
409 	public void beginConstraintsSection(int arg0) {
410 		System.out.println("c reading constraints");
411 		nbconstraints = arg0;
412 		currentconstraint = 0;
413 	}
414 
415 	public void beginConstraint(String name, int arity) {
416 		variables.clear();
417 		variables.ensure(arity);
418 		scope.clear();
419 		scope.ensure(arity);
420 		if (isVerbose()) {
421 			System.out.print("\rc grounding constraint " + name + "("
422 					+ (++currentconstraint * 100 / nbconstraints) + "%)");
423 		}
424 	}
425 
426 	public void constraintReference(String ref) {
427 		Integer id = relmapping.get(ref);
428 		if (id == null) {
429 			currentclausifiable = predmapping.get(ref);
430 		} else {
431 			currentclausifiable = relations[id];
432 		}
433 		if (currentclausifiable == null) {
434 			throw new IllegalArgumentException("Reference not supported:  "
435 					+ ref);
436 		}
437 	}
438 
439 	public void addVariableToConstraint(String arg0) {
440 		scope.push(varmapping.get(arg0));
441 	}
442 
443 	public void addEffectiveParameter(String arg0) {
444 		variables.push(varmapping.get(arg0));
445 	}
446 
447 	public void addEffectiveParameter(int arg0) {
448 		variables.push(new Constant(arg0));
449 	}
450 
451 	public void beginParameterList() {
452 		throw new UnsupportedOperationException(
453 				"I do not handle parameter list yet!");
454 
455 	}
456 
457 	public void addIntegerItem(int arg0) {
458 		// TODO Auto-generated method stub
459 
460 	}
461 
462 	public void addVariableItem(String arg0) {
463 		// TODO Auto-generated method stub
464 
465 	}
466 
467 	public void endParamaterList() {
468 		// TODO Auto-generated method stub
469 
470 	}
471 
472 	public void addConstantParameter(String arg0, int arg1) {
473 		throw new UnsupportedOperationException(
474 				"I do not handle constant parameter yet!");
475 	}
476 
477 	public void constraintExpression(String arg0) {
478 		throw new UnsupportedOperationException(
479 				"I do not handle constraint expression yet!");
480 	}
481 
482 	public void endConstraint() {
483 		try {
484 			currentclausifiable.toClause(solver, scope, variables);
485 		} catch (ContradictionException e) {
486 			System.err.println("c INSTANCE TRIVIALLY UNSAT");
487 		}
488 	}
489 
490 	public void endConstraintsSection() {
491 		if (isVerbose()) {
492 			System.out.println("\rc reading constraints done.");
493 		} else {
494 			System.out.println("c done with constraints.");
495 		}
496 	}
497 
498 	public void endInstance() {
499 		// TODO Auto-generated method stub
500 	}
501 
502 	IProblem getProblem() {
503 		return solver;
504 	}
505 
506 	@Override
507 	public IProblem parseInstance(final InputStream in)
508 			throws ParseFormatException, ContradictionException, IOException {
509 		return parseInstance(new InputStreamReader(in));
510 	}
511 }