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 java.io.Serializable;
31
32 import org.sat4j.minisat.core.Constr;
33 import org.sat4j.minisat.core.ILits;
34 import org.sat4j.minisat.core.Undoable;
35 import org.sat4j.minisat.core.UnitPropagationListener;
36 import org.sat4j.specs.IVecInt;
37
38 /**
39 * @author leberre
40 */
41 public class CBClause implements Constr, Undoable, Serializable {
42
43 private static final long serialVersionUID = 1L;
44
45 protected int falsified;
46
47 private boolean learnt;
48
49 protected final int[] lits;
50
51 protected final ILits voc;
52
53 private double activity;
54
55 public static CBClause brandNewClause(UnitPropagationListener s, ILits voc,
56 IVecInt literals) {
57 CBClause c = new CBClause(literals, voc);
58 c.register();
59 return c;
60 }
61
62 /**
63 *
64 */
65 public CBClause(IVecInt ps, ILits voc, boolean learnt) {
66 this.learnt = learnt;
67 this.lits = new int[ps.size()];
68 this.voc = voc;
69 ps.moveTo(this.lits);
70 }
71
72 public CBClause(IVecInt ps, ILits voc) {
73 this(ps, voc, false);
74 }
75
76 /*
77 * (non-Javadoc)
78 *
79 * @see org.sat4j.minisat.core.Constr#remove()
80 */
81 public void remove() {
82 for (int i = 0; i < lits.length; i++) {
83 voc.attaches(lits[i] ^ 1).remove(this);
84 }
85 }
86
87 /*
88 * (non-Javadoc)
89 *
90 * @see org.sat4j.minisat.core.Constr#propagate(org.sat4j.minisat.core.UnitPropagationListener,
91 * int)
92 */
93 public boolean propagate(UnitPropagationListener s, int p) {
94 voc.undos(p).push(this);
95 falsified++;
96 assert falsified != lits.length;
97 if (falsified == lits.length - 1) {
98 // find unassigned literal
99 for (int i = 0; i < lits.length; i++) {
100 if (!voc.isFalsified(lits[i])) {
101 return s.enqueue(lits[i], this);
102 }
103 }
104 // one of the variable in to be propagated to false.
105 // (which explains why the falsified counter has not
106 // been increased yet)
107 return false;
108 }
109 return true;
110 }
111
112 /*
113 * (non-Javadoc)
114 *
115 * @see org.sat4j.minisat.core.Constr#simplify()
116 */
117 public boolean simplify() {
118 for (int p : lits) {
119 if (voc.isSatisfied(p)) {
120 return true;
121 }
122 }
123 return false;
124 }
125
126 /*
127 * (non-Javadoc)
128 *
129 * @see org.sat4j.minisat.core.Constr#undo(int)
130 */
131 public void undo(int p) {
132 falsified--;
133 }
134
135 /*
136 * (non-Javadoc)
137 *
138 * @see org.sat4j.minisat.core.Constr#calcReason(int,
139 * org.sat4j.specs.VecInt)
140 */
141 public void calcReason(int p, IVecInt outReason) {
142 assert outReason.size() == 0;
143 for (int q : lits) {
144 assert voc.isFalsified(q) || q == p;
145 if (voc.isFalsified(q)) {
146 outReason.push(q ^ 1);
147 }
148 }
149 assert (p == ILits.UNDEFINED) || (outReason.size() == lits.length - 1);
150 }
151
152 /*
153 * (non-Javadoc)
154 *
155 * @see org.sat4j.minisat.core.Constr#learnt()
156 */
157 public boolean learnt() {
158 return learnt;
159 }
160
161 /*
162 * (non-Javadoc)
163 *
164 * @see org.sat4j.minisat.core.Constr#incActivity(double)
165 */
166 public void incActivity(double claInc) {
167 activity += claInc;
168 }
169
170 /*
171 * (non-Javadoc)
172 *
173 * @see org.sat4j.minisat.core.Constr#getActivity()
174 */
175 public double getActivity() {
176 return activity;
177 }
178
179 /*
180 * (non-Javadoc)
181 *
182 * @see org.sat4j.minisat.core.Constr#locked()
183 */
184 public boolean locked() {
185 for (int p : lits) {
186 if (voc.isSatisfied(p)) {
187 return voc.getReason(p) == this;
188 }
189 }
190 return false;
191 }
192
193 /*
194 * (non-Javadoc)
195 *
196 * @see org.sat4j.minisat.core.Constr#setLearnt()
197 */
198 public void setLearnt() {
199 learnt = true;
200 }
201
202 /*
203 * (non-Javadoc)
204 *
205 * @see org.sat4j.minisat.core.Constr#register()
206 */
207 public void register() {
208 for (int p : lits) {
209 voc.attach(p ^ 1, this);
210 }
211 if (learnt) {
212 for (int p : lits) {
213 if (voc.isFalsified(p)) {
214 voc.undos(p ^ 1).push(this);
215 falsified++;
216 }
217 }
218 assert falsified == lits.length - 1;
219 }
220 }
221
222 /*
223 * (non-Javadoc)
224 *
225 * @see org.sat4j.minisat.core.Constr#rescaleBy(double)
226 */
227 public void rescaleBy(double d) {
228 activity *= d;
229 }
230
231 /*
232 * (non-Javadoc)
233 *
234 * @see org.sat4j.minisat.core.Constr#size()
235 */
236 public int size() {
237 return lits.length;
238 }
239
240 /*
241 * (non-Javadoc)
242 *
243 * @see org.sat4j.minisat.core.Constr#get(int)
244 */
245 public int get(int i) {
246 return lits[i];
247 }
248
249 /*
250 * (non-Javadoc)
251 *
252 * @see org.sat4j.minisat.core.Constr#assertConstraint(org.sat4j.minisat.core.UnitPropagationListener)
253 */
254 public void assertConstraint(UnitPropagationListener s) {
255 assert voc.isUnassigned(lits[0]);
256 boolean ret = s.enqueue(lits[0], this);
257 assert ret;
258 }
259
260 @Override
261 public String toString() {
262 StringBuffer stb = new StringBuffer();
263 for (int i = 0; i < lits.length; i++) {
264 stb.append(lits[i]);
265 stb.append("["); //$NON-NLS-1$
266 stb.append(voc.valueToString(lits[i]));
267 stb.append("]"); //$NON-NLS-1$
268 stb.append(" "); //$NON-NLS-1$
269 }
270 return stb.toString();
271 }
272 }