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.pb;
27
28 import java.math.BigInteger;
29
30 import org.sat4j.core.Vec;
31 import org.sat4j.core.VecInt;
32 import org.sat4j.minisat.core.ILits;
33 import org.sat4j.minisat.core.UnitPropagationListener;
34 import org.sat4j.specs.ContradictionException;
35 import org.sat4j.specs.IVec;
36 import org.sat4j.specs.IVecInt;
37
38 public class PuebloMinWatchPb extends MinWatchPb {
39
40 private static final long serialVersionUID = 1L;
41
42 /**
43 * Constructeur de base des contraintes
44 *
45 * @param voc
46 * Informations sur le vocabulaire employ???
47 * @param ps
48 * Liste des litt???raux
49 * @param coefs
50 * Liste des coefficients
51 * @param moreThan
52 * Indication sur le comparateur
53 * @param degree
54 * Stockage du degr??? de la contrainte
55 */
56 private PuebloMinWatchPb(ILits voc, IDataStructurePB mpb) {
57
58 super(voc, mpb);
59 }
60
61 /**
62 * @param s
63 * outil pour la propagation des litt???raux
64 * @param ps
65 * liste des litt???raux de la nouvelle contrainte
66 * @param coefs
67 * liste des coefficients des litt???raux de la contrainte
68 * @param moreThan
69 * d???termine si c'est une sup???rieure ou ???gal ??? l'origine
70 * @param degree
71 * fournit le degr??? de la contrainte
72 * @return une nouvelle clause si tout va bien, ou null si un conflit est
73 * d???tect???
74 */
75 public static PuebloMinWatchPb minWatchPbNew(UnitPropagationListener s,
76 ILits voc, IVecInt ps, IVecInt coefs, boolean moreThan, int degree)
77 throws ContradictionException {
78 return minWatchPbNew(s, voc, ps, toVecBigInt(coefs), moreThan,
79 toBigInt(degree));
80 }
81
82 /**
83 * @param s
84 * outil pour la propagation des litt???raux
85 * @param ps
86 * liste des litt???raux de la nouvelle contrainte
87 * @param coefs
88 * liste des coefficients des litt???raux de la contrainte
89 * @param moreThan
90 * d???termine si c'est une sup???rieure ou ???gal ??? l'origine
91 * @param degree
92 * fournit le degr??? de la contrainte
93 * @return une nouvelle clause si tout va bien, ou null si un conflit est
94 * d???tect???
95 */
96 public static PuebloMinWatchPb minWatchPbNew(UnitPropagationListener s,
97 ILits voc, IVecInt ps, IVec<BigInteger> coefs, boolean moreThan,
98 BigInteger degree) throws ContradictionException {
99 // Il ne faut pas modifier les param?tres
100 VecInt litsVec = new VecInt(ps.size());
101 IVec<BigInteger> coefsVec = new Vec<BigInteger>(coefs.size());
102 ps.copyTo(litsVec);
103 coefs.copyTo(coefsVec);
104
105 // Ajouter les simplifications quand la structure sera d???finitive
106 IDataStructurePB mpb = niceParameters(litsVec, coefsVec, moreThan,
107 degree, voc);
108 PuebloMinWatchPb outclause = new PuebloMinWatchPb(voc, mpb);
109
110 if (outclause.degree.signum() <= 0) {
111 return null;
112 }
113
114 outclause.computeWatches();
115
116 outclause.computePropagation(s);
117
118 return outclause;
119
120 }
121
122 public static PuebloMinWatchPb minWatchPbNew(UnitPropagationListener s,
123 ILits voc, IDataStructurePB mpb) throws ContradictionException {
124 PuebloMinWatchPb outclause = new PuebloMinWatchPb(voc, mpb);
125
126 if (outclause.degree.signum() <= 0) {
127 return null;
128 }
129
130 outclause.computeWatches();
131
132 outclause.computePropagation(s);
133
134 return outclause;
135
136 }
137
138 /**
139 *
140 */
141 public static WatchPb watchPbNew(ILits voc, IVecInt lits, IVecInt coefs,
142 boolean moreThan, int degree) {
143 return watchPbNew(voc, lits, toVecBigInt(coefs), moreThan,
144 toBigInt(degree));
145 }
146
147 /**
148 *
149 */
150 public static WatchPb watchPbNew(ILits voc, IVecInt lits,
151 IVec<BigInteger> coefs, boolean moreThan, BigInteger degree) {
152 IDataStructurePB mpb = null;
153 mpb = niceCheckedParameters(lits, coefs, moreThan, degree, voc);
154 return new PuebloMinWatchPb(voc, mpb);
155 }
156
157 public static WatchPb normalizedWatchPbNew(ILits voc, IDataStructurePB mpb) {
158 return new PuebloMinWatchPb(voc, mpb);
159 }
160
161 @Override
162 protected BigInteger maximalCoefficient(int pIndice) {
163 return coefs[0];
164 }
165
166 @Override
167 protected BigInteger updateWatched(BigInteger mc, int pIndice) {
168 BigInteger maxCoef = mc;
169 if (watchingCount < size()) {
170 BigInteger upWatchCumul = watchCumul.subtract(coefs[pIndice]);
171 BigInteger borneSup = degree.add(maxCoef);
172 for (int ind = 0; ind < lits.length
173 && upWatchCumul.compareTo(borneSup) < 0; ind++) {
174 if (!voc.isFalsified(lits[ind]) && !watched[ind]) {
175 upWatchCumul = upWatchCumul.add(coefs[ind]);
176 watched[ind] = true;
177 assert watchingCount < size();
178 watching[watchingCount++] = ind;
179 voc.watch(lits[ind] ^ 1, this);
180 }
181 }
182 watchCumul = upWatchCumul.add(coefs[pIndice]);
183 }
184 return maxCoef;
185 }
186
187 }