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 static org.sat4j.core.LiteralsUtils.neg;
33  
34  import java.io.Serializable;
35  
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.UnitPropagationListener;
40  import org.sat4j.specs.IVecInt;
41  
42  /**
43   * Lazy data structure for clause using the Head Tail data structure from SATO,
44   * The original scheme is improved by avoiding moving pointers to literals but
45   * moving the literals themselves.
46   * 
47   * We suppose here that the clause contains at least 3 literals. Use the
48   * BinaryClause or UnaryClause clause data structures to deal with binary and
49   * unit clauses.
50   * 
51   * @author leberre
52   * @see BinaryClause
53   * @see UnitClause
54   * @since 2.1
55   */
56  public abstract class HTClause implements Propagatable, Constr, Serializable {
57  
58      private static final long serialVersionUID = 1L;
59  
60      protected double activity;
61  
62      protected final int[] middleLits;
63  
64      protected final ILits voc;
65  
66      protected int head;
67  
68      protected int tail;
69  
70      /**
71       * Creates a new basic clause
72       * 
73       * @param voc
74       *            the vocabulary of the formula
75       * @param ps
76       *            A VecInt that WILL BE EMPTY after calling that method.
77       */
78      public HTClause(IVecInt ps, ILits voc) {
79          assert ps.size() > 1;
80          this.head = ps.get(0);
81          this.tail = ps.last();
82          final int size = ps.size() - 2;
83          assert size > 0;
84          this.middleLits = new int[size];
85          System.arraycopy(ps.toArray(), 1, this.middleLits, 0, size);
86          ps.clear();
87          assert ps.size() == 0;
88          this.voc = voc;
89          this.activity = 0;
90      }
91  
92      /*
93       * (non-Javadoc)
94       * 
95       * @see Constr#calcReason(Solver, Lit, Vec)
96       */
97      public void calcReason(int p, IVecInt outReason) {
98          if (this.voc.isFalsified(this.head)) {
99              outReason.push(neg(this.head));
100         }
101         final int[] mylits = this.middleLits;
102         for (int mylit : mylits) {
103             if (this.voc.isFalsified(mylit)) {
104                 outReason.push(neg(mylit));
105             }
106         }
107         if (this.voc.isFalsified(this.tail)) {
108             outReason.push(neg(this.tail));
109         }
110     }
111 
112     /*
113      * (non-Javadoc)
114      * 
115      * @see Constr#remove(Solver)
116      */
117     public void remove(UnitPropagationListener upl) {
118         this.voc.watches(neg(this.head)).remove(this);
119         this.voc.watches(neg(this.tail)).remove(this);
120     }
121 
122     /*
123      * (non-Javadoc)
124      * 
125      * @see Constr#simplify(Solver)
126      */
127     public boolean simplify() {
128         if (this.voc.isSatisfied(this.head) || this.voc.isSatisfied(this.tail)) {
129             return true;
130         }
131         for (int middleLit : this.middleLits) {
132             if (this.voc.isSatisfied(middleLit)) {
133                 return true;
134             }
135         }
136         return false;
137     }
138 
139     public boolean propagate(UnitPropagationListener s, int p) {
140 
141         if (this.head == neg(p)) {
142             final int[] mylits = this.middleLits;
143             int temphead = 0;
144             // moving head on the right
145             while (temphead < mylits.length
146                     && this.voc.isFalsified(mylits[temphead])) {
147                 temphead++;
148             }
149             assert temphead <= mylits.length;
150             if (temphead == mylits.length) {
151                 this.voc.watch(p, this);
152                 return s.enqueue(this.tail, this);
153             }
154             this.head = mylits[temphead];
155             mylits[temphead] = neg(p);
156             this.voc.watch(neg(this.head), this);
157             return true;
158         }
159         assert this.tail == neg(p);
160         final int[] mylits = this.middleLits;
161         int temptail = mylits.length - 1;
162         // moving tail on the left
163         while (temptail >= 0 && this.voc.isFalsified(mylits[temptail])) {
164             temptail--;
165         }
166         assert -1 <= temptail;
167         if (-1 == temptail) {
168             this.voc.watch(p, this);
169             return s.enqueue(this.head, this);
170         }
171         this.tail = mylits[temptail];
172         mylits[temptail] = neg(p);
173         this.voc.watch(neg(this.tail), this);
174         return true;
175     }
176 
177     /*
178      * For learnt clauses only @author leberre
179      */
180     public boolean locked() {
181         return this.voc.getReason(this.head) == this
182                 || this.voc.getReason(this.tail) == this;
183     }
184 
185     /**
186      * @return the activity of the clause
187      */
188     public double getActivity() {
189         return this.activity;
190     }
191 
192     @Override
193     public String toString() {
194         StringBuffer stb = new StringBuffer();
195         stb.append(Lits.toString(this.head));
196         stb.append("["); //$NON-NLS-1$
197         stb.append(this.voc.valueToString(this.head));
198         stb.append("]"); //$NON-NLS-1$
199         stb.append(" "); //$NON-NLS-1$
200         for (int middleLit : this.middleLits) {
201             stb.append(Lits.toString(middleLit));
202             stb.append("["); //$NON-NLS-1$
203             stb.append(this.voc.valueToString(middleLit));
204             stb.append("]"); //$NON-NLS-1$
205             stb.append(" "); //$NON-NLS-1$
206         }
207         stb.append(Lits.toString(this.tail));
208         stb.append("["); //$NON-NLS-1$
209         stb.append(this.voc.valueToString(this.tail));
210         stb.append("]"); //$NON-NLS-1$
211         return stb.toString();
212     }
213 
214     /**
215      * Return the ith literal of the clause. Note that the order of the literals
216      * does change during the search...
217      * 
218      * @param i
219      *            the index of the literal
220      * @return the literal
221      */
222     public int get(int i) {
223         if (i == 0) {
224             return this.head;
225         }
226         if (i == this.middleLits.length + 1) {
227             return this.tail;
228         }
229         return this.middleLits[i - 1];
230     }
231 
232     /**
233      * @param d
234      */
235     public void rescaleBy(double d) {
236         this.activity *= d;
237     }
238 
239     public int size() {
240         return this.middleLits.length + 2;
241     }
242 
243     public void assertConstraint(UnitPropagationListener s) {
244         assert this.voc.isUnassigned(this.head);
245         boolean ret = s.enqueue(this.head, this);
246         assert ret;
247     }
248 
249     public ILits getVocabulary() {
250         return this.voc;
251     }
252 
253     public int[] getLits() {
254         int[] tmp = new int[size()];
255         System.arraycopy(this.middleLits, 0, tmp, 1, this.middleLits.length);
256         tmp[0] = this.head;
257         tmp[tmp.length - 1] = this.tail;
258         return tmp;
259     }
260 
261     @Override
262     public boolean equals(Object obj) {
263         if (obj == null) {
264             return false;
265         }
266         try {
267             HTClause wcl = (HTClause) obj;
268             if (wcl.head != this.head || wcl.tail != this.tail) {
269                 return false;
270             }
271             if (this.middleLits.length != wcl.middleLits.length) {
272                 return false;
273             }
274             boolean ok;
275             for (int lit : this.middleLits) {
276                 ok = false;
277                 for (int lit2 : wcl.middleLits) {
278                     if (lit == lit2) {
279                         ok = true;
280                         break;
281                     }
282                 }
283                 if (!ok) {
284                     return false;
285                 }
286             }
287             return true;
288         } catch (ClassCastException e) {
289             return false;
290         }
291     }
292 
293     @Override
294     public int hashCode() {
295         long sum = this.head + this.tail;
296         for (int p : this.middleLits) {
297             sum += p;
298         }
299         return (int) sum / this.middleLits.length;
300     }
301 
302     public boolean canBePropagatedMultipleTimes() {
303         return false;
304     }
305 
306     public Constr toConstraint() {
307         return this;
308     }
309 }