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