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