diff options
Diffstat (limited to 'src/jrummikub/ai/fdsolver/Solver.java')
-rw-r--r-- | src/jrummikub/ai/fdsolver/Solver.java | 81 |
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(); + } + } } |