1 |
| package org.sat4j.reader.csp; |
2 |
| |
3 |
| import java.util.HashMap; |
4 |
| import java.util.HashSet; |
5 |
| import java.util.Map; |
6 |
| import java.util.Set; |
7 |
| |
8 |
| import org.sat4j.core.VecInt; |
9 |
| import org.sat4j.specs.ContradictionException; |
10 |
| import org.sat4j.specs.ISolver; |
11 |
| import org.sat4j.specs.IVecInt; |
12 |
| |
13 |
| public class SupportsGeneralizedACEncoding extends SupportsDirectEncoding { |
14 |
| |
15 |
0
| public SupportsGeneralizedACEncoding(int[] domains, int nbtuples) {
|
16 |
0
| super(domains, nbtuples);
|
17 |
| } |
18 |
| |
19 |
0
| @Override
|
20 |
| public void toClause(ISolver solver, Var[] vars) |
21 |
| throws ContradictionException { |
22 |
0
| Map<Set<Integer>, IVecInt> supports = new HashMap<Set<Integer>, IVecInt>();
|
23 |
0
| int[] acc = new int[vars.length];
|
24 |
0
| fill(0, vars, acc, supports);
|
25 |
| |
26 |
0
| for (int[] tuple : tuples) {
|
27 |
0
| for (int i = 0; i < tuple.length; i++) {
|
28 |
0
| Set<Integer> set = new HashSet<Integer>();
|
29 |
0
| for (int j = 0; j < tuple.length; j++) {
|
30 |
0
| if (i != j) {
|
31 |
0
| set.add(vars[j].translate(tuple[j]));
|
32 |
| } |
33 |
| } |
34 |
0
| IVecInt support = supports.get(set);
|
35 |
| assert support!=null; |
36 |
0
| support.push(vars[i].translate(tuple[i]));
|
37 |
| } |
38 |
| } |
39 |
| |
40 |
0
| IVecInt clause = new VecInt();
|
41 |
0
| for (Map.Entry<Set<Integer>, IVecInt> entry : supports.entrySet()) {
|
42 |
0
| clause.clear();
|
43 |
| |
44 |
0
| for (int p : entry.getKey())
|
45 |
0
| clause.push(-p);
|
46 |
0
| for (int i : entry.getValue())
|
47 |
0
| clause.push(i);
|
48 |
0
| solver.addClause(clause);
|
49 |
| } |
50 |
| } |
51 |
| |
52 |
0
| private void fill(int n, Var[] vars, int[] acc,
|
53 |
| Map<Set<Integer>, IVecInt> supports) { |
54 |
0
| if (n == vars.length) {
|
55 |
0
| for (int j = 0; j < acc.length; j++) {
|
56 |
0
| Set<Integer> set = new HashSet<Integer>();
|
57 |
0
| for (int i = 0; i < acc.length; i++)
|
58 |
0
| if (i != j)
|
59 |
0
| set.add(vars[i].translate(acc[i]));
|
60 |
0
| supports.put(set, new VecInt());
|
61 |
| } |
62 |
| } else |
63 |
0
| for (int i : vars[n].domain()) {
|
64 |
0
| acc[n] = i;
|
65 |
0
| fill(n + 1, vars, acc, supports);
|
66 |
| } |
67 |
| |
68 |
| } |
69 |
| } |