View Javadoc

1   /*
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3    * 
4    * Based on the original minisat specification from:
5    * 
6    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7    * Sixth International Conference on Theory and Applications of Satisfiability
8    * Testing, LNCS 2919, pp 502-518, 2003.
9    * 
10   * This library is free software; you can redistribute it and/or modify it under
11   * the terms of the GNU Lesser General Public License as published by the Free
12   * Software Foundation; either version 2.1 of the License, or (at your option)
13   * any later version.
14   * 
15   * This library is distributed in the hope that it will be useful, but WITHOUT
16   * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17   * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18   * details.
19   * 
20   * You should have received a copy of the GNU Lesser General Public License
21   * along with this library; if not, write to the Free Software Foundation, Inc.,
22   * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
23   * 
24   */
25  
26  package org.sat4j.reader;
27  
28  import java.io.IOException;
29  import java.io.LineNumberReader;
30  import java.io.PrintWriter;
31  import java.io.Serializable;
32  import java.util.Scanner;
33  import java.util.StringTokenizer;
34  
35  import org.sat4j.core.VecInt;
36  import org.sat4j.opt.WeightedMaxSatDecorator;
37  import org.sat4j.specs.ContradictionException;
38  import org.sat4j.specs.IProblem;
39  import org.sat4j.specs.ISolver;
40  import org.sat4j.specs.IVecInt;
41  
42  /**
43   * Very simple Dimacs file parser. Allow solvers to read the constraints from a
44   * Dimacs formatted file. It should be used that way:
45   * 
46   * <pre>
47   * DimacsReader solver = new DimacsReader(SolverFactory.OneSolver());
48   * solver.readInstance(&quot;mybench.cnf&quot;);
49   * if (solver.isSatisfiable()) {
50   *     // SAT case
51   * } else {
52   *     // UNSAT case
53   * }
54   * </pre>
55   * 
56   * That parser is not used for efficiency reasons. It will be updated with Java
57   * 1.5 scanner feature.
58   * 
59   * @version 1.0
60   * @author dlb
61   * @author or
62   */
63  public class DimacsReader extends Reader implements Serializable {
64  
65      private static final long serialVersionUID = 1L;
66  
67      protected int expectedNbOfConstr; // as announced on the p cnf line
68  
69      protected final ISolver solver;
70  
71      private boolean checkConstrNb = true;
72  
73      private final String formatString;
74  
75      public DimacsReader(ISolver solver) {
76          this(solver, "cnf");
77      }
78  
79      public DimacsReader(ISolver solver, String format) {
80          this.solver = solver;
81          formatString = format;
82      }
83  
84      public void disableNumberOfConstraintCheck() {
85          checkConstrNb = false;
86      }
87  
88      /**
89       * Skip comments at the beginning of the input stream.
90       * 
91       * @param in
92       *            the input stream
93       * @throws IOException
94       *             if an IO problem occurs.
95       */
96      protected void skipComments(final LineNumberReader in) throws IOException {
97          int c;
98  
99          do {
100             in.mark(4);
101             c = in.read();
102             if (c == 'c') {
103                 in.readLine();
104             } else {
105                 in.reset();
106             }
107         } while (c == 'c');
108     }
109 
110     /**
111      * @param in
112      *            the input stream
113      * @throws IOException
114      *             iff an IO occurs
115      * @throws ParseFormatException
116      *             if the input stream does not comply with the DIMACS format.
117      */
118     protected void readProblemLine(LineNumberReader in) throws IOException,
119             ParseFormatException {
120 
121         String line = in.readLine();
122 
123         if (line == null) {
124             throw new ParseFormatException(
125                     "premature end of file: <p cnf ...> expected  on line "
126                             + in.getLineNumber());
127         }
128         StringTokenizer stk = new StringTokenizer(line);
129 
130         if (!(stk.hasMoreTokens() && stk.nextToken().equals("p")
131                 && stk.hasMoreTokens() && stk.nextToken().equals(formatString))) {
132             throw new ParseFormatException(
133                     "problem line expected (p cnf ...) on line "
134                             + in.getLineNumber());
135         }
136 
137         int vars;
138 
139         // reads the max var id
140         vars = Integer.parseInt(stk.nextToken());
141         assert vars > 0;
142         solver.newVar(vars);
143         // reads the number of clauses
144         expectedNbOfConstr = Integer.parseInt(stk.nextToken());
145         assert expectedNbOfConstr > 0;
146         solver.setExpectedNumberOfClauses(expectedNbOfConstr);
147         if ("wcnf".equals(formatString)) {
148             // assume we are in weighted MAXSAT mode
149             int top;
150             if (stk.hasMoreTokens()) {
151                 top = Integer.parseInt(stk.nextToken());
152             } else {
153                 top = Integer.MAX_VALUE;
154             }
155             ((WeightedMaxSatDecorator)solver).setTopWeight(top);
156         }
157     }
158 
159     /**
160      * @param in
161      *            the input stream
162      * @throws IOException
163      *             iff an IO problems occurs
164      * @throws ParseFormatException
165      *             if the input stream does not comply with the DIMACS format.
166      * @throws ContradictionException
167      *             si le probl?me est trivialement inconsistant.
168      */
169     protected void readConstrs(LineNumberReader in) throws IOException,
170             ParseFormatException, ContradictionException {
171         String line;
172 
173         int realNbOfConstr = 0;
174 
175         IVecInt literals = new VecInt();
176 
177         while (true) {
178             line = in.readLine();
179 
180             if (line == null) {
181                 // end of file
182                 if (literals.size() > 0) {
183                     // no 0 end the last clause
184                     solver.addClause(literals);
185                     realNbOfConstr++;
186                 }
187 
188                 break;
189             }
190 
191             if (line.startsWith("c ")) {
192                 // ignore comment line
193                 System.out.println("Found commmented line : " + line);
194                 continue;
195             }
196             if (line.startsWith("%") && expectedNbOfConstr == realNbOfConstr) {
197                 System.out
198                         .println("Ignoring the rest of the file (SATLIB format");
199                 break;
200             }
201             boolean added = handleConstr(line, literals);
202             if (added) {
203                 realNbOfConstr++;
204             }
205         }
206         if (checkConstrNb && expectedNbOfConstr != realNbOfConstr) {
207             throw new ParseFormatException("wrong nbclauses parameter. Found "
208                     + realNbOfConstr + ", " + expectedNbOfConstr + " expected");
209         }
210     }
211 
212     protected boolean handleConstr(String line, IVecInt literals)
213             throws ContradictionException {
214         int lit;
215         boolean added = false;
216         Scanner scan;
217         scan = new Scanner(line);
218         while (scan.hasNext()) {
219             lit = scan.nextInt();
220 
221             if (lit == 0) {
222                 if (literals.size() > 0) {
223                     solver.addClause(literals);
224                     literals.clear();
225                     added = true;
226                 }
227             } else {
228                 literals.push(lit);
229             }
230         }
231         return added;
232     }
233 
234     @Override
235     public final IProblem parseInstance(final java.io.Reader in)
236             throws ParseFormatException, ContradictionException, IOException {
237         return parseInstance(new LineNumberReader(in));
238 
239     }
240 
241     /**
242      * @param in
243      *            the input stream
244      * @throws ParseFormatException
245      *             if the input stream does not comply with the DIMACS format.
246      * @throws ContradictionException
247      *             si le probl?me est trivialement inconsitant
248      */
249     private IProblem parseInstance(LineNumberReader in)
250             throws ParseFormatException, ContradictionException {
251         solver.reset();
252         try {
253             skipComments(in);
254             readProblemLine(in);
255             readConstrs(in);
256             return solver;
257         } catch (IOException e) {
258             throw new ParseFormatException(e);
259         } catch (NumberFormatException e) {
260             throw new ParseFormatException("integer value expected on line "
261                     + in.getLineNumber(), e);
262         }
263     }
264 
265     @Override
266     public String decode(int[] model) {
267         StringBuffer stb = new StringBuffer();
268         for (int i = 0; i < model.length; i++) {
269             stb.append(model[i]);
270             stb.append(" ");
271         }
272         stb.append("0");
273         return stb.toString();
274     }
275 
276     @Override
277     public void decode(int[] model, PrintWriter out) {
278         for (int i = 0; i < model.length; i++) {
279             out.print(model[i]);
280             out.print(" ");
281         }
282         out.print("0");
283     }
284 
285     protected ISolver getSolver() {
286         return solver;
287     }
288 }