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   * Data structure for binary clause.
44   * 
45   * @author leberre
46   * @since 2.1
47   */
48  public abstract class BinaryClause implements Propagatable, Constr,
49          Serializable {
50  
51      private static final long serialVersionUID = 1L;
52  
53      protected double activity;
54  
55      private final ILits voc;
56  
57      protected int head;
58  
59      protected int tail;
60  
61      /**
62       * Creates a new basic clause
63       * 
64       * @param voc
65       *            the vocabulary of the formula
66       * @param ps
67       *            A VecInt that WILL BE EMPTY after calling that method.
68       */
69      public BinaryClause(IVecInt ps, ILits voc) {
70          assert ps.size() == 2;
71          this.head = ps.get(0);
72          this.tail = ps.get(1);
73          this.voc = voc;
74          this.activity = 0;
75      }
76  
77      /*
78       * (non-Javadoc)
79       * 
80       * @see Constr#calcReason(Solver, Lit, Vec)
81       */
82      public void calcReason(int p, IVecInt outReason) {
83          if (this.voc.isFalsified(this.head)) {
84              outReason.push(neg(this.head));
85          }
86          if (this.voc.isFalsified(this.tail)) {
87              outReason.push(neg(this.tail));
88          }
89      }
90  
91      /*
92       * (non-Javadoc)
93       * 
94       * @see Constr#remove(Solver)
95       */
96      public void remove(UnitPropagationListener upl) {
97          this.voc.watches(neg(this.head)).remove(this);
98          this.voc.watches(neg(this.tail)).remove(this);
99      }
100 
101     /*
102      * (non-Javadoc)
103      * 
104      * @see Constr#simplify(Solver)
105      */
106     public boolean simplify() {
107         if (this.voc.isSatisfied(this.head) || this.voc.isSatisfied(this.tail)) {
108             return true;
109         }
110         return false;
111     }
112 
113     public boolean propagate(UnitPropagationListener s, int p) {
114         this.voc.watch(p, this);
115         if (this.head == neg(p)) {
116             return s.enqueue(this.tail, this);
117         }
118         assert this.tail == neg(p);
119         return s.enqueue(this.head, this);
120     }
121 
122     /*
123      * For learnt clauses only @author leberre
124      */
125     public boolean locked() {
126         return this.voc.getReason(this.head) == this
127                 || this.voc.getReason(this.tail) == this;
128     }
129 
130     /**
131      * @return the activity of the clause
132      */
133     public double getActivity() {
134         return this.activity;
135     }
136 
137     @Override
138     public String toString() {
139         StringBuffer stb = new StringBuffer();
140         stb.append(Lits.toString(this.head));
141         stb.append("["); //$NON-NLS-1$
142         stb.append(this.voc.valueToString(this.head));
143         stb.append("]"); //$NON-NLS-1$
144         stb.append(" "); //$NON-NLS-1$
145         stb.append(Lits.toString(this.tail));
146         stb.append("["); //$NON-NLS-1$
147         stb.append(this.voc.valueToString(this.tail));
148         stb.append("]"); //$NON-NLS-1$
149         return stb.toString();
150     }
151 
152     /**
153      * Retourne le ieme literal de la clause. Attention, cet ordre change durant
154      * la recherche.
155      * 
156      * @param i
157      *            the index of the literal
158      * @return the literal
159      */
160     public int get(int i) {
161         if (i == 0) {
162             return this.head;
163         }
164         assert i == 1;
165         return this.tail;
166     }
167 
168     /**
169      * @param d
170      */
171     public void rescaleBy(double d) {
172         this.activity *= d;
173     }
174 
175     public int size() {
176         return 2;
177     }
178 
179     public void assertConstraint(UnitPropagationListener s) {
180         assert this.voc.isUnassigned(this.head);
181         boolean ret = s.enqueue(this.head, this);
182         assert ret;
183     }
184 
185     public ILits getVocabulary() {
186         return this.voc;
187     }
188 
189     public int[] getLits() {
190         int[] tmp = new int[2];
191         tmp[0] = this.head;
192         tmp[1] = this.tail;
193         return tmp;
194     }
195 
196     @Override
197     public boolean equals(Object obj) {
198         if (obj == null) {
199             return false;
200         }
201         try {
202             BinaryClause wcl = (BinaryClause) obj;
203             if (wcl.head != this.head || wcl.tail != this.tail) {
204                 return false;
205             }
206             return true;
207         } catch (ClassCastException e) {
208             return false;
209         }
210     }
211 
212     @Override
213     public int hashCode() {
214         long sum = this.head + this.tail;
215         return (int) sum / 2;
216     }
217 
218     public void register() {
219         this.voc.watch(neg(this.head), this);
220         this.voc.watch(neg(this.tail), this);
221     }
222 
223     public boolean canBePropagatedMultipleTimes() {
224         return false;
225     }
226 
227     public Constr toConstraint() {
228         return this;
229     }
230 }