View Javadoc

1   /*******************************************************************************
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004, 2012 Artois University and CNRS
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   * Contributors:
28   *   CRIL - initial API and implementation
29   *******************************************************************************/
30  package org.sat4j.pb.reader;
31  
32  import java.io.IOException;
33  import java.math.BigInteger;
34  import java.util.Iterator;
35  
36  import org.sat4j.pb.IPBSolver;
37  import org.sat4j.reader.ParseFormatException;
38  import org.sat4j.specs.ContradictionException;
39  import org.sat4j.specs.IProblem;
40  
41  /**
42   * @since 2.2
43   */
44  public class OPBReader2010 extends OPBReader2007 {
45  
46      public static final BigInteger SAT4J_MAX_BIG_INTEGER = new BigInteger(
47              "100000000000000000000000000000000000000000");
48  
49      private boolean isWbo = false;
50  
51      private BigInteger softLimit = SAT4J_MAX_BIG_INTEGER;
52  
53      /**
54  	 * 
55  	 */
56      private static final long serialVersionUID = 1L;
57  
58      public OPBReader2010(IPBSolver solver) {
59          super(solver);
60      }
61  
62      /**
63       * read the first comment line to get the number of variables and the number
64       * of constraints in the file calls metaData with the data that was read
65       * 
66       * @throws IOException
67       * @throws ParseFormatException
68       */
69      @Override
70      protected void readMetaData() throws IOException, ParseFormatException {
71          char c;
72          String s;
73  
74          // get the number of variables and constraints
75          c = get();
76          if (c != '*') {
77              throw new ParseFormatException(
78                      "First line of input file should be a comment");
79          }
80          s = readWord();
81          if (eof() || !"#variable=".equals(s)) {
82              throw new ParseFormatException(
83                      "First line should contain #variable= as first keyword");
84          }
85  
86          this.nbVars = Integer.parseInt(readWord());
87          this.nbNewSymbols = this.nbVars + 1;
88  
89          s = readWord();
90          if (eof() || !"#constraint=".equals(s)) {
91              throw new ParseFormatException(
92                      "First line should contain #constraint= as second keyword");
93          }
94  
95          this.nbConstr = Integer.parseInt(readWord());
96          this.charAvailable = false;
97          if (!eol()) {
98              String rest = this.in.readLine();
99  
100             if (rest != null && rest.contains("#soft")) {
101                 this.isWbo = true;
102                 this.hasObjFunc = true;
103             }
104             if (rest != null && rest.indexOf("#product=") != -1) {
105                 String[] splitted = rest.trim().split(" ");
106                 if (splitted[0].equals("#product=")) {
107                     Integer.parseInt(splitted[1]);
108                 }
109 
110                 // if (splitted[2].equals("sizeproduct="))
111                 // readWord();
112 
113             }
114         }
115         // callback to transmit the data
116         metaData(this.nbVars, this.nbConstr);
117     }
118 
119     @Override
120     protected void readObjective() throws IOException, ParseFormatException {
121         if (this.isWbo) {
122             readSoftLine();
123         } else {
124             super.readObjective();
125         }
126     }
127 
128     private void readSoftLine() throws IOException, ParseFormatException {
129         String s = readWord();
130         if (s == null || !"soft:".equals(s)) {
131             throw new ParseFormatException("Did not find expected soft: line");
132         }
133         s = readWord().trim();
134         if (s != null && !";".equals(s)) {
135             this.softLimit = new BigInteger(s);
136         }
137         skipSpaces();
138         if (get() != ';') {
139             throw new ParseFormatException(
140                     "soft: line should end with a semicolon");
141         }
142     }
143 
144     private boolean softConstraint;
145 
146     @Override
147     protected void beginConstraint() {
148         super.beginConstraint();
149         this.softConstraint = false;
150         try {
151             if (this.isWbo) {
152                 skipSpaces();
153                 char c = get();
154                 putback(c);
155                 if (c == '[') {
156                     this.softConstraint = true;
157                     String s = readWord();
158                     if (!s.endsWith("]")) {
159                         throw new ParseFormatException(
160                                 "Expecting end of weight ");
161                     }
162                     BigInteger coeff = new BigInteger(s.substring(1,
163                             s.length() - 1));
164                     getCoeffs().push(coeff);
165                     int varId = this.nbNewSymbols++;
166                     getVars().push(varId);
167                 }
168 
169             }
170         } catch (Exception e) {
171             throw new RuntimeException(e);
172         }
173     }
174 
175     @Override
176     protected void endConstraint() throws ContradictionException {
177         if (this.softConstraint) {
178             int varId = getVars().last();
179             BigInteger constrWeight = this.d;
180             for (Iterator<BigInteger> it = this.coeffs.iterator(); it.hasNext();) {
181                 constrWeight = constrWeight.add(it.next().abs());
182             }
183             if ("<=".equals(this.operator)) {
184                 constrWeight = constrWeight.negate();
185             }
186             this.coeffs.push(constrWeight);
187             this.lits.push(varId);
188         }
189         super.endConstraint();
190     }
191 
192     @Override
193     public IProblem parseInstance(final java.io.Reader input)
194             throws ParseFormatException, ContradictionException {
195         super.parseInstance(input);
196         if (this.isWbo && this.softLimit != SAT4J_MAX_BIG_INTEGER) {
197             this.solver.addPseudoBoolean(getVars(), getCoeffs(), false,
198                     this.softLimit.subtract(BigInteger.ONE));
199         }
200         return this.solver;
201     }
202 }