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 package org.sat4j.minisat.constraints.pb;
26
27 import java.math.BigInteger;
28 import java.util.HashMap;
29 import java.util.Map;
30
31 import org.sat4j.minisat.core.ILits;
32
33 public class ConflictMapClause extends ConflictMap {
34
35 public ConflictMapClause(Map<Integer, BigInteger> m, BigInteger d,
36 ILits voc, int level) {
37 super(m, d, voc, level);
38 }
39
40 public static IConflict createConflict(PBConstr cpb, int level) {
41 Map<Integer, BigInteger> m = new HashMap<Integer, BigInteger>();
42 int lit;
43 BigInteger coefLit;
44 for (int i = 0; i < cpb.size(); i++) {
45 lit = cpb.get(i);
46 coefLit = cpb.getCoef(i);
47 assert cpb.get(i) != 0;
48 assert cpb.getCoef(i).signum() > 0;
49 m.put(lit, coefLit);
50 }
51 return new ConflictMapClause(m, cpb.getDegree(), cpb.getVocabulary(),
52 level);
53 }
54
55 /**
56 * reduces the constraint defined by wpb until the result of the cutting
57 * plane is a conflict. this reduction returns a clause.
58 *
59 * @param litImplied
60 * @param ind
61 * @param reducedCoefs
62 * @param wpb
63 * @return BigInteger.ONE
64 */
65 @Override
66 protected BigInteger reduceUntilConflict(int litImplied, int ind,
67 BigInteger[] reducedCoefs, WatchPb wpb) {
68 for (int i = 0; i < reducedCoefs.length; i++)
69 if (i == ind || wpb.getVocabulary().isFalsified(wpb.get(i)))
70 reducedCoefs[i] = BigInteger.ONE;
71 else
72 reducedCoefs[i] = BigInteger.ZERO;
73 coefMultCons = coefs.get(litImplied ^ 1);
74 coefMult = BigInteger.ONE;
75 return BigInteger.ONE;
76 }
77 }