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