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.minisat.core;
31
32 import org.sat4j.specs.IVec;
33
34 /**
35 * That interface manages the solver's internal vocabulary. Everything related
36 * to variables and literals is available from here.
37 *
38 * For sake of efficiency, literals and variables are not object in SAT4J. They
39 * are represented by numbers. If the vocabulary contains n variables, then
40 * variables should be accessed by numbers from 1 to n and literals by numbers
41 * from 2 to 2*n+1.
42 *
43 * For a Dimacs variable v, the variable index in SAT4J is v, it's positive
44 * literal is 2*v (v << 1) and it's negative literal is 2*v+1 ((v<<1)^1). Note
45 * that one can easily access to the complementary literal of p by using bitwise
46 * operation ^.
47 *
48 * In SAT4J, literals are usualy denoted by p or q and variables by v or x.
49 *
50 * @author leberre
51 */
52 public interface ILits {
53
54 public static int UNDEFINED = -1;
55
56 public abstract void init(int nvar);
57
58 /**
59 * Translates a Dimacs literal into an internal representation literal.
60 *
61 * @param x
62 * the Dimacs literal (a non null integer).
63 * @return the literal in the internal representation.
64 */
65 public abstract int getFromPool(int x);
66
67 /**
68 * Returns true iff the variable is used in the set of constraints.
69 *
70 * @param x
71 * @return true iff the variable belongs to the formula.
72 */
73 boolean belongsToPool(int x);
74
75 /**
76 * reset the vocabulary.
77 */
78 void resetPool();
79
80 /**
81 * Make sure that all data structures are ready to manage howmany boolean
82 * variables.
83 *
84 * @param howmany
85 * the new capacity (in boolean variables) of the vocabulary.
86 */
87 void ensurePool(int howmany);
88
89 /**
90 * Unassigns a boolean variable (truth value if UNDEF).
91 *
92 * @param lit
93 * a literal in internal format.
94 */
95 void unassign(int lit);
96
97 /**
98 * Satisfies a boolean variable (truth value is TRUE).
99 *
100 * @param lit
101 * a literal in internal format.
102 */
103 void satisfies(int lit);
104
105 /**
106 * Removes a variable from the formula. All occurrences of that variables
107 * are removed. It is equivalent in our implementation to falsify the two
108 * phases of that variable.
109 *
110 * @param var
111 * a variable in Dimacs format.
112 * @since 2.3.2
113 */
114 void forgets(int var);
115
116 /**
117 * Check if a literal is satisfied.
118 *
119 * @param lit
120 * a literal in internal format.
121 * @return true if that literal is satisfied.
122 */
123 boolean isSatisfied(int lit);
124
125 /**
126 * Check if a literal is falsified.
127 *
128 * @param lit
129 * a literal in internal format.
130 * @return true if the literal is falsified. Note that a forgotten variable
131 * will also see its literals as falsified.
132 */
133 boolean isFalsified(int lit);
134
135 /**
136 * Check if a literal is assigned a truth value.
137 *
138 * @param lit
139 * a literal in internal format.
140 * @return true if the literal is neither satisfied nor falsified.
141 */
142 boolean isUnassigned(int lit);
143
144 /**
145 * @param lit
146 * @return true iff the truth value of that literal is due to a unit
147 * propagation or a decision.
148 */
149 public abstract boolean isImplied(int lit);
150
151 /**
152 * to obtain the max id of the variable
153 *
154 * @return the maximum number of variables in the formula
155 */
156 public abstract int nVars();
157
158 /**
159 * to obtain the real number of variables appearing in the formula
160 *
161 * @return the number of variables used in the pool
162 */
163 int realnVars();
164
165 /**
166 * Ask the solver for a free variable identifier, in Dimacs format (i.e. a
167 * positive number). Note that a previous call to ensurePool(max) will
168 * reserve in the solver the variable identifier from 1 to max, so
169 * nextFreeVarId() would return max+1, even if some variable identifiers
170 * smaller than max are not used.
171 *
172 * @return a variable identifier not in use in the constraints already
173 * inside the solver.
174 * @since 2.1
175 */
176 int nextFreeVarId(boolean reserve);
177
178 /**
179 * Reset a literal in the vocabulary.
180 *
181 * @param lit
182 * a literal in internal representation.
183 */
184 void reset(int lit);
185
186 /**
187 * Returns the level at which that literal has been assigned a value, else
188 * -1.
189 *
190 * @param lit
191 * a literal in internal representation.
192 * @return -1 if the literal is unassigned, or the decision level of the
193 * literal.
194 */
195 int getLevel(int lit);
196
197 /**
198 * Sets the decision level of a literal.
199 *
200 * @param lit
201 * a literal in internal representation.
202 * @param l
203 * a decision level, or -1
204 */
205 void setLevel(int lit, int l);
206
207 /**
208 * Returns the reason of the assignment of a literal.
209 *
210 * @param lit
211 * a literal in internal representation.
212 * @return the constraint that propagated that literal, else null.
213 */
214 Constr getReason(int lit);
215
216 /**
217 * Sets the reason of the assignment of a literal.
218 *
219 * @param lit
220 * a literal in internal representation.
221 * @param r
222 * the constraint that forces the assignment of that literal,
223 * null if there are none.
224 */
225 void setReason(int lit, Constr r);
226
227 /**
228 * Retrieve the methods to call when the solver backtracks. Useful for
229 * counter based data structures.
230 *
231 * @param lit
232 * a literal in internal representation.
233 * @return a list of methods to call on bactracking.
234 */
235 IVec<Undoable> undos(int lit);
236
237 /**
238 * Record a new constraint to watch when a literal is satisfied.
239 *
240 * @param lit
241 * a literal in internal representation.
242 * @param c
243 * a constraint that contains the negation of that literal.
244 */
245 void watch(int lit, Propagatable c);
246
247 /**
248 * @param lit
249 * a literal in internal representation.
250 * @return the list of all the constraints that watch the negation of lit
251 */
252 public abstract IVec<Propagatable> watches(int lit);
253
254 /**
255 * Returns a textual representation of the truth value of that literal.
256 *
257 * @param lit
258 * a literal in internal representation.
259 * @return one of T for true, F for False or ? for unassigned.
260 */
261 String valueToString(int lit);
262 }