summaryrefslogtreecommitdiffstats
path: root/src/jrummikub/ai/fdsolver/Solver.java
diff options
context:
space:
mode:
Diffstat (limited to 'src/jrummikub/ai/fdsolver/Solver.java')
-rw-r--r--src/jrummikub/ai/fdsolver/Solver.java81
1 files changed, 66 insertions, 15 deletions
diff --git a/src/jrummikub/ai/fdsolver/Solver.java b/src/jrummikub/ai/fdsolver/Solver.java
index 6660467..c47b1c1 100644
--- a/src/jrummikub/ai/fdsolver/Solver.java
+++ b/src/jrummikub/ai/fdsolver/Solver.java
@@ -3,11 +3,13 @@ package jrummikub.ai.fdsolver;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
+import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Map;
import java.util.Set;
+import static jrummikub.ai.fdsolver.Satisfiability.*;
public class Solver {
Set<Var<?>> vars = new HashSet<Var<?>>();
@@ -26,6 +28,7 @@ public class Solver {
Map<Var<?>, HashSet<?>> invalidatedValues = new HashMap<Var<?>, HashSet<?>>();
Var<?> branchVar;
Object branchValue;
+ HashSet<Constraint> finishedConstraints = new HashSet<Constraint>();
public <T> void invalidate(Var<T> var, T invalid) {
HashSet<T> values = (HashSet<T>) invalidatedValues.get(var);
@@ -47,16 +50,19 @@ public class Solver {
stack.add(new StackFrame());
}
+ private boolean isSolved() {
+ return dirtyVars.isEmpty() && unsolvedVars.isEmpty();
+ }
+
public boolean solve() {
do {
solveStep();
- } while (!(contradiction || (dirtyVars.isEmpty() && unsolvedVars
- .isEmpty())));
+ } while (!(contradiction || isSolved()));
return !contradiction;
}
public void solveStep() {
- if (unsolvedVars.isEmpty() && dirtyVars.isEmpty()) {
+ if (isSolved()) {
contradiction = true;
} else {
propagateAll();
@@ -74,17 +80,25 @@ public class Solver {
}
public void propagateOnce() {
- Iterator<Var<?>> it = dirtyVars.iterator();
- Var<?> dirtyVar = it.next();
- it.remove();
- outerLoop: for (Constraint constraint : constraints) {
- if (constraint.getWatchedVars().contains(dirtyVar)) {
- for (Propagator propagator : constraint.getPropagators(false)) {
- if (propagator.getWatchedVars().contains(dirtyVar)) {
- propagator.propagate();
- if (contradiction) {
- break outerLoop;
- }
+ Var<?> dirtyVar = Collections.max(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.getPropagators(false)) {
+ if (propagator.getWatchedVars().contains(dirtyVar)) {
+ propagator.propagate();
+ if (contradiction) {
+ break outerLoop;
}
}
}
@@ -109,6 +123,7 @@ public class Solver {
for (Var<?> var : constraint.getWatchedVars()) {
var.makeDirty();
+ var.getConstraints().add(constraint);
}
}
@@ -120,7 +135,14 @@ public class Solver {
@SuppressWarnings("unchecked")
void branchOn(Var<?> var) {
- Object value = var.getRange().iterator().next();
+
+ Set<?> range = var.getRange();
+ int n = (int)(Math.random() * range.size());
+ Iterator<?> it = range.iterator();
+ for (int i = 0; i < n; i++) {
+ it.next();
+ }
+ Object value = it.next();
branchWith((Var<Object>) var, value);
}
@@ -143,6 +165,16 @@ public class Solver {
}
}
+ private void finishedConstraint(Constraint constraint, Var<?> currentVar) {
+ for (Var<?> var : constraint.getWatchedVars()) {
+ if (var != currentVar) {
+ var.getConstraints().remove(constraint);
+ }
+ }
+ constraints.remove(constraint);
+ getTopStackFrame().finishedConstraints.add(constraint);
+ }
+
@SuppressWarnings("unchecked")
// This would need rank-2 types which java lacks
private void rollback(StackFrame item) {
@@ -156,6 +188,13 @@ public class Solver {
} else {
unsolvedVars.remove(var);
}
+ var.makeDirty(); // TODO think a bit more about this
+ }
+ for (Constraint constraint : item.finishedConstraints) {
+ for (Var<?> var : constraint.getWatchedVars()) {
+ var.getConstraints().add(constraint);
+ }
+ constraints.add(constraint);
}
}
@@ -191,5 +230,17 @@ public class Solver {
public <T> Var<T> makeVar(T... range) {
return makeVar(Arrays.asList(range));
}
+
+ public void record() {
+ for (Var<?> var : vars) {
+ var.record();
+ }
+ }
+
+ public void restore() {
+ for (Var<?> var : vars) {
+ var.restore();
+ }
+ }
}