diff options
Diffstat (limited to 'src/jrummikub/ai/fdsolver')
-rw-r--r-- | src/jrummikub/ai/fdsolver/Constraints.java | 5 | ||||
-rw-r--r-- | src/jrummikub/ai/fdsolver/Var.java | 3 | ||||
-rw-r--r-- | src/jrummikub/ai/fdsolver/constraint/ListSumConstraint.java | 91 |
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; + } + +} |