1 |
| |
2 |
| |
3 |
| |
4 |
| |
5 |
| |
6 |
| |
7 |
| package org.sat4j.minisat.constraints.pb; |
8 |
| |
9 |
| import java.math.BigInteger; |
10 |
| import java.util.Map; |
11 |
| |
12 |
| import org.sat4j.minisat.core.ILits; |
13 |
| |
14 |
| |
15 |
| |
16 |
| |
17 |
| |
18 |
| class Conflict extends MapPb { |
19 |
| |
20 |
| private ILits voc; |
21 |
| |
22 |
62490
| Conflict(Map<Integer, BigInteger> m, BigInteger d, ILits voc) {
|
23 |
62490
| super(m, d);
|
24 |
62490
| this.voc = voc;
|
25 |
| } |
26 |
| |
27 |
| private BigInteger coefMult = BigInteger.ZERO; |
28 |
| |
29 |
| private BigInteger coefMultCons = BigInteger.ZERO; |
30 |
| |
31 |
| |
32 |
| |
33 |
| |
34 |
| |
35 |
| |
36 |
| |
37 |
| |
38 |
| |
39 |
| |
40 |
2584713
| BigInteger resolve(WatchPb wpb, int litImplied) {
|
41 |
| assert litImplied > 1; |
42 |
2584713
| if (!coefs.containsKey(litImplied ^ 1)) {
|
43 |
| |
44 |
2004691
| return degree;
|
45 |
| } |
46 |
| |
47 |
| assert slackConflict().signum() <= 0; |
48 |
| assert degree.signum() >= 0; |
49 |
| |
50 |
| |
51 |
| |
52 |
580022
| BigInteger[] coefsCons = wpb.getCoefs();
|
53 |
580022
| BigInteger degreeCons = wpb.getDegree();
|
54 |
580022
| int[] litsCons = wpb.getLits();
|
55 |
| |
56 |
580022
| for (int i = 0; i < coefsCons.length; i++)
|
57 |
| assert coefsCons[i].signum() > 0; |
58 |
| |
59 |
| |
60 |
580022
| int ind = -1;
|
61 |
580022
| while (litsCons[++ind] != litImplied)
|
62 |
| ; |
63 |
| |
64 |
| assert litsCons[ind] == litImplied; |
65 |
| assert coefsCons[ind] != BigInteger.ZERO; |
66 |
| |
67 |
| |
68 |
580022
| degreeCons = reduceUntilConflict(litImplied, ind, litsCons, coefsCons,
|
69 |
| degreeCons, wpb); |
70 |
| |
71 |
| |
72 |
| |
73 |
580022
| degreeCons = (degreeCons.multiply(coefMultCons));
|
74 |
580022
| degree = degree.multiply(coefMult);
|
75 |
| |
76 |
580022
| if (coefMult.compareTo(BigInteger.ONE) > 0) {
|
77 |
941
| for (Integer i : coefs.keySet()) {
|
78 |
92386
| coefs.put(i, coefs.get(i).multiply(coefMult));
|
79 |
| } |
80 |
| } |
81 |
| |
82 |
| |
83 |
| |
84 |
580022
| degree = addCoeffNewConstraint(litsCons, coefsCons, degreeCons,
|
85 |
| coefMultCons); |
86 |
| assert !coefs.containsKey(litImplied); |
87 |
| assert !coefs.containsKey(litImplied ^ 1); |
88 |
| assert degree.signum() > 0; |
89 |
| |
90 |
| |
91 |
580022
| degree = saturation();
|
92 |
| assert slackConflict().signum() <= 0; |
93 |
| |
94 |
580022
| return degree;
|
95 |
| } |
96 |
| |
97 |
580022
| private BigInteger reduceUntilConflict(int litImplied, int ind, int[] lits,
|
98 |
| BigInteger[] coefsBis, BigInteger degreeBis, WatchPb wpb) { |
99 |
580022
| BigInteger slackResolve = BigInteger.ONE.negate();
|
100 |
580022
| BigInteger slackThis = BigInteger.ZERO;
|
101 |
580022
| BigInteger slackIndex = BigInteger.ZERO;
|
102 |
580022
| BigInteger ppcm;
|
103 |
| |
104 |
580022
| int cpt = -1;
|
105 |
| |
106 |
580022
| do {
|
107 |
708558
| cpt++;
|
108 |
| |
109 |
708558
| if (slackResolve.signum() >= 0) {
|
110 |
| assert slackThis.signum() > 0; |
111 |
| |
112 |
128536
| BigInteger tmp = reduceInConstraint(coefsBis, lits, ind,
|
113 |
| degreeBis); |
114 |
| assert ((tmp.compareTo(degreeBis) < 0) && (tmp |
115 |
| .compareTo(BigInteger.ONE) >= 0)); |
116 |
128536
| degreeBis = tmp;
|
117 |
| } |
118 |
| |
119 |
| assert coefs.get(litImplied ^ 1).signum() > 0; |
120 |
| assert coefsBis[ind].signum() > 0; |
121 |
| |
122 |
708558
| ppcm = ppcm(coefsBis[ind], coefs.get(litImplied ^ 1));
|
123 |
| assert ppcm.signum() > 0; |
124 |
708558
| coefMult = ppcm.divide(coefs.get(litImplied ^ 1));
|
125 |
708558
| coefMultCons = ppcm.divide(coefsBis[ind]);
|
126 |
| |
127 |
| assert coefMultCons.signum() > 0; |
128 |
| assert coefMult.signum() > 0; |
129 |
| assert coefMult.multiply(coefs.get(litImplied ^ 1)).equals( |
130 |
| coefMultCons.multiply(coefsBis[ind])); |
131 |
| |
132 |
| |
133 |
708558
| slackThis = wpb.slackConstraint(coefsBis, degreeBis).multiply(
|
134 |
| coefMultCons); |
135 |
708558
| slackIndex = slackConflict().multiply(coefMult);
|
136 |
| |
137 |
| assert slackIndex.signum() <= 0; |
138 |
| |
139 |
| |
140 |
708558
| slackResolve = slackThis.add(slackIndex);
|
141 |
708558
| } while (slackResolve.signum() >= 0);
|
142 |
| assert coefMult.multiply(coefs.get(litImplied ^ 1)).equals( |
143 |
| coefMultCons.multiply(coefsBis[ind])); |
144 |
580022
| return degreeBis;
|
145 |
| |
146 |
| } |
147 |
| |
148 |
4515805
| BigInteger slackConflict() {
|
149 |
4515805
| BigInteger poss = BigInteger.ZERO;
|
150 |
| |
151 |
4515805
| for (Integer i : coefs.keySet())
|
152 |
176458914
| if (coefs.get(i).signum() != 0 && !voc.isFalsified(i))
|
153 |
33862751
| poss = poss.add(coefs.get(i));
|
154 |
4515805
| return poss.subtract(degree);
|
155 |
| } |
156 |
| |
157 |
62490
| BigInteger getDegree() {
|
158 |
62490
| return degree;
|
159 |
| } |
160 |
| |
161 |
2736485
| boolean isAssertive(int dl) {
|
162 |
2736485
| BigInteger slack = BigInteger.ZERO;
|
163 |
2736485
| for (Integer i : coefs.keySet()) {
|
164 |
117697405
| if ((coefs.get(i).signum() > 0)
|
165 |
| && (((!voc.isFalsified(i)) || voc.getLevel(i) >= dl))) |
166 |
41139465
| slack = slack.add(coefs.get(i));
|
167 |
| } |
168 |
2736485
| slack = slack.subtract(degree);
|
169 |
2736485
| if (slack.signum() < 0)
|
170 |
66548
| return false;
|
171 |
2669937
| for (Integer i : coefs.keySet()) {
|
172 |
75715148
| if ((coefs.get(i).signum() > 0)
|
173 |
| && (voc.isUnassigned(i) || voc.getLevel(i) >= dl) |
174 |
| && (slack.subtract(coefs.get(i)).signum() < 0)) |
175 |
124924
| return true;
|
176 |
| } |
177 |
2545013
| return false;
|
178 |
| } |
179 |
| |
180 |
| |
181 |
| |
182 |
| |
183 |
| |
184 |
| |
185 |
| |
186 |
| |
187 |
| |
188 |
| |
189 |
708558
| protected static BigInteger ppcm(BigInteger a, BigInteger b) {
|
190 |
708558
| return a.divide(a.gcd(b)).multiply(b);
|
191 |
| } |
192 |
| |
193 |
| |
194 |
| |
195 |
| |
196 |
| |
197 |
| |
198 |
| |
199 |
| |
200 |
| |
201 |
128536
| public BigInteger reduceInConstraint(final BigInteger[] coefsBis,
|
202 |
| final int[] lits, final int indLitImplied, |
203 |
| final BigInteger degreeBis) { |
204 |
| |
205 |
| assert degreeBis.compareTo(BigInteger.ONE) > 0; |
206 |
| |
207 |
128536
| int lit = -1;
|
208 |
128536
| for (int ind = 0; (ind < lits.length) && (lit == -1); ind++)
|
209 |
21597574
| if (coefsBis[ind].signum() != 0 && voc.isUnassigned(lits[ind])) {
|
210 |
| assert coefsBis[ind].compareTo(degreeBis) < 0; |
211 |
14007
| lit = ind;
|
212 |
| } |
213 |
| |
214 |
| |
215 |
128536
| if (lit == -1)
|
216 |
114529
| for (int ind = 0; (ind < lits.length) && (lit == -1); ind++)
|
217 |
12079065
| if ((coefsBis[ind].signum() != 0)
|
218 |
| && (voc.isSatisfied(lits[ind])) |
219 |
| && (ind != indLitImplied)) |
220 |
114529
| lit = ind;
|
221 |
| |
222 |
| |
223 |
| assert lit != -1; |
224 |
| |
225 |
| assert lit != indLitImplied; |
226 |
| |
227 |
| |
228 |
128536
| BigInteger degUpdate = degreeBis.subtract(coefsBis[lit]);
|
229 |
128536
| coefsBis[lit] = BigInteger.ZERO;
|
230 |
| |
231 |
| |
232 |
| assert degUpdate.signum() > 0; |
233 |
128536
| BigInteger minimum = degUpdate;
|
234 |
128536
| for (int i = 0; i < coefsBis.length; i++) {
|
235 |
22416900
| if (coefsBis[i].signum() > 0)
|
236 |
18517093
| minimum = minimum.min(coefsBis[i]);
|
237 |
22416900
| coefsBis[i] = degUpdate.min(coefsBis[i]);
|
238 |
| } |
239 |
128536
| if (minimum.equals(degUpdate) && !degUpdate.equals(BigInteger.ONE)) {
|
240 |
| |
241 |
| |
242 |
153
| degUpdate = BigInteger.ONE;
|
243 |
153
| for (int i = 0; i < coefsBis.length; i++)
|
244 |
29876
| if (coefsBis[i].signum() > 0)
|
245 |
21322
| coefsBis[i] = degUpdate;
|
246 |
| } |
247 |
| |
248 |
| assert coefsBis[indLitImplied].signum() > 0; |
249 |
| assert degreeBis.compareTo(degUpdate) > 0; |
250 |
128536
| return degUpdate;
|
251 |
| } |
252 |
| |
253 |
| } |