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 }