diff options
Diffstat (limited to 'src/jrummikub/ai/fdsolver')
8 files changed, 119 insertions, 79 deletions
diff --git a/src/jrummikub/ai/fdsolver/Constraint.java b/src/jrummikub/ai/fdsolver/Constraint.java index b081d4b..a046324 100644 --- a/src/jrummikub/ai/fdsolver/Constraint.java +++ b/src/jrummikub/ai/fdsolver/Constraint.java @@ -10,4 +10,8 @@ public abstract class Constraint { public abstract Collection<Propagator> getPropagators(boolean negate); public abstract Satisfiability getSatisfiability(); + + public boolean isSatisfiable() { + return getSatisfiability() != Satisfiability.UNSAT; + } } diff --git a/src/jrummikub/ai/fdsolver/Solver.java b/src/jrummikub/ai/fdsolver/Solver.java index 2277ba4..0bdb344 100644 --- a/src/jrummikub/ai/fdsolver/Solver.java +++ b/src/jrummikub/ai/fdsolver/Solver.java @@ -7,6 +7,7 @@ import java.util.Collections; import java.util.HashMap; import java.util.HashSet; import java.util.Iterator; +import java.util.List; import java.util.Map; import java.util.Set; import static jrummikub.ai.fdsolver.Satisfiability.*; @@ -24,6 +25,8 @@ public class Solver { Set<Constraint> constraints = new HashSet<Constraint>(); + Set<Constraint> dirtyConstraints = new HashSet<Constraint>(); + ArrayList<StackFrame> stack = new ArrayList<StackFrame>(); boolean contradiction = false; @@ -83,27 +86,19 @@ public class Solver { } } - public void propagateOnce() { - Var<?> dirtyVar = Collections.min(dirtyVars); - dirtyVars.remove(dirtyVar); - outerLoop: for (Iterator<Constraint> i = dirtyVar.getConstraints() - .iterator(); i.hasNext();) { - Constraint constraint = i.next(); - Satisfiability sat = constraint.getSatisfiability(); - if (sat == UNSAT) { - contradiction = true; - break; - } - if (sat == TAUT) { - i.remove(); - finishedConstraint(constraint, dirtyVar); - continue; - } - for (Propagator propagator : constraint.cachedPropagators) { - if (propagator.getWatchedVars().contains(dirtyVar)) { - propagator.propagate(); - if (contradiction) { - break outerLoop; + public void propagateEach() { + List<Var<?>> oldDirtyVars = new ArrayList<Var<?>>(dirtyVars); + dirtyVars.clear(); + Collections.sort(oldDirtyVars); + outerLoop: for(Var<?> dirtyVar : oldDirtyVars) { + for (Constraint constraint : dirtyVar.getConstraints()) { + dirtyConstraints.add(constraint); + for (Propagator propagator : constraint.cachedPropagators) { + if (propagator.getWatchedVars().contains(dirtyVar)) { + propagator.propagate(); + if (contradiction) { + break outerLoop; + } } } } @@ -111,9 +106,31 @@ public class Solver { } public void propagateAll() { + int i = 0; while (!(dirtyVars.isEmpty() || contradiction)) { - propagateOnce(); + i++; + if (i == 50) { + cleanUpConstraints(); + i = 0; + } else { + propagateEach(); + } + } + cleanUpConstraints(); + } + + private void cleanUpConstraints() { + for (Constraint constraint : dirtyConstraints) { + Satisfiability sat = constraint.getSatisfiability(); + if (sat == UNSAT) { + contradiction = true; + break; + } + if (sat == TAUT) { + finishedConstraint(constraint, null); + } } + dirtyConstraints.clear(); } public void addVar(Var<?> var) { diff --git a/src/jrummikub/ai/fdsolver/Var.java b/src/jrummikub/ai/fdsolver/Var.java index 3124e8b..a454487 100644 --- a/src/jrummikub/ai/fdsolver/Var.java +++ b/src/jrummikub/ai/fdsolver/Var.java @@ -99,18 +99,12 @@ public class Var<T> implements Comparable<Var<T>> { return constraints.size(); } - private double fitness() { - return range.size();//neighborCount(); - } - @Override public int compareTo(Var<T> other) { - return ((Double)fitness()).compareTo(other.fitness()); - /* int rangeCompare = ((Integer)range.size()).compareTo(other.range.size()); if (rangeCompare != 0) return rangeCompare; - return -((Integer)neighborCount()).compareTo(other.neighborCount());*/ + return -((Integer)neighborCount()).compareTo(other.neighborCount()); } } 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; |