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