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 /**
29 * Access to the information related to a given problem instance.
30 *
31 * @author leberre
32 */
33 public interface IProblem {
34 /**
35 * Provide a model (if any) for a satisfiable formula. That method should be
36 * called AFTER isSatisfiable() or isSatisfiable(IVecInt) if the formula is
37 * satisfiable. Else an exception UnsupportedOperationException is launched.
38 *
39 * @return a model of the formula as an array of literals to satisfy.
40 * @see #isSatisfiable()
41 * @see #isSatisfiable(IVecInt)
42 */
43 int[] model();
44
45 /**
46 * Provide the truth value of a specific variable in the model. That method
47 * should be called AFTER isSatisfiable() if the formula is satisfiable.
48 * Else an exception UnsupportedOperationException is launched.
49 *
50 * @param var
51 * the variable id in Dimacs format
52 * @return the truth value of that variable in the model
53 * @since 1.6
54 * @see #model()
55 */
56 boolean model(int var);
57
58 /**
59 * Check the satisfiability of the set of constraints contained inside the
60 * solver.
61 *
62 * @return true if the set of constraints is satisfiable, else false.
63 */
64 boolean isSatisfiable() throws TimeoutException;
65
66 /**
67 * Check the satisfiability of the set of constraints contained inside the
68 * solver.
69 *
70 * @param assumps
71 * a set of literals (represented by usual non null integers in
72 * Dimacs format).
73 * @return true if the set of constraints is satisfiable when literals are
74 * satisfied, else false.
75 */
76 boolean isSatisfiable(IVecInt assumps) throws TimeoutException;
77
78 /**
79 * Look for a model satisfying all the clauses available in the problem. It
80 * is an alternative to isSatisfiable() and model() methods, as shown in the
81 * pseudo-code: <code>
82 if (isSatisfiable()) {
83 return model();
84 }
85 return null;
86 </code>
87 *
88 * @return a model of the formula as an array of literals to satisfy, or
89 * <code>null</code> if no model is found
90 * @throws TimeoutException
91 * if a model cannot be found within the given timeout.
92 * @since 1.7
93 */
94 int[] findModel() throws TimeoutException;
95
96 /**
97 * Look for a model satisfying all the clauses available in the problem. It
98 * is an alternative to isSatisfiable(IVecInt) and model() methods, as shown
99 * in the pseudo-code: <code>
100 if (isSatisfiable(assumpt)) {
101 return model();
102 }
103 return null;
104 </code>
105 *
106 * @return a model of the formula as an array of literals to satisfy, or
107 * <code>null</code> if no model is found
108 * @throws TimeoutException
109 * if a model cannot be found within the given timeout.
110 * @since 1.7
111 */
112 int[] findModel(IVecInt assumps) throws TimeoutException;
113
114 /**
115 * To know the number of constraints currently available in the solver.
116 * (without taking into account learnt constraints).
117 *
118 * @return the number of contraints added to the solver
119 */
120 int nConstraints();
121
122 /**
123 * To know the number of variables used in the solver.
124 *
125 * @return the number of variables created using newVar().
126 */
127 int nVars();
128
129 }