summaryrefslogtreecommitdiffstats
path: root/src/jrummikub/ai/fdsolver
diff options
context:
space:
mode:
Diffstat (limited to 'src/jrummikub/ai/fdsolver')
-rw-r--r--src/jrummikub/ai/fdsolver/Constraints.java5
-rw-r--r--src/jrummikub/ai/fdsolver/Var.java3
-rw-r--r--src/jrummikub/ai/fdsolver/constraint/ListSumConstraint.java91
3 files changed, 99 insertions, 0 deletions
diff --git a/src/jrummikub/ai/fdsolver/Constraints.java b/src/jrummikub/ai/fdsolver/Constraints.java
index 0885d2a..caa8cfa 100644
--- a/src/jrummikub/ai/fdsolver/Constraints.java
+++ b/src/jrummikub/ai/fdsolver/Constraints.java
@@ -7,6 +7,7 @@ import jrummikub.ai.fdsolver.constraint.FilterConstraint;
import jrummikub.ai.fdsolver.constraint.IfConstraint;
import jrummikub.ai.fdsolver.constraint.IndexConstraint;
import jrummikub.ai.fdsolver.constraint.LessThan;
+import jrummikub.ai.fdsolver.constraint.ListSumConstraint;
import jrummikub.ai.fdsolver.constraint.OffsetConstraint;
import jrummikub.ai.fdsolver.constraint.SameConstraint;
import jrummikub.ai.fdsolver.constraint.SumConstraint;
@@ -46,6 +47,10 @@ public class Constraints {
return new SumConstraint(x, y, z);
}
+ public static Constraint sum(Var<Integer> sum, List<Var<Integer>> list) {
+ return new ListSumConstraint(sum, list);
+ }
+
public static <T extends Comparable<T>> Constraint lessThan(Var<T> x, Var<T> y) {
return new LessThan<T>(false, x, y);
}
diff --git a/src/jrummikub/ai/fdsolver/Var.java b/src/jrummikub/ai/fdsolver/Var.java
index a454487..e885cef 100644
--- a/src/jrummikub/ai/fdsolver/Var.java
+++ b/src/jrummikub/ai/fdsolver/Var.java
@@ -42,6 +42,9 @@ public class Var<T> implements Comparable<Var<T>> {
range.remove(value);
solver.logInvalidation(this, value);
makeDirty();
+ if (range.size() == 0) {
+ solver.contradiction = true;
+ }
}
HashSet<Constraint> getConstraints() {
diff --git a/src/jrummikub/ai/fdsolver/constraint/ListSumConstraint.java b/src/jrummikub/ai/fdsolver/constraint/ListSumConstraint.java
new file mode 100644
index 0000000..22f480f
--- /dev/null
+++ b/src/jrummikub/ai/fdsolver/constraint/ListSumConstraint.java
@@ -0,0 +1,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;
+ }
+
+}