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/Constraint.java4
-rw-r--r--src/jrummikub/ai/fdsolver/Solver.java61
-rw-r--r--src/jrummikub/ai/fdsolver/Var.java8
-rw-r--r--src/jrummikub/ai/fdsolver/constraint/ComparatorConstraint.java39
-rw-r--r--src/jrummikub/ai/fdsolver/constraint/IfConstraint.java2
-rw-r--r--src/jrummikub/ai/fdsolver/constraint/IndexConstraint.java56
-rw-r--r--src/jrummikub/ai/fdsolver/constraint/OffsetConstraint.java23
-rw-r--r--src/jrummikub/ai/fdsolver/constraint/SameConstraint.java5
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;