1 /*
2 * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3 *
4 * Based on the original minisat specification from:
5 *
6 * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7 * Sixth International Conference on Theory and Applications of Satisfiability
8 * Testing, LNCS 2919, pp 502-518, 2003.
9 *
10 * This library is free software; you can redistribute it and/or modify it under
11 * the terms of the GNU Lesser General Public License as published by the Free
12 * Software Foundation; either version 2.1 of the License, or (at your option)
13 * any later version.
14 *
15 * This library is distributed in the hope that it will be useful, but WITHOUT
16 * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17 * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18 * details.
19 *
20 * You should have received a copy of the GNU Lesser General Public License
21 * along with this library; if not, write to the Free Software Foundation, Inc.,
22 * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
23 *
24 */
25
26 package org.sat4j.minisat.constraints.cnf;
27
28 import java.io.Serializable;
29
30 import org.sat4j.minisat.core.Constr;
31 import org.sat4j.minisat.core.ILits;
32 import org.sat4j.minisat.core.Undoable;
33 import org.sat4j.minisat.core.UnitPropagationListener;
34 import org.sat4j.specs.IVecInt;
35
36 /**
37 * @author leberre
38 */
39 public class CBClause implements Constr, Undoable, Serializable {
40
41 private static final long serialVersionUID = 1L;
42
43 protected int falsified;
44
45 private boolean learnt;
46
47 protected final int[] lits;
48
49 protected final ILits voc;
50
51 private double activity;
52
53 public static CBClause brandNewClause(UnitPropagationListener s, ILits voc,
54 IVecInt literals) {
55 CBClause c = new CBClause(literals, voc);
56 c.register();
57 return c;
58 }
59
60 /**
61 *
62 */
63 public CBClause(IVecInt ps, ILits voc, boolean learnt) {
64 this.learnt = learnt;
65 this.lits = new int[ps.size()];
66 this.voc = voc;
67 ps.moveTo(this.lits);
68 }
69
70 public CBClause(IVecInt ps, ILits voc) {
71 this(ps, voc, false);
72 }
73
74 /*
75 * (non-Javadoc)
76 *
77 * @see org.sat4j.minisat.core.Constr#remove()
78 */
79 public void remove() {
80 for (int i = 0; i < lits.length; i++) {
81 voc.watches(lits[i] ^ 1).remove(this);
82 }
83 }
84
85 /*
86 * (non-Javadoc)
87 *
88 * @see org.sat4j.minisat.core.Constr#propagate(org.sat4j.minisat.core.UnitPropagationListener,
89 * int)
90 */
91 public boolean propagate(UnitPropagationListener s, int p) {
92 voc.undos(p).push(this);
93 falsified++;
94 assert falsified != lits.length;
95 if (falsified == lits.length - 1) {
96 // find unassigned literal
97 for (int i = 0; i < lits.length; i++) {
98 if (!voc.isFalsified(lits[i])) {
99 return s.enqueue(lits[i], this);
100 }
101 }
102 // one of the variable in to be propagated to false.
103 // (which explains why the falsified counter has not
104 // been increased yet)
105 return false;
106 }
107 return true;
108 }
109
110 /*
111 * (non-Javadoc)
112 *
113 * @see org.sat4j.minisat.core.Constr#simplify()
114 */
115 public boolean simplify() {
116 for (int p : lits) {
117 if (voc.isSatisfied(p)) {
118 return true;
119 }
120 }
121 return false;
122 }
123
124 /*
125 * (non-Javadoc)
126 *
127 * @see org.sat4j.minisat.core.Constr#undo(int)
128 */
129 public void undo(int p) {
130 falsified--;
131 }
132
133 /*
134 * (non-Javadoc)
135 *
136 * @see org.sat4j.minisat.core.Constr#calcReason(int,
137 * org.sat4j.specs.VecInt)
138 */
139 public void calcReason(int p, IVecInt outReason) {
140 assert outReason.size() == 0;
141 for (int q : lits) {
142 assert voc.isFalsified(q) || q == p;
143 if (voc.isFalsified(q)) {
144 outReason.push(q ^ 1);
145 }
146 }
147 assert (p == ILits.UNDEFINED) || (outReason.size() == lits.length - 1);
148 }
149
150 /*
151 * (non-Javadoc)
152 *
153 * @see org.sat4j.minisat.core.Constr#learnt()
154 */
155 public boolean learnt() {
156 return learnt;
157 }
158
159 /*
160 * (non-Javadoc)
161 *
162 * @see org.sat4j.minisat.core.Constr#incActivity(double)
163 */
164 public void incActivity(double claInc) {
165 activity += claInc;
166 }
167
168 /*
169 * (non-Javadoc)
170 *
171 * @see org.sat4j.minisat.core.Constr#getActivity()
172 */
173 public double getActivity() {
174 return activity;
175 }
176
177 /*
178 * (non-Javadoc)
179 *
180 * @see org.sat4j.minisat.core.Constr#locked()
181 */
182 public boolean locked() {
183 return voc.getReason(lits[0]) == this;
184 }
185
186 /*
187 * (non-Javadoc)
188 *
189 * @see org.sat4j.minisat.core.Constr#setLearnt()
190 */
191 public void setLearnt() {
192 learnt = true;
193 }
194
195 /*
196 * (non-Javadoc)
197 *
198 * @see org.sat4j.minisat.core.Constr#register()
199 */
200 public void register() {
201 for (int p : lits) {
202 voc.watch(p ^ 1, this);
203 }
204 if (learnt) {
205 for (int p : lits) {
206 if (voc.isFalsified(p)) {
207 voc.undos(p ^ 1).push(this);
208 falsified++;
209 }
210 }
211 assert falsified == lits.length - 1;
212 }
213 }
214
215 /*
216 * (non-Javadoc)
217 *
218 * @see org.sat4j.minisat.core.Constr#rescaleBy(double)
219 */
220 public void rescaleBy(double d) {
221 activity *= d;
222 }
223
224 /*
225 * (non-Javadoc)
226 *
227 * @see org.sat4j.minisat.core.Constr#size()
228 */
229 public int size() {
230 return lits.length;
231 }
232
233 /*
234 * (non-Javadoc)
235 *
236 * @see org.sat4j.minisat.core.Constr#get(int)
237 */
238 public int get(int i) {
239 return lits[i];
240 }
241
242 /*
243 * (non-Javadoc)
244 *
245 * @see org.sat4j.minisat.core.Constr#assertConstraint(org.sat4j.minisat.core.UnitPropagationListener)
246 */
247 public void assertConstraint(UnitPropagationListener s) {
248 assert voc.isUnassigned(lits[0]);
249 boolean ret = s.enqueue(lits[0], this);
250 assert ret;
251 }
252
253 @Override
254 public String toString() {
255 StringBuffer stb = new StringBuffer();
256 for (int i = 0; i < lits.length; i++) {
257 stb.append(lits[i]);
258 stb.append("["); //$NON-NLS-1$
259 stb.append(voc.valueToString(lits[i]));
260 stb.append("]"); //$NON-NLS-1$
261 stb.append(" "); //$NON-NLS-1$
262 }
263 return stb.toString();
264 }
265 }