View Javadoc

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      int UNDEFINED = -1;
55  
56      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      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     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     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     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 }