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