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