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.tools;
29  
30  import java.io.ObjectInputStream;
31  import java.io.PrintStream;
32  import java.io.PrintWriter;
33  import java.util.Map;
34  
35  import org.sat4j.specs.ContradictionException;
36  import org.sat4j.specs.IConstr;
37  import org.sat4j.specs.ISolver;
38  import org.sat4j.specs.IVec;
39  import org.sat4j.specs.IVecInt;
40  import org.sat4j.specs.IteratorInt;
41  import org.sat4j.specs.SearchListener;
42  import org.sat4j.specs.TimeoutException;
43  
44  /**
45   * Solver used to display in a writer the CNF instance in Dimacs format.
46   * 
47   * That solver is useful to produce CNF files to be used by third party solvers.
48   * 
49   * @author leberre
50   * 
51   */
52  public class DimacsOutputSolver implements ISolver {
53  
54  	/**
55       * 
56       */
57  	private static final long serialVersionUID = 1L;
58  
59  	private transient PrintWriter out;
60  
61  	private int nbvars;
62  
63  	private int nbclauses;
64  
65  	private boolean fixedNbClauses = false;
66  
67  	private boolean firstConstr = true;
68  
69  	public DimacsOutputSolver() {
70  		this(new PrintWriter(System.out, true));
71  	}
72  
73  	public DimacsOutputSolver(PrintWriter pw) {
74  		out = pw;
75  	}
76  
77  	private void readObject(ObjectInputStream stream) {
78  		out = new PrintWriter(System.out, true);
79  	}
80  
81  	public int newVar() {
82  		return 0;
83  	}
84  
85  	public int newVar(int howmany) {
86  		out.print("p cnf " + howmany);
87  		nbvars = howmany;
88  		return 0;
89  	}
90  
91  	public void setExpectedNumberOfClauses(int nb) {
92  		out.println(" " + nb);
93  		nbclauses = nb;
94  		fixedNbClauses = true;
95  	}
96  
97  	public IConstr addClause(IVecInt literals) throws ContradictionException {
98  		if (firstConstr) {
99  			if (!fixedNbClauses) {
100 				out.println(" XXXXXX");
101 			}
102 			firstConstr = false;
103 		}
104 		for (IteratorInt iterator = literals.iterator(); iterator.hasNext();)
105 			out.print(iterator.next() + " ");
106 		out.println("0");
107 		return null;
108 	}
109 
110 	public boolean removeConstr(IConstr c) {
111 		throw new UnsupportedOperationException();
112 	}
113 
114 	public void addAllClauses(IVec<IVecInt> clauses)
115 			throws ContradictionException {
116 		throw new UnsupportedOperationException();
117 	}
118 
119 	public IConstr addAtMost(IVecInt literals, int degree)
120 			throws ContradictionException {
121 		if (degree > 1) {
122 			throw new UnsupportedOperationException(
123 					"Not a clausal problem! degree " + degree);
124 		}
125 		assert degree == 1;
126 		if (firstConstr) {
127 			if (!fixedNbClauses) {
128 				out.println("XXXXXX");
129 			}
130 			firstConstr = false;
131 		}
132 		for (int i = 0; i <= literals.size(); i++) {
133 			for (int j = i + 1; j < literals.size(); j++) {
134 				out.println("" + (-literals.get(i)) + " " + (-literals.get(j))
135 						+ " 0");
136 			}
137 		}
138 		return null;
139 	}
140 
141 	public IConstr addAtLeast(IVecInt literals, int degree)
142 			throws ContradictionException {
143 		if (degree > 1) {
144 			throw new UnsupportedOperationException(
145 					"Not a clausal problem! degree " + degree);
146 		}
147 		assert degree == 1;
148 		return addClause(literals);
149 	}
150 
151 	public void setTimeout(int t) {
152 		// TODO Auto-generated method stub
153 	}
154 
155 	public void setTimeoutMs(long t) {
156 		// TODO Auto-generated method stub
157 	}
158 
159 	public int getTimeout() {
160 		return 0;
161 	}
162 
163 	/**
164 	 * @since 2.1
165 	 */
166 	public long getTimeoutMs() {
167 		return 0L;
168 	}
169 
170 	public void reset() {
171 		fixedNbClauses = false;
172 		firstConstr = true;
173 
174 	}
175 
176 	public void printStat(PrintStream output, String prefix) {
177 		// TODO Auto-generated method stub
178 
179 	}
180 
181 	public void printStat(PrintWriter output, String prefix) {
182 		// TODO Auto-generated method stub
183 
184 	}
185 
186 	public Map<String, Number> getStat() {
187 		// TODO Auto-generated method stub
188 		return null;
189 	}
190 
191 	public String toString(String prefix) {
192 		return "Dimacs output solver";
193 	}
194 
195 	public void clearLearntClauses() {
196 		// TODO Auto-generated method stub
197 
198 	}
199 
200 	public int[] model() {
201 		throw new UnsupportedOperationException();
202 	}
203 
204 	public boolean model(int var) {
205 		throw new UnsupportedOperationException();
206 	}
207 
208 	public boolean isSatisfiable() throws TimeoutException {
209 		throw new TimeoutException("There is no real solver behind!");
210 	}
211 
212 	public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
213 		throw new TimeoutException("There is no real solver behind!");
214 	}
215 
216 	public int[] findModel() throws TimeoutException {
217 		throw new UnsupportedOperationException();
218 	}
219 
220 	public int[] findModel(IVecInt assumps) throws TimeoutException {
221 		throw new UnsupportedOperationException();
222 	}
223 
224 	public int nConstraints() {
225 		return nbclauses;
226 	}
227 
228 	public int nVars() {
229 		return nbvars;
230 	}
231 
232 	public void expireTimeout() {
233 		// TODO Auto-generated method stub
234 
235 	}
236 
237 	public boolean isSatisfiable(IVecInt assumps, boolean global)
238 			throws TimeoutException {
239 		throw new TimeoutException("There is no real solver behind!");
240 	}
241 
242 	public boolean isSatisfiable(boolean global) throws TimeoutException {
243 		throw new TimeoutException("There is no real solver behind!");
244 	}
245 
246 	public void printInfos(PrintWriter output, String prefix) {
247 	}
248 
249 	public void setTimeoutOnConflicts(int count) {
250 	}
251 
252 	public boolean isDBSimplificationAllowed() {
253 		return false;
254 	}
255 
256 	public void setDBSimplificationAllowed(boolean status) {
257 	}
258 
259 	/**
260 	 * @since 2.1
261 	 */
262 	public void setSearchListener(SearchListener sl) {
263 	}
264 
265 	/**
266 	 * @since 2.1
267 	 */
268 	public int nextFreeVarId(boolean reserve) {
269 		throw new UnsupportedOperationException();
270 	}
271 
272 	/**
273 	 * @since 2.1
274 	 */
275 	public boolean removeSubsumedConstr(IConstr c) {
276 		return false;
277 	}
278 
279 	/**
280 	 * @since 2.1
281 	 */
282 	public IConstr addBlockingClause(IVecInt literals)
283 			throws ContradictionException {
284 		throw new UnsupportedOperationException();
285 	}
286 
287 	/**
288 	 * @since 2.2
289 	 */
290 	public SearchListener getSearchListener() {
291 		throw new UnsupportedOperationException();
292 	}
293 
294 	/**
295 	 * @since 2.2
296 	 */
297 	public boolean isVerbose() {
298 		return true;
299 	}
300 
301 	/**
302 	 * @since 2.2
303 	 */
304 	public void setVerbose(boolean value) {
305 		// do nothing
306 	}
307 
308 	/**
309 	 * @since 2.2
310 	 */
311 	public void setLogPrefix(String prefix) {
312 		// do nothing
313 
314 	}
315 
316 	/**
317 	 * @since 2.2
318 	 */
319 	public String getLogPrefix() {
320 		return "";
321 	}
322 
323 	/**
324 	 * @since 2.2
325 	 */
326 	public IVecInt unsatExplanation() {
327 		throw new UnsupportedOperationException();
328 	}
329 }