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
31 package org.sat4j.tools.encoding;
32
33 import java.util.ArrayList;
34 import java.util.HashMap;
35
36 import org.sat4j.core.ConstrGroup;
37 import org.sat4j.core.VecInt;
38 import org.sat4j.specs.ContradictionException;
39 import org.sat4j.specs.IConstr;
40 import org.sat4j.specs.ISolver;
41 import org.sat4j.specs.IVecInt;
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58 public class Product extends EncodingStrategyAdapter {
59
60 public IConstr addAtMostNonOpt(ISolver solver, IVecInt literals, int k)
61 throws ContradictionException {
62
63 ConstrGroup group = new ConstrGroup();
64
65 IVecInt clause = new VecInt();
66
67 final int n = literals.size();
68
69 if (k > n) {
70 return group;
71 }
72 if (n == k + 1) {
73 for (int i = 0; i < n; i++) {
74 clause.push(-literals.get(i));
75 }
76 group.add(solver.addClause(clause));
77 clause.clear();
78 return group;
79 }
80 if (n < 7) {
81 Binomial binomial = new Binomial();
82
83 return binomial.addAtMost(solver, literals, k);
84 }
85
86 final int p = (int) Math.ceil(Math.pow(n, 1 / (double) (k + 1)));
87
88 int[][] a = new int[n][k + 1];
89 int[] result;
90
91
92
93
94
95
96
97 result = decompositionBase10VersBaseP(0, p, k + 1);
98 a[0] = result;
99 ArrayList<Integer> dejaPris = new ArrayList<Integer>();
100 dejaPris.add(0);
101 int tmp = 1;
102 for (int i = 1; i <= k + 1; i++) {
103 a[i] = decompositionBase10VersBaseP(tmp, p, k + 1);
104 dejaPris.add(tmp);
105 tmp = tmp * p;
106 }
107 tmp = 2;
108 for (int i = k + 2; i < n; i++) {
109 while (dejaPris.contains(tmp)) {
110 tmp++;
111 }
112 a[i] = decompositionBase10VersBaseP(tmp, p, k + 1);
113 tmp++;
114 }
115
116 ArrayList<Integer>[] hashTupleSetTable = new ArrayList[k + 1];
117
118 int[][][] aWithoutD = new int[n][k + 1][k];
119
120 int hash;
121 HashMap<Integer, Integer>[] ady = new HashMap[k + 1];
122 VecInt[] adxd = new VecInt[k + 1];
123 int varId;
124
125 for (int d = 0; d < k + 1; d++) {
126 hashTupleSetTable[d] = new ArrayList<Integer>();
127 ady[d] = new HashMap<Integer, Integer>();
128 adxd[d] = new VecInt();
129 for (int i = 0; i < n; i++) {
130 for (int j = 0; j < k; j++) {
131 if (j < d) {
132 aWithoutD[i][d][j] = a[i][j];
133 } else {
134 aWithoutD[i][d][j] = a[i][j + 1];
135 }
136 }
137 hash = recompositionBase10DepuisBaseP(aWithoutD[i][d], p);
138 if (!hashTupleSetTable[d].contains(new Integer(hash))) {
139 hashTupleSetTable[d].add(new Integer(hash));
140 varId = solver.nextFreeVarId(true);
141 ady[d].put(hash, varId);
142 adxd[d].push(varId);
143 }
144 }
145 }
146
147 for (int d = 0; d < k + 1; d++) {
148 for (int i = 0; i < n; i++) {
149 clause.push(-literals.get(i));
150 clause.push(ady[d].get(recompositionBase10DepuisBaseP(
151 aWithoutD[i][d], p)));
152 group.add(solver.addClause(clause));
153 clause.clear();
154 }
155 group.add(addAtMost(solver, adxd[d], k));
156 }
157
158 return group;
159 }
160
161 @Override
162 public IConstr addAtMost(ISolver solver, IVecInt literals, int k)
163 throws ContradictionException {
164 return super.addAtMost(solver, literals, k);
165 }
166
167 @Override
168 public IConstr addAtMostOne(ISolver solver, IVecInt literals)
169 throws ContradictionException {
170
171 ConstrGroup group = new ConstrGroup(false);
172
173 IVecInt clause = new VecInt();
174
175 final int n = literals.size();
176
177 if (n < 7) {
178 Binomial binomial = new Binomial();
179 return binomial.addAtMostOne(solver, literals);
180 }
181
182 final int p = (int) Math.ceil(Math.sqrt(n));
183 final int q = (int) Math.ceil((double) n / (double) p);
184
185 int[] u = new int[p];
186 int[] v = new int[q];
187
188 for (int i = 0; i < p; i++) {
189 u[i] = solver.nextFreeVarId(true);
190 }
191 for (int i = 0; i < q; i++) {
192 v[i] = solver.nextFreeVarId(true);
193 }
194
195 int cpt = 0;
196 for (int i = 0; i < p; i++) {
197 for (int j = 0; j < q; j++) {
198 if (cpt < n) {
199 clause.push(-literals.get(cpt));
200 clause.push(u[i]);
201 group.add(solver.addClause(clause));
202 clause.clear();
203 clause.push(-literals.get(cpt));
204 clause.push(v[j]);
205 group.add(solver.addClause(clause));
206 clause.clear();
207 cpt++;
208 }
209 }
210 }
211
212 group.add(addAtMostOne(solver, new VecInt(u)));
213 group.add(addAtMostOne(solver, new VecInt(v)));
214 return group;
215 }
216
217 private int[] decompositionBase10VersBaseP(int n, int p, int nbBits) {
218 int[] result = new int[nbBits];
219
220 int reste;
221 int pow;
222 int quotient;
223 reste = n;
224 for (int j = 0; j < nbBits - 1; j++) {
225 pow = (int) Math.pow(p, nbBits - j - 1);
226 quotient = reste / pow;
227 result[j] = quotient + 1;
228 reste = reste - quotient * pow;
229 }
230 result[nbBits - 1] = reste + 1;
231 return result;
232 }
233
234 private int recompositionBase10DepuisBaseP(int[] tab, int p) {
235 int result = 0;
236 for (int i = 0; i < tab.length - 1; i++) {
237 result = (result + tab[i] - 1) * p;
238 }
239 result += tab[tab.length - 1] - 1;
240 return result;
241 }
242
243 @Override
244 public IConstr addAtLeast(ISolver solver, IVecInt literals, int k)
245 throws ContradictionException {
246
247 IVecInt newLits = new VecInt();
248 for (int i = 0; i < literals.size(); i++) {
249 newLits.push(-literals.get(i));
250 }
251
252 return addAtMost(solver, newLits, literals.size() - k);
253 }
254
255 @Override
256 public IConstr addExactlyOne(ISolver solver, IVecInt literals)
257 throws ContradictionException {
258 ConstrGroup group = new ConstrGroup();
259
260 group.add(addAtLeastOne(solver, literals));
261 group.add(addAtMostOne(solver, literals));
262
263 return group;
264 }
265
266 @Override
267 public IConstr addExactly(ISolver solver, IVecInt literals, int degree)
268 throws ContradictionException {
269 ConstrGroup group = new ConstrGroup();
270
271 group.add(addAtLeast(solver, literals, degree));
272 group.add(addAtMost(solver, literals, degree));
273
274 return group;
275 }
276
277 }