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 /**
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 conflicts)
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 * Note that such method should also be called when you no longer need the
295 * solver because the state of the solver may prevent the GC to proceed.
296 * There is a known issue for instance where failing to call reset() on a
297 * solver will keep timer threads alive and exhausts memory.
298 */
299 void reset();
300
301 /**
302 * Display statistics to the given output stream Please use writers instead
303 * of stream.
304 *
305 * @param out
306 * @param prefix
307 * the prefix to put in front of each line
308 * @see #printStat(PrintWriter, String)
309 */
310 @Deprecated
311 void printStat(PrintStream out, String prefix);
312
313 /**
314 * Display statistics to the given output writer
315 *
316 * @param out
317 * @param prefix
318 * the prefix to put in front of each line
319 * @since 1.6
320 * @deprecated using the prefix does no longer makes sense because the
321 * solver owns it.
322 */
323 @Deprecated
324 void printStat(PrintWriter out, String prefix);
325
326 /**
327 * Display statistics to the given output writer
328 *
329 * @param out
330 * @since 2.3.3
331 *
332 * @see #setLogPrefix(String)
333 */
334 void printStat(PrintWriter out);
335
336 /**
337 * To obtain a map of the available statistics from the solver. Note that
338 * some keys might be specific to some solvers.
339 *
340 * @return a Map with the name of the statistics as key.
341 */
342 Map<String, Number> getStat();
343
344 /**
345 * Display a textual representation of the solver configuration.
346 *
347 * @param prefix
348 * the prefix to use on each line.
349 * @return a textual description of the solver internals.
350 */
351 String toString(String prefix);
352
353 /**
354 * Remove clauses learned during the solving process.
355 */
356 void clearLearntClauses();
357
358 /**
359 * Set whether the solver is allowed to simplify the formula by propagating
360 * the truth value of top level satisfied variables.
361 *
362 * Note that the solver should not be allowed to perform such simplification
363 * when constraint removal is planned.
364 */
365 void setDBSimplificationAllowed(boolean status);
366
367 /**
368 * Indicate whether the solver is allowed to simplify the formula by
369 * propagating the truth value of top level satisfied variables.
370 *
371 * Note that the solver should not be allowed to perform such simplification
372 * when constraint removal is planned.
373 */
374 boolean isDBSimplificationAllowed();
375
376 /**
377 * Allow the user to hook a listener to the solver to be notified of the
378 * main steps of the search process.
379 *
380 * @param sl
381 * a Search Listener.
382 * @since 2.1
383 */
384 <S extends ISolverService> void setSearchListener(SearchListener<S> sl);
385
386 /**
387 * Allow the solver to ask for unit clauses before each restarts.
388 *
389 * @param ucp
390 * an object able to provide unit clauses.
391 * @since 2.3.4
392 */
393 void setUnitClauseProvider(UnitClauseProvider ucp);
394
395 /**
396 * Get the current SearchListener.
397 *
398 * @return a Search Listener.
399 * @since 2.2
400 */
401 <S extends ISolverService> SearchListener<S> getSearchListener();
402
403 /**
404 * To know if the solver is in verbose mode (output allowed) or not.
405 *
406 * @return true if the solver is verbose.
407 * @since 2.2
408 */
409 boolean isVerbose();
410
411 /**
412 * Set the verbosity of the solver
413 *
414 * @param value
415 * true to allow the solver to output messages on the console,
416 * false either.
417 * @since 2.2
418 */
419 void setVerbose(boolean value);
420
421 /**
422 * Set the prefix used to display information.
423 *
424 * @param prefix
425 * the prefix to be in front of each line of text
426 * @since 2.2
427 */
428 void setLogPrefix(String prefix);
429
430 /**
431 *
432 * @return the string used to prefix the output.
433 * @since 2.2
434 */
435 String getLogPrefix();
436
437 /**
438 *
439 * Retrieve an explanation of the inconsistency in terms of assumption
440 * literals. This is only application when isSatisfiable(assumps) is used.
441 * Note that !isSatisfiable(assumps)&&assumps.contains(unsatExplanation())
442 * should hold.
443 *
444 * @return a subset of the assumptions used when calling
445 * isSatisfiable(assumps). Will return null if not applicable (i.e.
446 * no assumptions used).
447 * @see #isSatisfiable(IVecInt)
448 * @see #isSatisfiable(IVecInt, boolean)
449 * @since 2.2
450 */
451 IVecInt unsatExplanation();
452
453 /**
454 * That method is designed to be used to retrieve the real model of the
455 * current set of constraints, i.e. to provide the truth value of boolean
456 * variables used internally in the solver (for encoding purposes for
457 * instance).
458 *
459 * If no variables are added in the solver, then
460 * Arrays.equals(model(),modelWithInternalVariables()).
461 *
462 * In case new variables are added to the solver, then the number of models
463 * returned by that method is greater of equal to the number of models
464 * returned by model() when using a ModelIterator.
465 *
466 * @return an array of literals, in Dimacs format, corresponding to a model
467 * of the formula over all the variables declared in the solver.
468 * @see #model()
469 * @see org.sat4j.tools.ModelIterator
470 * @since 2.3.1
471 */
472 int[] modelWithInternalVariables();
473
474 /**
475 * Retrieve the real number of variables used in the solver.
476 *
477 * In many cases, realNumberOfVariables()==nVars(). However, when working
478 * with SAT encodings or translation from MAXSAT to PMS, one can have
479 * realNumberOfVariables()>nVars().
480 *
481 * Those additional variables are supposed to be created using the
482 * {@link #nextFreeVarId(boolean)} method.
483 *
484 * @return the number of variables reserved in the solver.
485 * @see #nextFreeVarId(boolean)
486 * @since 2.3.1
487 */
488 int realNumberOfVariables();
489
490 /**
491 * Ask to the solver if it is in "hot" mode, meaning that the heuristics is
492 * not reset after call is isSatisfiable(). This is only useful in case of
493 * repeated calls to the solver with same set of variables.
494 *
495 * @return true iff the solver keep the heuristics value unchanged across
496 * calls.
497 * @since 2.3.2
498 */
499 boolean isSolverKeptHot();
500
501 /**
502 * Changed the behavior of the SAT solver heuristics between successive
503 * calls. If the value is true, then the solver will be "hot" on reuse, i.e.
504 * the heuristics will not be reset. Else the heuristics will be reset.
505 *
506 * @param keepHot
507 * true to keep the heuristics values across calls, false either.
508 * @since 2.3.2
509 */
510 void setKeepSolverHot(boolean keepHot);
511
512 /**
513 * Retrieve the real engine in case the engine is decorated by one or
514 * several decorator. This can be used for instance to setup the engine,
515 * which requires to bypass all the decorators.
516 *
517 * It is thus safe to downcast the ISolver to an ICDCL interface. We cannot
518 * directly return an ICDCL object because we are not on the same
519 * abstraction level here.
520 *
521 * @return the solver
522 * @since 2.3.3
523 */
524 ISolver getSolvingEngine();
525 }