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  package org.sat4j.maxsat.reader;
20  
21  import java.io.IOException;
22  import java.math.BigInteger;
23  
24  import org.sat4j.maxsat.WeightedMaxSatDecorator;
25  import org.sat4j.reader.DimacsReader;
26  import org.sat4j.reader.ParseFormatException;
27  import org.sat4j.specs.ContradictionException;
28  
29  /**
30   * Simple reader for the weighted maxsat problem.
31   * 
32   * @author daniel
33   *
34   */
35  public class WDimacsReader extends DimacsReader {
36  
37  	protected BigInteger weight;
38  	protected BigInteger top;
39  	
40      @Override
41  	protected void flushConstraint() throws ContradictionException {
42      	decorator.addSoftClause(weight, literals);
43  	}
44  
45  	@Override
46  	protected boolean handleLine() throws ContradictionException, IOException, ParseFormatException {
47  		weight = scanner.nextBigInteger();
48  		return super.handleLine();
49  	}
50  
51  	/**
52       * 
53       */
54      private static final long serialVersionUID = 1L;
55  
56      private final WeightedMaxSatDecorator decorator;
57      
58      public WDimacsReader(WeightedMaxSatDecorator solver) {
59          super(solver,"wcnf");
60          decorator = solver;
61      }
62  
63      public WDimacsReader(WeightedMaxSatDecorator solver, String format) {
64          super(solver, format);
65          decorator = solver;
66      }
67  
68      @Override
69      protected void readProblemLine() throws IOException,
70              ParseFormatException {
71      	String line = scanner.nextLine().trim();
72  
73  		if (line == null) {
74  			throw new ParseFormatException(
75  					"premature end of file: <p cnf ...> expected");
76  		}
77  		String[] tokens = line.split("\\s+");
78  		if (tokens.length < 4 || !"p".equals(tokens[0])
79  				|| !formatString.equals(tokens[1])) {
80  			throw new ParseFormatException("problem line expected (p cnf ...)");
81  		}
82  
83  		int vars;
84  
85  		// reads the max var id
86  		vars = Integer.parseInt(tokens[2]);
87  		assert vars > 0;
88  		solver.newVar(vars);
89  		// reads the number of clauses
90  		expectedNbOfConstr = Integer.parseInt(tokens[3]);
91  		assert expectedNbOfConstr > 0;
92  		solver.setExpectedNumberOfClauses(expectedNbOfConstr);
93  		
94          if ("wcnf".equals(formatString)) {
95              // assume we are in weighted MAXSAT mode
96              if (tokens.length==5) {
97                  top = new BigInteger(tokens[4]);
98              } else {
99                  top = WeightedMaxSatDecorator.SAT4J_MAX_BIG_INTEGER;
100             }             
101             decorator.setTopWeight(top);
102         }
103     }
104 
105     
106 }