View Javadoc

1   /*******************************************************************************
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
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   * Based on the original MiniSat specification from:
20   * 
21   * An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
22   * Sixth International Conference on Theory and Applications of Satisfiability
23   * Testing, LNCS 2919, pp 502-518, 2003.
24   *
25   * See www.minisat.se for the original solver in C++.
26   * 
27   *******************************************************************************/
28  package org.sat4j.reader;
29  
30  import java.io.IOException;
31  import java.io.InputStream;
32  import java.io.PrintWriter;
33  import java.io.Serializable;
34  
35  import org.sat4j.core.VecInt;
36  import org.sat4j.specs.ContradictionException;
37  import org.sat4j.specs.IProblem;
38  import org.sat4j.specs.ISolver;
39  import org.sat4j.specs.IVecInt;
40  
41  /**
42   * Very simple Dimacs file parser. Allow solvers to read the constraints from a
43   * Dimacs formatted file. It should be used that way:
44   * 
45   * <pre>
46   * DimacsReader solver = new DimacsReader(SolverFactory.OneSolver());
47   * solver.readInstance(&quot;mybench.cnf&quot;);
48   * if (solver.isSatisfiable()) {
49   * 	// SAT case
50   * } else {
51   * 	// UNSAT case
52   * }
53   * </pre>
54   * 
55   * That parser is not used for efficiency reasons. It will be updated with Java
56   * 1.5 scanner feature.
57   * 
58   * @version 1.0
59   * @author dlb
60   * @author or
61   */
62  public class DimacsReader extends Reader implements Serializable {
63  
64  	private static final long serialVersionUID = 1L;
65  
66  	protected int expectedNbOfConstr; // as announced on the p cnf line
67  
68  	protected final ISolver solver;
69  
70  	private boolean checkConstrNb = true;
71  
72  	protected final String formatString;
73  
74  	/**
75  	 * @since 2.1
76  	 */
77  	protected EfficientScanner scanner;
78  
79  	public DimacsReader(ISolver solver) {
80  		this(solver, "cnf");
81  	}
82  
83  	public DimacsReader(ISolver solver, String format) {
84  		this.solver = solver;
85  		formatString = format;
86  	}
87  
88  	public void disableNumberOfConstraintCheck() {
89  		checkConstrNb = false;
90  	}
91  
92  	/**
93  	 * Skip comments at the beginning of the input stream.
94  	 * 
95  	 * @param in
96  	 *            the input stream
97  	 * @throws IOException
98  	 *             if an IO problem occurs.
99  	 * @since 2.1
100 	 */
101 	protected void skipComments() throws IOException {
102 		scanner.skipComments();
103 	}
104 
105 	/**
106 	 * @param in
107 	 *            the input stream
108 	 * @throws IOException
109 	 *             iff an IO occurs
110 	 * @throws ParseFormatException
111 	 *             if the input stream does not comply with the DIMACS format.
112 	 * @since 2.1
113 	 */
114 	protected void readProblemLine() throws IOException, ParseFormatException {
115 
116 		String line = scanner.nextLine().trim();
117 
118 		if (line == null) {
119 			throw new ParseFormatException(
120 					"premature end of file: <p cnf ...> expected");
121 		}
122 		String[] tokens = line.split("\\s+");
123 		if (tokens.length < 4 || !"p".equals(tokens[0])
124 				|| !formatString.equals(tokens[1])) {
125 			throw new ParseFormatException("problem line expected (p cnf ...)");
126 		}
127 
128 		int vars;
129 
130 		// reads the max var id
131 		vars = Integer.parseInt(tokens[2]);
132 		assert vars > 0;
133 		solver.newVar(vars);
134 		// reads the number of clauses
135 		expectedNbOfConstr = Integer.parseInt(tokens[3]);
136 		assert expectedNbOfConstr > 0;
137 		solver.setExpectedNumberOfClauses(expectedNbOfConstr);
138 	}
139 
140 	/**
141 	 * @since 2.1
142 	 */
143 	protected IVecInt literals = new VecInt();
144 
145 	/**
146 	 * @param in
147 	 *            the input stream
148 	 * @throws IOException
149 	 *             iff an IO problems occurs
150 	 * @throws ParseFormatException
151 	 *             if the input stream does not comply with the DIMACS format.
152 	 * @throws ContradictionException
153 	 *             si le probl?me est trivialement inconsistant.
154 	 * @since 2.1
155 	 */
156 	protected void readConstrs() throws IOException, ParseFormatException,
157 			ContradictionException {
158 		int realNbOfConstr = 0;
159 
160 		literals.clear();
161 		boolean needToContinue = true;
162 
163 		while (needToContinue) {
164 			boolean added = false;
165 			if (scanner.eof()) {
166 				// end of file
167 				if (literals.size() > 0) {
168 					// no 0 end the last clause
169 					flushConstraint();
170 					added = true;
171 				}
172 				needToContinue = false;
173 			} else {
174 				if (scanner.currentChar() == 'c') {
175 					// ignore comment line
176 					scanner.skipRestOfLine();
177 					continue;
178 				}
179 				if (scanner.currentChar() == '%'
180 						&& expectedNbOfConstr == realNbOfConstr) {
181 					if (solver.isVerbose()) {
182 						System.out
183 								.println("Ignoring the rest of the file (SATLIB format");
184 					}
185 					break;
186 				}
187 				added = handleLine();
188 			}
189 			if (added) {
190 				realNbOfConstr++;
191 			}
192 		}
193 		if (checkConstrNb && expectedNbOfConstr != realNbOfConstr) {
194 			throw new ParseFormatException("wrong nbclauses parameter. Found "
195 					+ realNbOfConstr + ", " + expectedNbOfConstr + " expected");
196 		}
197 	}
198 
199 	/**
200 	 * 
201 	 * @throws ContradictionException
202 	 * @since 2.1
203 	 */
204 	protected void flushConstraint() throws ContradictionException {
205 		solver.addClause(literals);
206 	}
207 
208 	/**
209 	 * @since 2.1
210 	 */
211 	protected boolean handleLine() throws ContradictionException, IOException,
212 			ParseFormatException {
213 		int lit;
214 		boolean added = false;
215 		while (!scanner.eof()) {
216 			lit = scanner.nextInt();
217 			if (lit == 0) {
218 				if (literals.size() > 0) {
219 					flushConstraint();
220 					literals.clear();
221 					added = true;
222 				}
223 				break;
224 			}
225 			literals.push(lit);
226 		}
227 		return added;
228 	}
229 
230 	@Override
231 	public IProblem parseInstance(InputStream in) throws ParseFormatException,
232 			ContradictionException, IOException {
233 		scanner = new EfficientScanner(in);
234 		return parseInstance();
235 	}
236 
237 	@Override
238 	public final IProblem parseInstance(final java.io.Reader in)
239 			throws ParseFormatException, ContradictionException, IOException {
240 		throw new UnsupportedOperationException();
241 
242 	}
243 
244 	/**
245 	 * @param in
246 	 *            the input stream
247 	 * @throws ParseFormatException
248 	 *             if the input stream does not comply with the DIMACS format.
249 	 * @throws ContradictionException
250 	 *             si le probl?me est trivialement inconsitant
251 	 */
252 	private IProblem parseInstance() throws ParseFormatException,
253 			ContradictionException {
254 		solver.reset();
255 		try {
256 			skipComments();
257 			readProblemLine();
258 			readConstrs();
259 			scanner.close();
260 			return solver;
261 		} catch (IOException e) {
262 			throw new ParseFormatException(e);
263 		} catch (NumberFormatException e) {
264 			throw new ParseFormatException("integer value expected ");
265 		}
266 	}
267 
268 	@Override
269 	public String decode(int[] model) {
270 		StringBuffer stb = new StringBuffer();
271 		for (int i = 0; i < model.length; i++) {
272 			stb.append(model[i]);
273 			stb.append(" ");
274 		}
275 		stb.append("0");
276 		return stb.toString();
277 	}
278 
279 	@Override
280 	public void decode(int[] model, PrintWriter out) {
281 		for (int i = 0; i < model.length; i++) {
282 			out.print(model[i]);
283 			out.print(" ");
284 		}
285 		out.print("0");
286 	}
287 
288 	protected ISolver getSolver() {
289 		return solver;
290 	}
291 }