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.PrintWriter;
31
32 /**
33 * Access to the information related to a given problem instance.
34 *
35 * @author leberre
36 */
37 public interface IProblem {
38 /**
39 * Provide a model (if any) for a satisfiable formula. That method should be
40 * called AFTER isSatisfiable() or isSatisfiable(IVecInt) if the formula is
41 * satisfiable. Else an exception UnsupportedOperationException is launched.
42 *
43 * @return a model of the formula as an array of literals to satisfy.
44 * @see #isSatisfiable()
45 * @see #isSatisfiable(IVecInt)
46 */
47 int[] model();
48
49 /**
50 * Provide the truth value of a specific variable in the model. That method
51 * should be called AFTER isSatisfiable() if the formula is satisfiable.
52 * Else an exception UnsupportedOperationException is launched.
53 *
54 * @param var
55 * the variable id in Dimacs format
56 * @return the truth value of that variable in the model
57 * @since 1.6
58 * @see #model()
59 */
60 boolean model(int var);
61
62 /**
63 * Check the satisfiability of the set of constraints contained inside the
64 * solver.
65 *
66 * @return true if the set of constraints is satisfiable, else false.
67 */
68 boolean isSatisfiable() throws TimeoutException;
69
70 /**
71 * Check the satisfiability of the set of constraints contained inside the
72 * solver.
73 *
74 * @param assumps
75 * a set of literals (represented by usual non null integers
76 * in Dimacs format).
77 * @param globalTimeout
78 * whether that call is part of a global process (i.e.
79 * optimization) or not. if (global), the timeout will not be
80 * reset between each call.
81 * @return true if the set of constraints is satisfiable when literals are
82 * satisfied, else false.
83 */
84 boolean isSatisfiable(IVecInt assumps, boolean globalTimeout)
85 throws TimeoutException;
86
87 /**
88 * Check the satisfiability of the set of constraints contained inside the
89 * solver.
90 *
91 * @param globalTimeout
92 * whether that call is part of a global process (i.e.
93 * optimization) or not. if (global), the timeout will not be
94 * reset between each call.
95 * @return true if the set of constraints is satisfiable, else false.
96 */
97 boolean isSatisfiable(boolean globalTimeout) throws TimeoutException;
98
99 /**
100 * Check the satisfiability of the set of constraints contained inside the
101 * solver.
102 *
103 * @param assumps
104 * a set of literals (represented by usual non null integers
105 * in Dimacs format).
106 * @return true if the set of constraints is satisfiable when literals are
107 * satisfied, else false.
108 */
109 boolean isSatisfiable(IVecInt assumps) throws TimeoutException;
110
111 /**
112 * Look for a model satisfying all the clauses available in the problem. It
113 * is an alternative to isSatisfiable() and model() methods, as shown in the
114 * pseudo-code: <code>
115 if (isSatisfiable()) {
116 return model();
117 }
118 return null;
119 </code>
120 *
121 * @return a model of the formula as an array of literals to satisfy, or
122 * <code>null</code> if no model is found
123 * @throws TimeoutException
124 * if a model cannot be found within the given timeout.
125 * @since 1.7
126 */
127 int[] findModel() throws TimeoutException;
128
129 /**
130 * Look for a model satisfying all the clauses available in the problem. It
131 * is an alternative to isSatisfiable(IVecInt) and model() methods, as shown
132 * in the pseudo-code: <code>
133 if (isSatisfiable(assumpt)) {
134 return model();
135 }
136 return null;
137 </code>
138 *
139 * @return a model of the formula as an array of literals to satisfy, or
140 * <code>null</code> if no model is found
141 * @throws TimeoutException
142 * if a model cannot be found within the given timeout.
143 * @since 1.7
144 */
145 int[] findModel(IVecInt assumps) throws TimeoutException;
146
147 /**
148 * To know the number of constraints currently available in the solver.
149 * (without taking into account learned constraints).
150 *
151 * @return the number of constraints added to the solver
152 */
153 int nConstraints();
154
155 /**
156 * To know the number of variables used in the solver.
157 *
158 * @return the number of variables created using newVar().
159 */
160 int nVars();
161
162 /**
163 * To print additional informations regarding the problem.
164 *
165 * @param out
166 * the place to print the information
167 * @param prefix
168 * the prefix to put in front of each line
169 */
170 void printInfos(PrintWriter out, String prefix);
171
172 }