1 /*
2 * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3 *
4 * Based on the original minisat specification from:
5 *
6 * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7 * Sixth International Conference on Theory and Applications of Satisfiability
8 * Testing, LNCS 2919, pp 502-518, 2003.
9 *
10 * This library is free software; you can redistribute it and/or modify it under
11 * the terms of the GNU Lesser General Public License as published by the Free
12 * Software Foundation; either version 2.1 of the License, or (at your option)
13 * any later version.
14 *
15 * This library is distributed in the hope that it will be useful, but WITHOUT
16 * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17 * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18 * details.
19 *
20 * You should have received a copy of the GNU Lesser General Public License
21 * along with this library; if not, write to the Free Software Foundation, Inc.,
22 * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
23 *
24 */
25
26 package org.sat4j.specs;
27
28 import java.io.PrintStream;
29 import java.io.PrintWriter;
30 import java.io.Serializable;
31 import java.math.BigInteger;
32 import java.util.Map;
33
34 /**
35 * That interface contains all the services available on a SAT solver.
36 *
37 * @author leberre
38 */
39 public interface ISolver extends IProblem, Serializable {
40
41 /**
42 * Create a new variable in the solver (and thus in the vocabulary).
43 *
44 * WE STRONGLY ENCOURAGE TO PRECOMPUTE THE NUMBER OF VARIABLES NEEDED AND TO
45 * USE newVar(howmany) INSTEAD. IF YOU EXPERIENCE A PROBLEM OF EFFICIENCY
46 * WHEN READING/BUILDING YOUR SAT INSTANCE, PLEASE CHECK THAT YOU ARE NOT
47 * USING THAT METHOD.
48 *
49 * @return the number of variables available in the vocabulary, which is the
50 * identifier of the new variable.
51 */
52 @Deprecated
53 int newVar();
54
55 /**
56 * Create <code>howmany</code> variables in the solver (and thus in the
57 * vocabulary).
58 *
59 * @param howmany
60 * number of variables to create
61 * @return the total number of variables available in the solver (the
62 * highest variable number)
63 */
64 int newVar(int howmany);
65
66 /**
67 * To inform the solver of the expected number of clauses to read. This is
68 * an optional method, that is called when the <code>p cnf</code> line is
69 * read in dimacs formatted input file.
70 *
71 * @param nb
72 * the expected number of clauses.
73 * @since 1.6
74 */
75 void setExpectedNumberOfClauses(int nb);
76
77 /**
78 * Create a clause from a set of literals The literals are represented by
79 * non null integers such that opposite literals a represented by opposite
80 * values. (clasical Dimacs way of representing literals).
81 *
82 * @param literals
83 * a set of literals
84 * @return a reference to the constraint added in the solver, to use in
85 * removeConstr().
86 * @throws ContradictionException
87 * iff the vector of literals is empty or if it contains only
88 * falsified literals after unit propagation
89 * @see #removeConstr(IConstr)
90 */
91 IConstr addClause(IVecInt literals) throws ContradictionException;
92
93 /**
94 * Remove a constraint returned by one of the add method from the solver.
95 * All learnt clauses will be cleared.
96 *
97 * @param c
98 * a constraint returned by one of the add method.
99 * @return true if the constraint was sucessfully removed.
100 */
101 boolean removeConstr(IConstr c);
102
103 /**
104 * Create clauses from a set of set of literals. This is convenient to
105 * create in a single call all the clauses (mandatory for the distributed
106 * version of the solver). It is mainly a loop to addClause().
107 *
108 * @param clauses
109 * a vector of set (VecInt) of literals in the dimacs format. The
110 * vector can be reused since the solver is not supposed to keep
111 * a reference to that vector.
112 * @throws ContradictionException
113 * iff the vector of literals is empty or if it contains only
114 * falsified literals after unit propagation
115 * @see #addClause(IVecInt)
116 */
117 void addAllClauses(IVec<IVecInt> clauses) throws ContradictionException;
118
119 /**
120 * Create a cardinality constraint of the type "at most n of those literals
121 * must be satisfied"
122 *
123 * @param literals
124 * a set of literals The vector can be reused since the solver is
125 * not supposed to keep a reference to that vector.
126 * @param degree
127 * the degree of the cardinality constraint
128 * @return a reference to the constraint added in the solver, to use in
129 * removeConstr().
130 * @throws ContradictionException
131 * iff the vector of literals is empty or if it contains more
132 * than degree satisfied literals after unit propagation
133 * @see #removeConstr(IConstr)
134 */
135
136 IConstr addAtMost(IVecInt literals, int degree)
137 throws ContradictionException;
138
139 /**
140 * Create a cardinality constraint of the type "at least n of those literals
141 * must be satisfied"
142 *
143 * @param literals
144 * a set of literals. The vector can be reused since the solver
145 * is not supposed to keep a reference to that vector.
146 * @param degree
147 * the degree of the cardinality constraint
148 * @return a reference to the constraint added in the solver, to use in
149 * removeConstr().
150 * @throws ContradictionException
151 * iff the vector of literals is empty or if degree literals are
152 * not remaining unfalsified after unit propagation
153 * @see #removeConstr(IConstr)
154 */
155 IConstr addAtLeast(IVecInt literals, int degree)
156 throws ContradictionException;
157
158 /**
159 * Create a Pseudo-Boolean constraint of the type "at least n of those
160 * literals must be satisfied"
161 *
162 * @param lits
163 * a set of literals. The vector can be reused since the solver
164 * is not supposed to keep a reference to that vector.
165 * @param coeffs
166 * the coefficients of the literals. The vector can be reused
167 * since the solver is not supposed to keep a reference to that
168 * vector.
169 * @param moreThan
170 * true if it is a constraint >= degree
171 * @param d
172 * the degree of the cardinality constraint
173 * @return a reference to the constraint added in the solver, to use in
174 * removeConstr().
175 * @throws ContradictionException
176 * iff the vector of literals is empty or if the constraint is
177 * falsified after unit propagation
178 * @see #removeConstr(IConstr)
179 */
180 IConstr addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs,
181 boolean moreThan, BigInteger d) throws ContradictionException;
182
183 /**
184 * To set the internal timeout of the solver. When the timeout is reached, a
185 * timeout exception is launched by the solver.
186 *
187 * @param t
188 * the timeout (in s)
189 */
190 void setTimeout(int t);
191
192 /**
193 * To set the internal timeout of the solver. When the timeout is reached, a
194 * timeout exception is launched by the solver.
195 *
196 * @param t
197 * the timeout (in milliseconds)
198 */
199 void setTimeoutMs(long t);
200
201 /**
202 * Useful to check the internal timeout of the solver.
203 *
204 * @return the internal timeout of the solver (in second)
205 */
206 int getTimeout();
207
208 /**
209 * Clean up the internal state of the solver.
210 */
211 void reset();
212
213 /**
214 * Display statistics to the given output stream Please use writers instead
215 * of stream.
216 *
217 * @param out
218 * @param prefix
219 * the prefix to put in front of each line
220 * @see #printStat(PrintWriter, String)
221 */
222 @Deprecated
223 void printStat(PrintStream out, String prefix);
224
225 /**
226 * Display statistics to the given output writer
227 *
228 * @param out
229 * @param prefix
230 * the prefix to put in front of each line
231 * @since 1.6
232 */
233 void printStat(PrintWriter out, String prefix);
234
235 /**
236 * To obtain a map of the available statistics from the solver. Note that
237 * some keys might be specific to some solvers.
238 *
239 * @return a Map with the name of the statistics as key.
240 */
241 Map<String, Number> getStat();
242
243 /**
244 * Display a textual representation of the solver configuration.
245 *
246 * @param prefix
247 * the prefix to use on each line.
248 * @return a textual description of the solver internals.
249 */
250 String toString(String prefix);
251
252 void clearLearntClauses();
253 }