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();
+		}
+	}
 
 }