View Javadoc

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