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