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.specs;
29  
30  import java.io.PrintStream;
31  import java.io.PrintWriter;
32  import java.io.Serializable;
33  import java.util.Map;
34  
35  /**
36   * This interface contains all services provided by a SAT solver.
37   * 
38   * @author leberre
39   */
40  public interface ISolver extends IProblem, Serializable {
41  
42  	/**
43  	 * Create a new variable in the solver (and thus in the vocabulary).
44  	 * 
45  	 * WE STRONGLY ENCOURAGE TO PRECOMPUTE THE NUMBER OF VARIABLES NEEDED AND TO
46  	 * USE newVar(howmany) INSTEAD. IF YOU EXPERIENCE A PROBLEM OF EFFICIENCY
47  	 * WHEN READING/BUILDING YOUR SAT INSTANCE, PLEASE CHECK THAT YOU ARE NOT
48  	 * USING THAT METHOD.
49  	 * 
50  	 * @return the number of variables available in the vocabulary, which is the
51  	 *         identifier of the new variable.
52  	 */
53  	@Deprecated
54  	int newVar();
55  
56  	/**
57  	 * Create <code>howmany</code> variables in the solver (and thus in the
58  	 * vocabulary).
59  	 * 
60  	 * @param howmany
61  	 *            number of variables to create
62  	 * @return the total number of variables available in the solver (the
63  	 *         highest variable number)
64  	 */
65  	int newVar(int howmany);
66  
67  	/**
68  	 * Ask the solver for a free variable identifier, in Dimacs format (i.e. a
69  	 * positive number). Note that a previous call to newVar(max) will reserve
70  	 * in the solver the variable identifier from 1 to max, so nextFreeVarId()
71  	 * would return max+1, even if some variable identifiers smaller than max
72  	 * are not used. By default, the method will always answer by the maximum
73  	 * variable identifier used so far + 1.
74  	 * 
75  	 * @param reserve
76  	 *            if true, the maxVarId is updated in the solver, i.e.
77  	 *            successive calls to nextFreeVarId(true) will return increasing
78  	 *            variable id while successive calls to nextFreeVarId(false)
79  	 *            will always answer the same.
80  	 * @return a variable identifier not in use in the constraints already
81  	 *         inside the solver.
82  	 * @since 2.1
83  	 */
84  	int nextFreeVarId(boolean reserve);
85  
86  	/**
87  	 * To inform the solver of the expected number of clauses to read. This is
88  	 * an optional method, that is called when the <code>p cnf</code> line is
89  	 * read in dimacs formatted input file.
90  	 * 
91  	 * Note that this method is supposed to be called AFTER a call to
92  	 * newVar(int)
93  	 * 
94  	 * @param nb
95  	 *            the expected number of clauses.
96  	 * @see #newVar(int)
97  	 * @since 1.6
98  	 */
99  	void setExpectedNumberOfClauses(int nb);
100 
101 	/**
102 	 * Create a clause from a set of literals The literals are represented by
103 	 * non null integers such that opposite literals a represented by opposite
104 	 * values. (classical Dimacs way of representing literals).
105 	 * 
106 	 * @param literals
107 	 *            a set of literals
108 	 * @return a reference to the constraint added in the solver, to use in
109 	 *         removeConstr().
110 	 * @throws ContradictionException
111 	 *             iff the vector of literals is empty or if it contains only
112 	 *             falsified literals after unit propagation
113 	 * @see #removeConstr(IConstr)
114 	 */
115 	IConstr addClause(IVecInt literals) throws ContradictionException;
116 
117 	/**
118 	 * Add a clause in order to prevent an assignment to occur. This happens
119 	 * usually when iterating over models for instance.
120 	 * 
121 	 * @param literals
122 	 * @return
123 	 * @throws ContradictionException
124 	 * @since 2.1
125 	 */
126 	IConstr addBlockingClause(IVecInt literals) throws ContradictionException;
127 
128 	/**
129 	 * Remove a constraint returned by one of the add method from the solver.
130 	 * All learned clauses will be cleared.
131 	 * 
132 	 * Current implementation does not handle properly the case of unit clauses.
133 	 * 
134 	 * @param c
135 	 *            a constraint returned by one of the add method.
136 	 * @return true if the constraint was successfully removed.
137 	 */
138 	boolean removeConstr(IConstr c);
139 
140 	/**
141 	 * Remove a constraint returned by one of the add method from the solver
142 	 * that is subsumed by a constraint already in the solver or to be added to
143 	 * the solver.
144 	 * 
145 	 * Unlike the removeConstr() method, learned clauses will NOT be cleared.
146 	 * 
147 	 * That method is expected to be used to remove constraints used in the
148 	 * optimization process.
149 	 * 
150 	 * In order to prevent a wrong from the user, the method will only work if
151 	 * the argument is the last constraint added to the solver. An illegal
152 	 * argument exception will be thrown in other cases.
153 	 * 
154 	 * @param c
155 	 *            a constraint returned by one of the add method. It must be the
156 	 *            latest constr added to the solver.
157 	 * @return true if the constraint was successfully removed.
158 	 * @since 2.1
159 	 */
160 	boolean removeSubsumedConstr(IConstr c);
161 
162 	/**
163 	 * Create clauses from a set of set of literals. This is convenient to
164 	 * create in a single call all the clauses (mandatory for the distributed
165 	 * version of the solver). It is mainly a loop to addClause().
166 	 * 
167 	 * @param clauses
168 	 *            a vector of set (VecInt) of literals in the dimacs format. The
169 	 *            vector can be reused since the solver is not supposed to keep
170 	 *            a reference to that vector.
171 	 * @throws ContradictionException
172 	 *             iff the vector of literals is empty or if it contains only
173 	 *             falsified literals after unit propagation
174 	 * @see #addClause(IVecInt)
175 	 */
176 	void addAllClauses(IVec<IVecInt> clauses) throws ContradictionException;
177 
178 	/**
179 	 * Create a cardinality constraint of the type "at most n of those literals
180 	 * must be satisfied"
181 	 * 
182 	 * @param literals
183 	 *            a set of literals The vector can be reused since the solver is
184 	 *            not supposed to keep a reference to that vector.
185 	 * @param degree
186 	 *            the degree of the cardinality constraint
187 	 * @return a reference to the constraint added in the solver, to use in
188 	 *         removeConstr().
189 	 * @throws ContradictionException
190 	 *             iff the vector of literals is empty or if it contains more
191 	 *             than degree satisfied literals after unit propagation
192 	 * @see #removeConstr(IConstr)
193 	 */
194 
195 	IConstr addAtMost(IVecInt literals, int degree)
196 			throws ContradictionException;
197 
198 	/**
199 	 * Create a cardinality constraint of the type "at least n of those literals
200 	 * must be satisfied"
201 	 * 
202 	 * @param literals
203 	 *            a set of literals. The vector can be reused since the solver
204 	 *            is not supposed to keep a reference to that vector.
205 	 * @param degree
206 	 *            the degree of the cardinality constraint
207 	 * @return a reference to the constraint added in the solver, to use in
208 	 *         removeConstr().
209 	 * @throws ContradictionException
210 	 *             iff the vector of literals is empty or if degree literals are
211 	 *             not remaining unfalsified after unit propagation
212 	 * @see #removeConstr(IConstr)
213 	 */
214 	IConstr addAtLeast(IVecInt literals, int degree)
215 			throws ContradictionException;
216 
217 	/**
218 	 * To set the internal timeout of the solver. When the timeout is reached, a
219 	 * timeout exception is launched by the solver.
220 	 * 
221 	 * @param t
222 	 *            the timeout (in s)
223 	 */
224 	void setTimeout(int t);
225 
226 	/**
227 	 * To set the internal timeout of the solver. When the timeout is reached, a
228 	 * timeout exception is launched by the solver.
229 	 * 
230 	 * Here the timeout is given in number of conflicts. That way, the behavior
231 	 * of the solver should be the same across different architecture.
232 	 * 
233 	 * @param count
234 	 *            the timeout (in number of counflicts)
235 	 */
236 	void setTimeoutOnConflicts(int count);
237 
238 	/**
239 	 * To set the internal timeout of the solver. When the timeout is reached, a
240 	 * timeout exception is launched by the solver.
241 	 * 
242 	 * @param t
243 	 *            the timeout (in milliseconds)
244 	 */
245 	void setTimeoutMs(long t);
246 
247 	/**
248 	 * Useful to check the internal timeout of the solver.
249 	 * 
250 	 * @return the internal timeout of the solver (in seconds)
251 	 */
252 	int getTimeout();
253 
254 	/**
255 	 * Useful to check the internal timeout of the solver.
256 	 * 
257 	 * @return the internal timeout of the solver (in milliseconds)
258 	 * @since 2.1
259 	 */
260 	long getTimeoutMs();
261 
262 	/**
263 	 * Expire the timeout of the solver.
264 	 */
265 	void expireTimeout();
266 
267 	/**
268 	 * Clean up the internal state of the solver.
269 	 */
270 	void reset();
271 
272 	/**
273 	 * Display statistics to the given output stream Please use writers instead
274 	 * of stream.
275 	 * 
276 	 * @param out
277 	 * @param prefix
278 	 *            the prefix to put in front of each line
279 	 * @see #printStat(PrintWriter, String)
280 	 */
281 	@Deprecated
282 	void printStat(PrintStream out, String prefix);
283 
284 	/**
285 	 * Display statistics to the given output writer
286 	 * 
287 	 * @param out
288 	 * @param prefix
289 	 *            the prefix to put in front of each line
290 	 * @since 1.6
291 	 */
292 	void printStat(PrintWriter out, String prefix);
293 
294 	/**
295 	 * To obtain a map of the available statistics from the solver. Note that
296 	 * some keys might be specific to some solvers.
297 	 * 
298 	 * @return a Map with the name of the statistics as key.
299 	 */
300 	Map<String, Number> getStat();
301 
302 	/**
303 	 * Display a textual representation of the solver configuration.
304 	 * 
305 	 * @param prefix
306 	 *            the prefix to use on each line.
307 	 * @return a textual description of the solver internals.
308 	 */
309 	String toString(String prefix);
310 
311 	/**
312 	 * Remove clauses learned during the solving process.
313 	 */
314 	void clearLearntClauses();
315 
316 	/**
317 	 * Set whether the solver is allowed to simplify the formula by propagating
318 	 * the truth value of top level satisfied variables.
319 	 * 
320 	 * Note that the solver should not be allowed to perform such simplification
321 	 * when constraint removal is planned.
322 	 */
323 	void setDBSimplificationAllowed(boolean status);
324 
325 	/**
326 	 * Indicate whether the solver is allowed to simplify the formula by
327 	 * propagating the truth value of top level satisfied variables.
328 	 * 
329 	 * Note that the solver should not be allowed to perform such simplification
330 	 * when constraint removal is planned.
331 	 */
332 	boolean isDBSimplificationAllowed();
333 
334 	/**
335 	 * Allow the user to hook a listener to the solver to be notified of the
336 	 * main steps of the search process.
337 	 * 
338 	 * @param sl
339 	 *            a Search Listener.
340 	 * @since 2.1
341 	 */
342 	void setSearchListener(SearchListener sl);
343 
344 	/**
345 	 * Get the current SearchListener.
346 	 * 
347 	 * @return a Search Listener.
348 	 * @since 2.2
349 	 */
350 	SearchListener getSearchListener();
351 
352 	/**
353 	 * To know if the solver is in verbose mode (output allowed) or not.
354 	 * 
355 	 * @return true if the solver is verbose.
356 	 * @since 2.2
357 	 */
358 	boolean isVerbose();
359 
360 	/**
361 	 * Set the verbosity of the solver
362 	 * 
363 	 * @param value
364 	 *            true to allow the solver to output messages on the console,
365 	 *            false either.
366 	 * @since 2.2
367 	 */
368 	void setVerbose(boolean value);
369 
370 	/**
371 	 * Set the prefix used to display information.
372 	 * 
373 	 * @param prefix
374 	 *            the prefix to be in front of each line of text
375 	 * @since 2.2
376 	 */
377 	void setLogPrefix(String prefix);
378 
379 	/**
380 	 * 
381 	 * @return the string used to prefix the output.
382 	 * @since 2.2
383 	 */
384 	String getLogPrefix();
385 
386 	/**
387 	 * 
388 	 * Retrieve an explanation of the inconsistency in terms of assumption
389 	 * literals. This is only application when isSatisfiable(assumps) is used.
390 	 * Note that !isSatisfiable(assumps)&&assumps.contains(unsatExplanation())
391 	 * should hold.
392 	 * 
393 	 * @return a subset of the assumptions used when calling
394 	 *         isSatisfiable(assumps). Will return null if not applicable (i.e.
395 	 *         no assumptions used).
396 	 * @see #isSatisfiable(IVecInt)
397 	 * @see #isSatisfiable(IVecInt, boolean)
398 	 * @since 2.2
399 	 */
400 	IVecInt unsatExplanation();
401 }