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