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 pseudo boolean algorithms described in:
20 * A fast pseudo-Boolean constraint solver Chai, D.; Kuehlmann, A.
21 * Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
22 * Volume 24, Issue 3, March 2005 Page(s): 305 - 317
23 *
24 * and
25 * Heidi E. Dixon, 2004. Automating Pseudo-Boolean Inference within a DPLL
26 * Framework. Ph.D. Dissertation, University of Oregon.
27 *******************************************************************************/
28 /*=============================================================================
29 * parser for CSP instances represented in XML format
30 *
31 * Copyright (c) 2006 Olivier ROUSSEL (olivier.roussel <at> cril.univ-artois.fr)
32 *
33 * Permission is hereby granted, free of charge, to any person obtaining a copy
34 * of this software and associated documentation files (the "Software"), to deal
35 * in the Software without restriction, including without limitation the rights
36 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
37 * copies of the Software, and to permit persons to whom the Software is
38 * furnished to do so, subject to the following conditions:
39 *
40 * The above copyright notice and this permission notice shall be included in
41 * all copies or substantial portions of the Software.
42 *
43 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
44 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
45 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
46 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
47 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
48 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
49 * THE SOFTWARE.
50 *=============================================================================
51 */
52 package org.sat4j.pb.reader;
53
54 import java.io.IOException;
55 import java.math.BigInteger;
56 import java.util.HashMap;
57 import java.util.Iterator;
58 import java.util.Map;
59
60 import org.sat4j.core.Vec;
61 import org.sat4j.core.VecInt;
62 import org.sat4j.pb.IPBSolver;
63 import org.sat4j.reader.ParseFormatException;
64 import org.sat4j.specs.ContradictionException;
65 import org.sat4j.specs.IVec;
66 import org.sat4j.specs.IVecInt;
67
68 /**
69 * Reader complying with the PB07 input format.
70 *
71 * Non-linear to linear translation adapted from the PB07 readers provided
72 * by Olivier Roussel and Vasco Manquinho
73 * (was available in C++, not in Java)
74 *
75 * http://www.cril.univ-artois.fr/PB07/parser/SimpleParser.java
76 * http://www.cril.univ-artois.fr/PB07/parser/SimpleParser.cc
77 *
78 * @author parrain
79 * @author daniel
80 *
81 */
82 public class OPBReader2007 extends OPBReader2006 {
83
84 /**
85 *
86 */
87 private static final long serialVersionUID = 1L;
88
89 private int nbProducts;
90
91 // MetaData: #products and productSize in file.
92
93 /**
94 * @param solver
95 */
96 public OPBReader2007(IPBSolver solver) {
97 super(solver);
98 }
99
100 @Override
101 protected boolean isGoodFirstCharacter(char c) {
102 return Character.isLetter(c) || c == '_' || c == '~';
103 }
104
105 @Override
106 protected void checkId(StringBuffer s) throws ParseFormatException {
107 // Small check on the coefficient ID to make sure everything is ok
108 int cpt = 1;
109 if (s.charAt(0) == '~')
110 cpt = 2;
111 int varID = Integer.parseInt(s.substring(cpt));
112 if (varID > nbVars) {
113 throw new ParseFormatException(
114 "Variable identifier larger than #variables in metadata.");
115 }
116 }
117
118 /**
119 * contains the number of new symbols generated to linearize products
120 */
121 private int nbNewSymbols;
122
123 @Override
124 protected void readTerm(StringBuffer coeff, StringBuffer var)
125 throws IOException, ParseFormatException, ContradictionException {
126 readInteger(coeff);
127
128 skipSpaces();
129
130 var.setLength(0);
131 IVec<String> tmpLit = new Vec<String>();
132 StringBuffer tmpVar = new StringBuffer();
133 while (readIdentifier(tmpVar)) {
134 tmpLit = tmpLit.push(tmpVar.toString());
135 skipSpaces();
136 }
137 if (tmpLit.size() == 0)
138 throw new ParseFormatException("identifier expected");
139 if (tmpLit.size() == 1) {
140 // it is a "normal" term
141 var.append(tmpLit.last());
142 tmpLit.pop();
143 } else {
144 // it is a product term
145 var.append(linearizeProduct(tmpLit));
146 }
147 }
148
149 /**
150 * callback called when we read a term of a constraint
151 *
152 * @param var
153 * the identifier of the variable
154 * @param lits
155 * a set of literals in DIMACS format in which var once
156 * translated will be added.
157 */
158 protected void literalInAProduct(String var, IVecInt lits) {
159 int beginning = ((var.charAt(0) == '~') ? 2 : 1);
160 int id = Integer.parseInt(var.substring(beginning));
161 int lid = ((var.charAt(0) == '~') ? -1 : 1) * id;
162 lits.push(lid);
163 }
164
165 /**
166 * callback called when we read a term of a constraint
167 *
168 * @param var
169 * the identifier of the variable
170 * @param lits
171 * a set of literals in DIMACS format in which var once
172 * translated will be added.
173 */
174 protected void negateLiteralInAProduct(String var, IVecInt lits) {
175 int beginning = ((var.charAt(0) == '~') ? 2 : 1);
176 int id = Integer.parseInt(var.substring(beginning));
177 int lid = ((var.charAt(0) == '~') ? 1 : -1) * id;
178 lits.push(lid);
179 }
180
181 /**
182 * read the first comment line to get the number of variables and the number
183 * of constraints in the file calls metaData with the data that was read
184 *
185 * @throws IOException
186 * @throws ParseException
187 */
188 @Override
189 protected void readMetaData() throws IOException, ParseFormatException {
190 char c;
191 String s;
192
193 // get the number of variables and constraints
194 c = get();
195 if (c != '*')
196 throw new ParseFormatException(
197 "First line of input file should be a comment");
198 s = readWord();
199 if (eof() || !"#variable=".equals(s))
200 throw new ParseFormatException(
201 "First line should contain #variable= as first keyword");
202
203 nbVars = Integer.parseInt(readWord());
204 nbNewSymbols = nbVars + 1;
205
206 s = readWord();
207 if (eof() || !"#constraint=".equals(s))
208 throw new ParseFormatException(
209 "First line should contain #constraint= as second keyword");
210
211 nbConstr = Integer.parseInt(readWord());
212 charAvailable = false;
213 if (!eol()) {
214 String rest = in.readLine();
215
216 if (rest!=null&&rest.indexOf("#product=") != -1) {
217 String[] splitted = rest.trim().split(" ");
218 if (splitted[0].equals("#product=")) {
219 nbProducts = Integer.parseInt(splitted[1]);
220 nbVars += nbProducts;
221 nbConstr += 2 * nbProducts;
222 }
223
224 // if (splitted[2].equals("sizeproduct="))
225 // readWord();
226
227 }
228 }
229 // callback to transmit the data
230 metaData(nbVars, nbConstr);
231 }
232
233 @Override
234 protected int translateVarToId(String var) {
235 int beginning = ((var.charAt(0) == '~') ? 2 : 1);
236 int id = Integer.parseInt(var.substring(beginning));
237 return ((var.charAt(0) == '~') ? -1 : 1) * id;
238 }
239
240 private String linearizeProduct(IVec<String> tmpLit)
241 throws ContradictionException {
242 tmpLit.sort(String.CASE_INSENSITIVE_ORDER);
243 String newVar = getProductVariable(tmpLit);
244 if (newVar == null) {
245 // generate a new symbol
246 newVar = "X" + String.valueOf(nbNewSymbols++);
247 // linearization proposed by O. Roussel (PB07)
248 // generate the clause
249 // product => newSymbol (this is a clause)
250 // not x1 or not x2 ... or not xn or newSymbol
251 productStore.put(newVar, tmpLit);
252 IVecInt newLits = new VecInt();
253 for (Iterator<String> iterator = tmpLit.iterator();iterator.hasNext();)
254 negateLiteralInAProduct(iterator.next(), newLits);
255 literalInAProduct(newVar, newLits);
256 solver.addClause(newLits);
257 // generate the PB-constraint
258 // newSymbol => product translated as
259 // x1+x2+x3...+xn-n*newSymbol>=0
260 newLits.clear();
261 IVec<BigInteger> newCoefs = new Vec<BigInteger>();
262 for (Iterator<String> iterator = tmpLit.iterator();iterator.hasNext();) {
263 literalInAProduct(iterator.next(), newLits);
264 newCoefs.push(BigInteger.ONE);
265 }
266 literalInAProduct(newVar, newLits);
267 newCoefs.push(new BigInteger(String.valueOf(-tmpLit.size())));
268 solver.addPseudoBoolean(newLits, newCoefs, true, BigInteger.ZERO);
269 nbConstraintsRead += 2;
270 }
271 return newVar;
272 }
273
274 private Map<String, IVec<String>> productStore = new HashMap<String, IVec<String>>();
275
276 private String getProductVariable(IVec<String> lits) {
277 for (Map.Entry<String, IVec<String>> c : productStore.entrySet())
278 if (c.getValue().equals(lits))
279 return c.getKey();
280 return null;
281 }
282
283 }