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.UnitPropagationListener;
33 import org.sat4j.specs.ContradictionException;
34 import org.sat4j.specs.IVecInt;
35
36 /*
37 * Created on 16 oct. 2003 To change the template for this generated file go to
38 * Window>Preferences>Java>Code Generation>Code and Comments
39 */
40
41 /**
42 * Lazy data structure for clause using Watched Literals.
43 *
44 * @author leberre
45 */
46 public abstract class WLClause implements Constr, Serializable {
47
48 private static final long serialVersionUID = 1L;
49
50 private double activity;
51
52 protected final int[] lits;
53
54 protected final ILits voc;
55
56 /**
57 * Creates a new basic clause
58 *
59 * @param voc
60 * the vocabulary of the formula
61 * @param ps
62 * A VecInt that WILL BE EMPTY after calling that method.
63 */
64 public WLClause(IVecInt ps, ILits voc) {
65 lits = new int[ps.size()];
66 ps.moveTo(lits);
67 assert ps.size() == 0;
68 this.voc = voc;
69 activity = 0;
70 }
71
72 /**
73 * Perform some sanity check before constructing a clause a) if a literal is
74 * assigned true, return null (the clause is satisfied) b) if a literal is
75 * assigned false, remove it c) if a clause contains a literal and its
76 * opposite (tautology) return null d) remove duplicate literals e) if the
77 * clause is empty, return null f) if the clause if unit, transmit it to the
78 * object responsible for unit propagation
79 *
80 * @param ps
81 * the list of literals
82 * @param voc
83 * the vocabulary used
84 * @param s
85 * the object responsible for unit propagation
86 * @return null if the clause should be ignored, the (possibly modified)
87 * list of literals otherwise
88 * @throws ContradictionException
89 * if discovered by unit propagation
90 */
91 public static IVecInt sanityCheck(IVecInt ps, ILits voc,
92 UnitPropagationListener s) throws ContradictionException {
93 // si un litt???ral de ps est vrai, retourner vrai
94 // enlever les litt???raux falsifi???s de ps
95 for (int i = 0; i < ps.size();) {
96 // on verifie si le litteral est affecte
97 if (voc.isUnassigned(ps.get(i))) {
98 // on passe au literal suivant
99 i++;
100 } else {
101 // Si le litteral est satisfait, la clause est
102 // satisfaite
103 if (voc.isSatisfied(ps.get(i))) {
104 // on retourne la clause
105 return null;
106 }
107 // on enleve le ieme litteral
108 ps.delete(i);
109
110 }
111 }
112
113 // on trie le vecteur ps
114 ps.sortUnique();
115
116 // ???limine les clauses tautologiques
117 // deux litt???raux de signe oppos???s apparaissent dans la m???me
118 // clause
119 for (int i = 0; i < ps.size() - 1; i++) {
120 if (ps.get(i) == (ps.get(i + 1) ^ 1)) {
121 // la clause est tautologique
122 return null;
123 }
124 }
125
126 if (propagationCheck(ps, s))
127 return null;
128
129 return ps;
130 }
131
132 /**
133 * Check if this clause is null or unit
134 *
135 * @param p
136 * the list of literals (supposed to be clean as after a call to
137 * sanityCheck())
138 * @param s
139 * the object responsible for unit propagation
140 * @return true iff the clause should be ignored (because it's unit)
141 * @throws ContradictionException
142 * when detected by unit propagation
143 */
144 static boolean propagationCheck(IVecInt ps, UnitPropagationListener s)
145 throws ContradictionException {
146 if (ps.size() == 0) {
147 throw new ContradictionException("Creating Empty clause ?"); //$NON-NLS-1$
148 } else if (ps.size() == 1) {
149 if (!s.enqueue(ps.get(0))) {
150 throw new ContradictionException("Contradictory Unit Clauses"); //$NON-NLS-1$
151 }
152 return true;
153 }
154
155 return false;
156 }
157
158 /**
159 * Creates a brand new clause, presumably from external data. Performs all
160 * sanity checks.
161 *
162 * @param s
163 * the object responsible for unit propagation
164 * @param voc
165 * the vocabulary
166 * @param literals
167 * the literals to store in the clause
168 * @return the created clause or null if the clause should be ignored
169 * (tautology for example)
170 */
171 public static WLClause brandNewClause(UnitPropagationListener s, ILits voc,
172 IVecInt literals) {
173 WLClause c = new DefaultWLClause(literals, voc);
174 c.register();
175 return c;
176 }
177
178 /*
179 * (non-Javadoc)
180 *
181 * @see Constr#calcReason(Solver, Lit, Vec)
182 */
183 public void calcReason(int p, IVecInt outReason) {
184 assert outReason.size() == 0
185 && ((p == ILits.UNDEFINED) || (p == lits[0]));
186 final int[] mylits = lits;
187 for (int i = (p == ILits.UNDEFINED) ? 0 : 1; i < mylits.length; i++) {
188 assert voc.isFalsified(mylits[i]);
189 outReason.push(mylits[i] ^ 1);
190 }
191 }
192
193 /*
194 * (non-Javadoc)
195 *
196 * @see Constr#remove(Solver)
197 */
198 public void remove() {
199 voc.watches(lits[0] ^ 1).remove(this);
200 voc.watches(lits[1] ^ 1).remove(this);
201 // la clause peut etre effacee
202 }
203
204 /*
205 * (non-Javadoc)
206 *
207 * @see Constr#simplify(Solver)
208 */
209 public boolean simplify() {
210 for (int i = 0; i < lits.length; i++) {
211 if (voc.isSatisfied(lits[i])) {
212 return true;
213 }
214 }
215 return false;
216 }
217
218 public boolean propagate(UnitPropagationListener s, int p) {
219 final int[] mylits = lits;
220 // Lits[1] doit contenir le litt???ral falsifi???
221 if (mylits[0] == (p ^ 1)) {
222 mylits[0] = mylits[1];
223 mylits[1] = p ^ 1;
224 }
225 assert mylits[1] == (p ^ 1);
226 // // Si le premier litt???ral est satisfait, la clause est satisfaite
227 // The solver appears to solve more benchmarks (while being sometimes
228 // slower)
229 // if commenting those lines.
230 // if (voc.isSatisfied(lits[0])) {
231 // // reinsert la clause dans la liste des clauses surveillees
232 // voc.watch(p, this);
233 // return true;
234 // }
235
236 // Recherche un nouveau litt???ral ??? regarder
237 for (int i = 2; i < mylits.length; i++) {
238 if (!voc.isFalsified(mylits[i])) {
239 mylits[1] = mylits[i];
240 mylits[i] = p ^ 1;
241 voc.watch(mylits[1] ^ 1, this);
242 return true;
243 }
244 }
245 assert voc.isFalsified(mylits[1]);
246 // La clause est unitaire ou nulle
247 voc.watch(p, this);
248 // avance pour la propagation
249 return s.enqueue(mylits[0], this);
250 }
251
252 /*
253 * For learnt clauses only @author leberre
254 */
255 public boolean locked() {
256 return voc.getReason(lits[0]) == this;
257 }
258
259 /**
260 * @return the activity of the clause
261 */
262 public double getActivity() {
263 return activity;
264 }
265
266 @Override
267 public String toString() {
268 StringBuffer stb = new StringBuffer();
269 for (int i = 0; i < lits.length; i++) {
270 stb.append(Lits.toString(lits[i]));
271 stb.append("["); //$NON-NLS-1$
272 stb.append(voc.valueToString(lits[i]));
273 stb.append("]"); //$NON-NLS-1$
274 stb.append(" "); //$NON-NLS-1$
275 }
276 return stb.toString();
277 }
278
279 /**
280 * Retourne le ieme literal de la clause. Attention, cet ordre change durant
281 * la recherche.
282 *
283 * @param i
284 * the index of the literal
285 * @return the literal
286 */
287 public int get(int i) {
288 return lits[i];
289 }
290
291 /**
292 * @param claInc
293 */
294 public void incActivity(double claInc) {
295 activity += claInc;
296 }
297
298 /**
299 * @param d
300 */
301 public void rescaleBy(double d) {
302 activity *= d;
303 }
304
305 public int size() {
306 return lits.length;
307 }
308
309 public void assertConstraint(UnitPropagationListener s) {
310 boolean ret = s.enqueue(lits[0], this);
311 assert ret;
312 }
313
314 public ILits getVocabulary() {
315 return voc;
316 }
317
318 public int[] getLits() {
319 int[] tmp = new int[size()];
320 System.arraycopy(lits, 0, tmp, 0, size());
321 return tmp;
322 }
323
324 }