blob: 22f480fac07d40f0d3afcf46a027de8d2cc046ec (
plain)
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
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
|
package jrummikub.ai.fdsolver.constraint;
import java.util.ArrayList;
import java.util.Collection;
import java.util.Collections;
import java.util.Comparator;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Set;
import jrummikub.ai.fdsolver.Constraint;
import jrummikub.ai.fdsolver.Propagator;
import jrummikub.ai.fdsolver.Satisfiability;
import jrummikub.ai.fdsolver.Var;
public class ListSumConstraint extends Constraint {
Var<Integer> sum;
List<Var<Integer>> list;
List<Var<?>> vars = new ArrayList<Var<?>>();
public ListSumConstraint(Var<Integer> sum, List<Var<Integer>> list) {
this.sum = sum;
this.list = list;
vars.add(sum);
vars.addAll(list);
}
@Override
public Collection<Var<?>> getWatchedVars() {
return vars;
}
@Override
public Collection<Propagator> getPropagators(boolean negate) {
return Collections.emptyList();
}
@Override
public Satisfiability getSatisfiability() {
List<Integer> values = new ArrayList<Integer>();
int valueSum = 0;
boolean isTaut = sum.getRange().size()==1;
for (Var<Integer> var : list) {
Iterator<Integer> it = var.getRange().iterator();
int value = it.next();
if (it.hasNext())
isTaut = false;
values.add(value);
valueSum += value;
}
if (isTaut) {
if (valueSum == sum.getValue()) {
return Satisfiability.TAUT;
} else {
return Satisfiability.UNSAT;
}
}
Set<Integer> reachableValues = new HashSet<Integer>();
Set<Integer> newValues = new HashSet<Integer>();
reachableValues.add(valueSum);
if (sum.getRange().contains(valueSum)) {
return Satisfiability.SAT;
}
for (int i = 0; i < values.size(); i++) {
Var<Integer> var = list.get(i);
int offset = values.get(i);
for (int x : var.getRange()) {
if (x == offset)
continue;
newValues.clear();
for (int y : reachableValues) {
int newValue = x + y - offset;
if (!reachableValues.contains(newValue)) {
newValues.add(x + y - offset);
}
}
if (!Collections.disjoint(sum.getRange(), newValues)) {
return Satisfiability.SAT;
}
reachableValues.addAll(newValues);
}
}
return Satisfiability.UNSAT;
}
}
|
