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 * To inform the solver of the expected number of clauses to read. This is
69 * an optional method, that is called when the <code>p cnf</code> line is
70 * read in dimacs formatted input file.
71 *
72 * Note that this method is supposed to be called AFTER a call to newVar(int)
73 *
74 * @param nb
75 * the expected number of clauses.
76 * @see #newVar(int)
77 * @since 1.6
78 */
79 void setExpectedNumberOfClauses(int nb);
80
81 /**
82 * Create a clause from a set of literals The literals are represented by
83 * non null integers such that opposite literals a represented by opposite
84 * values. (classical Dimacs way of representing literals).
85 *
86 * @param literals
87 * a set of literals
88 * @return a reference to the constraint added in the solver, to use in
89 * removeConstr().
90 * @throws ContradictionException
91 * iff the vector of literals is empty or if it contains only
92 * falsified literals after unit propagation
93 * @see #removeConstr(IConstr)
94 */
95 IConstr addClause(IVecInt literals) throws ContradictionException;
96
97 /**
98 * Remove a constraint returned by one of the add method from the solver.
99 * All learned clauses will be cleared.
100 *
101 * Current implementation does not handle properly the case of unit clauses.
102 *
103 * @param c
104 * a constraint returned by one of the add method.
105 * @return true if the constraint was successfully removed.
106 */
107 boolean removeConstr(IConstr c);
108
109 /**
110 * Create clauses from a set of set of literals. This is convenient to
111 * create in a single call all the clauses (mandatory for the distributed
112 * version of the solver). It is mainly a loop to addClause().
113 *
114 * @param clauses
115 * a vector of set (VecInt) of literals in the dimacs format. The
116 * vector can be reused since the solver is not supposed to keep
117 * a reference to that vector.
118 * @throws ContradictionException
119 * iff the vector of literals is empty or if it contains only
120 * falsified literals after unit propagation
121 * @see #addClause(IVecInt)
122 */
123 void addAllClauses(IVec<IVecInt> clauses) throws ContradictionException;
124
125 /**
126 * Create a cardinality constraint of the type "at most n of those literals
127 * must be satisfied"
128 *
129 * @param literals
130 * a set of literals The vector can be reused since the solver is
131 * not supposed to keep a reference to that vector.
132 * @param degree
133 * the degree of the cardinality constraint
134 * @return a reference to the constraint added in the solver, to use in
135 * removeConstr().
136 * @throws ContradictionException
137 * iff the vector of literals is empty or if it contains more
138 * than degree satisfied literals after unit propagation
139 * @see #removeConstr(IConstr)
140 */
141
142 IConstr addAtMost(IVecInt literals, int degree)
143 throws ContradictionException;
144
145 /**
146 * Create a cardinality constraint of the type "at least n of those literals
147 * must be satisfied"
148 *
149 * @param literals
150 * a set of literals. The vector can be reused since the solver
151 * is not supposed to keep a reference to that vector.
152 * @param degree
153 * the degree of the cardinality constraint
154 * @return a reference to the constraint added in the solver, to use in
155 * removeConstr().
156 * @throws ContradictionException
157 * iff the vector of literals is empty or if degree literals are
158 * not remaining unfalsified after unit propagation
159 * @see #removeConstr(IConstr)
160 */
161 IConstr addAtLeast(IVecInt literals, int degree)
162 throws ContradictionException;
163
164 /**
165 * To set the internal timeout of the solver. When the timeout is reached, a
166 * timeout exception is launched by the solver.
167 *
168 * @param t
169 * the timeout (in s)
170 */
171 void setTimeout(int t);
172
173 /**
174 * To set the internal timeout of the solver. When the timeout is reached, a
175 * timeout exception is launched by the solver.
176 *
177 * Here the timeout is given in number of conflicts. That way, the behavior
178 * of the solver should be the same across different architecture.
179 *
180 * @param count
181 * the timeout (in number of counflicts)
182 */
183 void setTimeoutOnConflicts(int count);
184
185 /**
186 * To set the internal timeout of the solver. When the timeout is reached, a
187 * timeout exception is launched by the solver.
188 *
189 * @param t
190 * the timeout (in milliseconds)
191 */
192 void setTimeoutMs(long t);
193
194 /**
195 * Useful to check the internal timeout of the solver.
196 *
197 * @return the internal timeout of the solver (in seconds)
198 */
199 int getTimeout();
200
201 /**
202 * Useful to check the internal timeout of the solver.
203 *
204 * @return the internal timeout of the solver (in milliseconds)
205 */
206 long getTimeoutMs();
207
208 /**
209 * Expire the timeout of the solver.
210 */
211 void expireTimeout();
212
213 /**
214 * Clean up the internal state of the solver.
215 */
216 void reset();
217
218 /**
219 * Display statistics to the given output stream Please use writers instead
220 * of stream.
221 *
222 * @param out
223 * @param prefix
224 * the prefix to put in front of each line
225 * @see #printStat(PrintWriter, String)
226 */
227 @Deprecated
228 void printStat(PrintStream out, String prefix);
229
230 /**
231 * Display statistics to the given output writer
232 *
233 * @param out
234 * @param prefix
235 * the prefix to put in front of each line
236 * @since 1.6
237 */
238 void printStat(PrintWriter out, String prefix);
239
240 /**
241 * To obtain a map of the available statistics from the solver. Note that
242 * some keys might be specific to some solvers.
243 *
244 * @return a Map with the name of the statistics as key.
245 */
246 Map<String, Number> getStat();
247
248 /**
249 * Display a textual representation of the solver configuration.
250 *
251 * @param prefix
252 * the prefix to use on each line.
253 * @return a textual description of the solver internals.
254 */
255 String toString(String prefix);
256
257 /**
258 * Remove clauses learned during the solving process.
259 */
260 void clearLearntClauses();
261
262 /**
263 * Set whether the solver is allowed to simplify the formula
264 * by propagating the truth value of top level satisfied variables.
265 *
266 * Note that the solver should not be allowed to perform such simplification
267 * when constraint removal is planned.
268 */
269 void setDBSimplificationAllowed(boolean status);
270
271 /**
272 * Indicate whether the solver is allowed to simplify the formula
273 * by propagating the truth value of top level satisfied variables.
274 *
275 * Note that the solver should not be allowed to perform such simplification
276 * when constraint removal is planned.
277 */
278 boolean isDBSimplificationAllowed();
279 }