diff options
Diffstat (limited to 'src/jrummikub/ai/fdsolver/constraint')
5 files changed, 75 insertions, 50 deletions
diff --git a/src/jrummikub/ai/fdsolver/constraint/ComparatorConstraint.java b/src/jrummikub/ai/fdsolver/constraint/ComparatorConstraint.java index ab0edde..019de92 100644 --- a/src/jrummikub/ai/fdsolver/constraint/ComparatorConstraint.java +++ b/src/jrummikub/ai/fdsolver/constraint/ComparatorConstraint.java @@ -6,6 +6,7 @@ import java.util.Arrays; import java.util.Collection; import java.util.Collections; import java.util.Comparator; +import java.util.NoSuchElementException; import jrummikub.ai.fdsolver.Constraint; import jrummikub.ai.fdsolver.Propagator; @@ -17,8 +18,9 @@ public class ComparatorConstraint<T> extends Constraint { Comparator<T> comparator, reverseComparator; ComparatorPropagator<T> trueX, trueY, falseX, falseY; boolean allowEqual; - - ComparatorConstraint(final Comparator<T> comparator, boolean allowEqual, Var<T> x, Var<T> y) { + + ComparatorConstraint(final Comparator<T> comparator, boolean allowEqual, + Var<T> x, Var<T> y) { this.x = x; this.y = y; this.comparator = comparator; @@ -31,37 +33,42 @@ public class ComparatorConstraint<T> extends Constraint { }; trueX = new ComparatorPropagator<T>(comparator, allowEqual, x, y); trueY = new ComparatorPropagator<T>(reverseComparator, allowEqual, y, x); - falseX = new ComparatorPropagator<T>(reverseComparator, !allowEqual, x, y); + falseX = new ComparatorPropagator<T>(reverseComparator, !allowEqual, x, + y); falseY = new ComparatorPropagator<T>(comparator, !allowEqual, y, x); } - + @Override public Collection<Var<?>> getWatchedVars() { - return Arrays.<Var<?>>asList(x,y); + return Arrays.<Var<?>> asList(x, y); } @Override public Collection<Propagator> getPropagators(boolean negate) { if (negate) { - return Arrays.<Propagator>asList(falseX,falseY); + return Arrays.<Propagator> asList(falseX, falseY); } else { - return Arrays.<Propagator>asList(trueX,trueY); + return Arrays.<Propagator> asList(trueX, trueY); } } @Override public Satisfiability getSatisfiability() { - T maxX = Collections.max(x.getRange(), comparator); - T minY = Collections.min(y.getRange(), comparator); - if (comparator.compare(maxX, minY) < (allowEqual ? 1 : 0)) { - return TAUT; - } - T minX = Collections.min(x.getRange(), comparator); - T maxY = Collections.max(y.getRange(), comparator); - if (comparator.compare(maxY, minX) < (allowEqual ? 0 : 1)) { + try { + T maxX = Collections.max(x.getRange(), comparator); + T minY = Collections.min(y.getRange(), comparator); + if (comparator.compare(maxX, minY) < (allowEqual ? 1 : 0)) { + return TAUT; + } + T minX = Collections.min(x.getRange(), comparator); + T maxY = Collections.max(y.getRange(), comparator); + if (comparator.compare(maxY, minX) < (allowEqual ? 0 : 1)) { + return UNSAT; + } + return SAT; + } catch (NoSuchElementException e) { return UNSAT; } - return SAT; } } diff --git a/src/jrummikub/ai/fdsolver/constraint/IfConstraint.java b/src/jrummikub/ai/fdsolver/constraint/IfConstraint.java index 3046eb5..fc1b484 100644 --- a/src/jrummikub/ai/fdsolver/constraint/IfConstraint.java +++ b/src/jrummikub/ai/fdsolver/constraint/IfConstraint.java @@ -63,7 +63,7 @@ public class IfConstraint extends Constraint { @Override public void propagate() { - if (child.getSatisfiability() == Satisfiability.UNSAT) { + if (!child.isSatisfiable()) { condition.invalidate(!negateCond); } } diff --git a/src/jrummikub/ai/fdsolver/constraint/IndexConstraint.java b/src/jrummikub/ai/fdsolver/constraint/IndexConstraint.java index 9d80a37..6698282 100644 --- a/src/jrummikub/ai/fdsolver/constraint/IndexConstraint.java +++ b/src/jrummikub/ai/fdsolver/constraint/IndexConstraint.java @@ -8,6 +8,8 @@ import java.util.HashSet; import java.util.Iterator; import java.util.List; +import org.w3c.dom.ranges.Range; + import jrummikub.ai.fdsolver.Constraint; import jrummikub.ai.fdsolver.Propagator; import jrummikub.ai.fdsolver.Satisfiability; @@ -47,16 +49,16 @@ public class IndexConstraint<T> extends Constraint { @Override public void propagate() { - HashSet<T> union = new HashSet<T>(); + HashSet<T> invUnion = new HashSet<T>(target.getRange()); for (int i : index.getRange()) { - union.addAll(list.get(i).getRange()); - } - for (Iterator<T> i = target.iterator(); i.hasNext();) { - T val = i.next(); - if (!union.contains(val)) { - i.remove(); + invUnion.removeAll(list.get(i).getRange()); + if (invUnion.isEmpty()) { + return; } } + for (T val : invUnion) { + target.invalidate(val); + } }; } @@ -70,9 +72,8 @@ public class IndexConstraint<T> extends Constraint { public void propagate() { for (Iterator<Integer> i = index.iterator(); i.hasNext();) { int id = i.next(); - HashSet<T> range = new HashSet<T>(target.getRange()); - range.retainAll(list.get(id).getRange()); - if (range.isEmpty()) { + Var<T> item = list.get(id); + if (Collections.disjoint(item.getRange(), target.getRange())) { i.remove(); } } @@ -107,28 +108,33 @@ public class IndexConstraint<T> extends Constraint { } return Arrays.<Propagator> asList(new UnionProp(), new IndexProp(), new VarProp()); } - + @Override - public Satisfiability getSatisfiability() { - HashSet<T> union = new HashSet<T>(); + public boolean isSatisfiable() { for (int i : index.getRange()) { - union.addAll(list.get(i).getRange()); - } - boolean isSat = false; - for (T val : target.getRange()) { - if (union.contains(val)) { - isSat = true; - break; + if(!Collections.disjoint(list.get(i).getRange(), target.getRange())) { + return true; } } - if (!isSat) { + return false; + } + + @Override + public Satisfiability getSatisfiability() { + boolean sat = isSatisfiable(); + if (!sat) { return Satisfiability.UNSAT; - } else { - if (union.size() == 1 && target.getRange().size() == 1) { - return Satisfiability.TAUT; - } else { + } + if (target.getRange().size() > 1) + return Satisfiability.SAT; + for (int i : index.getRange()) { + Var<T> var = list.get(i); + if (var.getRange().size() > 1) + return Satisfiability.SAT; + if(var.getValue() != target.getValue()) { return Satisfiability.SAT; } } + return Satisfiability.TAUT; } } diff --git a/src/jrummikub/ai/fdsolver/constraint/OffsetConstraint.java b/src/jrummikub/ai/fdsolver/constraint/OffsetConstraint.java index a324d2a..eb72df8 100644 --- a/src/jrummikub/ai/fdsolver/constraint/OffsetConstraint.java +++ b/src/jrummikub/ai/fdsolver/constraint/OffsetConstraint.java @@ -2,6 +2,7 @@ package jrummikub.ai.fdsolver.constraint; import java.util.Arrays; import java.util.Collection; +import java.util.Collections; import java.util.HashSet; import java.util.Iterator; @@ -60,12 +61,24 @@ public class OffsetConstraint extends Constraint { @Override public Satisfiability getSatisfiability() { - HashSet<Integer> shiftedRange = new HashSet<Integer>(); - for (int val : x.getRange()) { - shiftedRange.add(val + offset); + boolean disjoint = true; + if (x.getRange().size() < y.getRange().size()) { + for (int xv : x.getRange()) { + if (y.getRange().contains(xv + offset)) { + disjoint = false; + break; + } + } + } else { + for (int yv : y.getRange()) { + if (x.getRange().contains(yv - offset)) { + disjoint = false; + break; + } + } } - shiftedRange.retainAll(y.getRange()); - if (shiftedRange.isEmpty()) { + + if (disjoint) { return Satisfiability.UNSAT; } else if (x.getRange().size() == 1 && y.getRange().size() == 1) { return Satisfiability.TAUT; diff --git a/src/jrummikub/ai/fdsolver/constraint/SameConstraint.java b/src/jrummikub/ai/fdsolver/constraint/SameConstraint.java index 954b6fa..7fc0025 100644 --- a/src/jrummikub/ai/fdsolver/constraint/SameConstraint.java +++ b/src/jrummikub/ai/fdsolver/constraint/SameConstraint.java @@ -2,6 +2,7 @@ package jrummikub.ai.fdsolver.constraint; import java.util.Arrays; import java.util.Collection; +import java.util.Collections; import java.util.HashSet; import java.util.Iterator; @@ -56,9 +57,7 @@ public class SameConstraint<T> extends Constraint { @Override public Satisfiability getSatisfiability() { - HashSet<T> range = new HashSet<T>(x.getRange()); - range.retainAll(y.getRange()); - if (range.isEmpty()) { + if (Collections.disjoint(x.getRange(), y.getRange())) { return Satisfiability.UNSAT; } else if (x.getRange().size() == 1 && y.getRange().size() == 1) { return Satisfiability.TAUT; |