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.constraints.cnf;
31  
32  import java.io.Serializable;
33  
34  import org.sat4j.core.LiteralsUtils;
35  import org.sat4j.core.Vec;
36  import org.sat4j.minisat.core.Constr;
37  import org.sat4j.minisat.core.ILits;
38  import org.sat4j.minisat.core.Propagatable;
39  import org.sat4j.minisat.core.Undoable;
40  import org.sat4j.specs.IVec;
41  
42  /**
43   * @author laihem
44   * @author leberre
45   * 
46   */
47  public final class Lits implements Serializable, ILits {
48  
49      private static final int DEFAULT_INIT_SIZE = 128;
50  
51      private static final long serialVersionUID = 1L;
52  
53      private boolean pool[] = new boolean[1];
54  
55      private int realnVars = 0;
56  
57      @SuppressWarnings("unchecked")
58      private IVec<Propagatable>[] watches = new IVec[0];
59  
60      private int[] level = new int[0];
61  
62      private Constr[] reason = new Constr[0];
63  
64      private int maxvarid = 0;
65  
66      @SuppressWarnings("unchecked")
67      private IVec<Undoable>[] undos = new IVec[0];
68  
69      private boolean[] falsified = new boolean[0];
70  
71      public Lits() {
72          init(DEFAULT_INIT_SIZE);
73      }
74  
75      @SuppressWarnings({ "unchecked" })
76      public void init(int nvar) {
77          if (nvar < this.pool.length) {
78              return;
79          }
80          assert nvar >= 0;
81          // let some space for unused 0 indexer.
82          int nvars = nvar + 1;
83          boolean[] npool = new boolean[nvars];
84          System.arraycopy(this.pool, 0, npool, 0, this.pool.length);
85          this.pool = npool;
86  
87          int[] nlevel = new int[nvars];
88          System.arraycopy(this.level, 0, nlevel, 0, this.level.length);
89          this.level = nlevel;
90  
91          IVec<Propagatable>[] nwatches = new IVec[2 * nvars];
92          System.arraycopy(this.watches, 0, nwatches, 0, this.watches.length);
93          this.watches = nwatches;
94  
95          IVec<Undoable>[] nundos = new IVec[nvars];
96          System.arraycopy(this.undos, 0, nundos, 0, this.undos.length);
97          this.undos = nundos;
98  
99          Constr[] nreason = new Constr[nvars];
100         System.arraycopy(this.reason, 0, nreason, 0, this.reason.length);
101         this.reason = nreason;
102 
103         boolean[] newFalsified = new boolean[2 * nvars];
104         System.arraycopy(this.falsified, 0, newFalsified, 0,
105                 this.falsified.length);
106         this.falsified = newFalsified;
107     }
108 
109     public int getFromPool(int x) {
110         int var = Math.abs(x);
111         if (var >= this.pool.length) {
112             init(Math.max(var, this.pool.length << 1));
113         }
114         assert var < this.pool.length;
115         if (var > this.maxvarid) {
116             this.maxvarid = var;
117         }
118         int lit = LiteralsUtils.toInternal(x);
119         assert lit > 1;
120         if (!this.pool[var]) {
121             this.realnVars++;
122             this.pool[var] = true;
123             this.watches[var << 1] = new Vec<Propagatable>();
124             this.watches[var << 1 | 1] = new Vec<Propagatable>();
125             this.undos[var] = new Vec<Undoable>();
126             this.level[var] = -1;
127             this.falsified[var << 1] = false; // because truthValue[var] is
128             // UNDEFINED
129             this.falsified[var << 1 | 1] = false; // because truthValue[var] is
130             // UNDEFINED
131         }
132         return lit;
133     }
134 
135     public boolean belongsToPool(int x) {
136         assert x > 0;
137         if (x >= this.pool.length) {
138             return false;
139         }
140         return this.pool[x];
141     }
142 
143     public void resetPool() {
144         for (int i = 0; i < this.pool.length; i++) {
145             if (this.pool[i]) {
146                 reset(i << 1);
147             }
148         }
149         this.maxvarid = 0;
150         this.realnVars = 0;
151     }
152 
153     public void ensurePool(int howmany) {
154         if (howmany >= this.pool.length) {
155             init(Math.max(howmany, this.pool.length << 1));
156         }
157         this.maxvarid = howmany;
158     }
159 
160     public void unassign(int lit) {
161         assert this.falsified[lit] || this.falsified[lit ^ 1];
162         this.falsified[lit] = false;
163         this.falsified[lit ^ 1] = false;
164     }
165 
166     public void satisfies(int lit) {
167         assert !this.falsified[lit] && !this.falsified[lit ^ 1];
168         this.falsified[lit] = false;
169         this.falsified[lit ^ 1] = true;
170     }
171 
172     public void forgets(int var) {
173         this.falsified[var << 1] = true;
174         this.falsified[var << 1 ^ 1] = true;
175     }
176 
177     public boolean isSatisfied(int lit) {
178         return this.falsified[lit ^ 1];
179     }
180 
181     public boolean isFalsified(int lit) {
182         return this.falsified[lit];
183     }
184 
185     public boolean isUnassigned(int lit) {
186         return !this.falsified[lit] && !this.falsified[lit ^ 1];
187     }
188 
189     public String valueToString(int lit) {
190         if (isUnassigned(lit)) {
191             return "?"; //$NON-NLS-1$
192         }
193         if (isSatisfied(lit)) {
194             return "T"; //$NON-NLS-1$
195         }
196         return "F"; //$NON-NLS-1$
197     }
198 
199     public int nVars() {
200         // return pool.length - 1;
201         return this.maxvarid;
202     }
203 
204     public int not(int lit) {
205         return lit ^ 1;
206     }
207 
208     public static String toString(int lit) {
209         return ((lit & 1) == 0 ? "" : "-") + (lit >> 1); //$NON-NLS-1$//$NON-NLS-2$
210     }
211 
212     public void reset(int lit) {
213         this.watches[lit].clear();
214         this.watches[lit ^ 1].clear();
215         this.level[lit >> 1] = -1;
216         this.reason[lit >> 1] = null;
217         this.undos[lit >> 1].clear();
218         this.falsified[lit] = false;
219         this.falsified[lit ^ 1] = false;
220         this.pool[lit >> 1] = false;
221     }
222 
223     public int getLevel(int lit) {
224         return this.level[lit >> 1];
225     }
226 
227     public void setLevel(int lit, int l) {
228         this.level[lit >> 1] = l;
229     }
230 
231     public Constr getReason(int lit) {
232         return this.reason[lit >> 1];
233     }
234 
235     public void setReason(int lit, Constr r) {
236         this.reason[lit >> 1] = r;
237     }
238 
239     public IVec<Undoable> undos(int lit) {
240         return this.undos[lit >> 1];
241     }
242 
243     public void watch(int lit, Propagatable c) {
244         this.watches[lit].push(c);
245     }
246 
247     public IVec<Propagatable> watches(int lit) {
248         return this.watches[lit];
249     }
250 
251     public boolean isImplied(int lit) {
252         int var = lit >> 1;
253         assert this.reason[var] == null || this.falsified[lit]
254                 || this.falsified[lit ^ 1];
255         // a literal is implied if it is a unit clause, ie
256         // propagated without reason at decision level 0.
257         return this.pool[var]
258                 && (this.reason[var] != null || this.level[var] == 0);
259     }
260 
261     public int realnVars() {
262         return this.realnVars;
263     }
264 
265     /**
266      * To get the capacity of the current vocabulary.
267      * 
268      * @return the total number of variables that can be managed by the
269      *         vocabulary.
270      */
271     protected int capacity() {
272         return this.pool.length - 1;
273     }
274 
275     /**
276      * @since 2.1
277      */
278     public int nextFreeVarId(boolean reserve) {
279         if (reserve) {
280             ensurePool(this.maxvarid + 1);
281             // ensure pool changes maxvarid
282             return this.maxvarid;
283         }
284         return this.maxvarid + 1;
285     }
286 }