1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28 package org.sat4j.pb.constraints.pb;
29
30 import java.math.BigInteger;
31
32 import org.sat4j.minisat.constraints.cnf.Lits;
33 import org.sat4j.minisat.core.VarActivityListener;
34 import org.sat4j.specs.IVec;
35 import org.sat4j.specs.IVecInt;
36
37
38
39
40
41 public class MapPb implements IDataStructurePB {
42
43
44
45
46
47
48 protected InternalMapPBStructure weightedLits;
49
50 protected BigInteger degree;
51
52 protected int assertiveLiteral = -1;
53
54 MapPb(PBConstr cpb) {
55 weightedLits = new InternalMapPBStructure(cpb);
56 degree = cpb.getDegree();
57 }
58
59 MapPb(int size) {
60 weightedLits = new InternalMapPBStructure(size);
61 degree = BigInteger.ZERO;
62 }
63
64 public boolean isCardinality() {
65 for (int i = 0; i < size(); i++)
66 if (!(weightedLits.getCoef(i).equals(BigInteger.ONE)))
67 return false;
68 return true;
69 }
70
71 public boolean isLongSufficient() {
72 BigInteger som = BigInteger.ZERO;
73 for (int i = 0; i < size() && som.bitLength() < Long.SIZE; i++) {
74 assert weightedLits.getCoef(i).compareTo(BigInteger.ZERO) >= 0;
75 som = som.add(weightedLits.getCoef(i));
76 }
77 return som.bitLength() < Long.SIZE;
78 }
79
80 public int getAssertiveLiteral() {
81 return assertiveLiteral;
82 }
83
84 public BigInteger saturation() {
85 assert degree.signum() > 0;
86 BigInteger minimum = degree;
87 for (int ind = 0; ind < size(); ind++) {
88 assert weightedLits.getCoef(ind).signum() > 0;
89 if (degree.compareTo(weightedLits.getCoef(ind)) < 0)
90 changeCoef(ind, degree);
91 assert weightedLits.getCoef(ind).signum() > 0;
92 minimum = minimum.min(weightedLits.getCoef(ind));
93 }
94
95 if (minimum.equals(degree) && minimum.compareTo(BigInteger.ONE) > 0) {
96 degree = BigInteger.ONE;
97 for (int ind = 0; ind < size(); ind++)
98 changeCoef(ind, BigInteger.ONE);
99 }
100
101 return degree;
102 }
103
104 public BigInteger cuttingPlane(PBConstr cpb, BigInteger deg,
105 BigInteger[] reducedCoefs, VarActivityListener val) {
106 return cuttingPlane(cpb, deg, reducedCoefs, BigInteger.ONE, val);
107 }
108
109 public BigInteger cuttingPlane(PBConstr cpb, BigInteger degreeCons,
110 BigInteger[] reducedCoefs, BigInteger coefMult,
111 VarActivityListener val) {
112 degree = degree.add(degreeCons);
113 assert degree.signum() > 0;
114
115 if (reducedCoefs == null)
116 for (int i = 0; i < cpb.size(); i++) {
117 val.varBumpActivity(cpb.get(i));
118 cuttingPlaneStep(cpb.get(i), multiplyCoefficient(
119 cpb.getCoef(i), coefMult));
120 }
121 else
122 for (int i = 0; i < cpb.size(); i++) {
123 val.varBumpActivity(cpb.get(i));
124 cuttingPlaneStep(cpb.get(i), multiplyCoefficient(
125 reducedCoefs[i], coefMult));
126 }
127
128 return degree;
129 }
130
131 public BigInteger cuttingPlane(int[] lits, BigInteger[] reducedCoefs,
132 BigInteger deg) {
133 return cuttingPlane(lits, reducedCoefs, deg, BigInteger.ONE);
134 }
135
136 public BigInteger cuttingPlane(int lits[], BigInteger[] reducedCoefs,
137 BigInteger degreeCons, BigInteger coefMult) {
138 degree = degree.add(degreeCons);
139 assert degree.signum() > 0;
140
141 for (int i = 0; i < lits.length; i++)
142 cuttingPlaneStep(lits[i], reducedCoefs[i].multiply(coefMult));
143
144 return degree;
145 }
146
147 private void cuttingPlaneStep(final int lit, final BigInteger coef) {
148 assert coef.signum() >= 0;
149 int nlit = lit ^ 1;
150 if (coef.signum() > 0) {
151 if (weightedLits.containsKey(nlit)) {
152 assert !weightedLits.containsKey(lit);
153 assert weightedLits.get(nlit) != null;
154 if (weightedLits.get(nlit).compareTo(coef) < 0) {
155 BigInteger tmp = weightedLits.get(nlit);
156 setCoef(lit, coef.subtract(tmp));
157 assert weightedLits.get(lit).signum() > 0;
158 degree = degree.subtract(tmp);
159 removeCoef(nlit);
160 } else {
161 if (weightedLits.get(nlit).equals(coef)) {
162 degree = degree.subtract(coef);
163 removeCoef(nlit);
164 } else {
165 decreaseCoef(nlit, coef);
166 assert weightedLits.get(nlit).signum() > 0;
167 degree = degree.subtract(coef);
168 }
169 }
170 } else {
171 assert (!weightedLits.containsKey(lit))
172 || (weightedLits.get(lit).signum() > 0);
173 if (weightedLits.containsKey(lit))
174 increaseCoef(lit, coef);
175 else
176 setCoef(lit, coef);
177 assert weightedLits.get(lit).signum() > 0;
178 }
179 }
180 assert (!weightedLits.containsKey(nlit))
181 || (!weightedLits.containsKey(lit));
182 }
183
184 public void buildConstraintFromConflict(IVecInt resLits,
185 IVec<BigInteger> resCoefs) {
186 resLits.clear();
187 resCoefs.clear();
188 weightedLits.copyCoefs(resCoefs);
189 weightedLits.copyLits(resLits);
190 };
191
192 public void buildConstraintFromMapPb(int[] resLits, BigInteger[] resCoefs) {
193
194 assert resLits.length == resCoefs.length;
195 assert resLits.length == size();
196 weightedLits.copyCoefs(resCoefs);
197 weightedLits.copyLits(resLits);
198 };
199
200 public BigInteger getDegree() {
201 return degree;
202 }
203
204 public int size() {
205 return weightedLits.size();
206 }
207
208
209
210
211
212
213 @Override
214 public String toString() {
215 StringBuffer stb = new StringBuffer();
216 for (int ind = 0; ind < size(); ind++) {
217 stb.append(weightedLits.getCoef(ind));
218 stb.append(".");
219 stb.append(Lits.toString(weightedLits.getLit(ind)));
220 stb.append(" ");
221 }
222 return stb.toString() + " >= " + degree;
223 }
224
225 private BigInteger multiplyCoefficient(BigInteger coef, BigInteger mult) {
226 if (coef.equals(BigInteger.ONE))
227 return mult;
228 return coef.multiply(mult);
229 }
230
231 void increaseCoef(int lit, BigInteger incCoef) {
232 weightedLits.put(lit, weightedLits.get(lit).add(incCoef));
233 }
234
235 void decreaseCoef(int lit, BigInteger decCoef) {
236 weightedLits.put(lit, weightedLits.get(lit).subtract(decCoef));
237 }
238
239 void setCoef(int lit, BigInteger newValue) {
240 weightedLits.put(lit, newValue);
241 }
242
243 void changeCoef(int indLit, BigInteger newValue) {
244 weightedLits.changeCoef(indLit, newValue);
245 }
246
247 void removeCoef(int lit) {
248 weightedLits.remove(lit);
249 }
250
251 }