diff options
18 files changed, 598 insertions, 55 deletions
diff --git a/src/jrummikub/ai/fdsolver/Constraint.java b/src/jrummikub/ai/fdsolver/Constraint.java index 0d4071d..f7955ce 100644 --- a/src/jrummikub/ai/fdsolver/Constraint.java +++ b/src/jrummikub/ai/fdsolver/Constraint.java @@ -1,5 +1,11 @@ package jrummikub.ai.fdsolver; +import java.util.Collection; + public interface Constraint { - + public Collection<Var<?>> getWatchedVars(); + + public Collection<Propagator> getPropagators(boolean negate); + + public Satisfiability getSatisfiability(); } diff --git a/src/jrummikub/ai/fdsolver/Constraints.java b/src/jrummikub/ai/fdsolver/Constraints.java deleted file mode 100644 index 589ecb5..0000000 --- a/src/jrummikub/ai/fdsolver/Constraints.java +++ /dev/null @@ -1,13 +0,0 @@ -package jrummikub.ai.fdsolver; - -public class Constraints { - - public static <T extends Comparable<T>> void lessThan(Solver solver, Var<T> x, Var<T> y) { - // TODO Auto-generated method stub - } - - public static <T extends Comparable<T>> void lessThan(Solver solver, Var<T> x, T y) { - // TODO Auto-generated method stub - } - -} diff --git a/src/jrummikub/ai/fdsolver/LessThan.java b/src/jrummikub/ai/fdsolver/LessThan.java deleted file mode 100644 index 25acd9b..0000000 --- a/src/jrummikub/ai/fdsolver/LessThan.java +++ /dev/null @@ -1,9 +0,0 @@ -package jrummikub.ai.fdsolver; - -public class LessThan<T> implements Constraint { - - public LessThan(Var<T> x, Var<T> y) { - // TODO Auto-generated constructor stub - } - -} diff --git a/src/jrummikub/ai/fdsolver/Propagator.java b/src/jrummikub/ai/fdsolver/Propagator.java new file mode 100644 index 0000000..dfe720a --- /dev/null +++ b/src/jrummikub/ai/fdsolver/Propagator.java @@ -0,0 +1,9 @@ +package jrummikub.ai.fdsolver; + +import java.util.Collection; + +public interface Propagator { + public abstract Collection<Var<?>> getWatchedVars(); + + public abstract void propagate(); +} diff --git a/src/jrummikub/ai/fdsolver/Satisfiability.java b/src/jrummikub/ai/fdsolver/Satisfiability.java new file mode 100644 index 0000000..9f3a23a --- /dev/null +++ b/src/jrummikub/ai/fdsolver/Satisfiability.java @@ -0,0 +1,5 @@ +package jrummikub.ai.fdsolver; + +public enum Satisfiability { + TAUT, SAT, UNSAT +} diff --git a/src/jrummikub/ai/fdsolver/Solver.java b/src/jrummikub/ai/fdsolver/Solver.java index 1164c36..6660467 100644 --- a/src/jrummikub/ai/fdsolver/Solver.java +++ b/src/jrummikub/ai/fdsolver/Solver.java @@ -1,25 +1,195 @@ package jrummikub.ai.fdsolver; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Collection; +import java.util.HashMap; +import java.util.HashSet; +import java.util.Iterator; +import java.util.Map; +import java.util.Set; + public class Solver { + Set<Var<?>> vars = new HashSet<Var<?>>(); + + Set<Var<?>> dirtyVars = new HashSet<Var<?>>(); + + Set<Var<?>> unsolvedVars = new HashSet<Var<?>>(); + + Set<Constraint> constraints = new HashSet<Constraint>(); + + ArrayList<StackFrame> stack = new ArrayList<StackFrame>(); + + boolean contradiction = false; - public void add(Constraint constraint) { - // TODO Auto-generated method stub - + static private class StackFrame { + Map<Var<?>, HashSet<?>> invalidatedValues = new HashMap<Var<?>, HashSet<?>>(); + Var<?> branchVar; + Object branchValue; + + public <T> void invalidate(Var<T> var, T invalid) { + HashSet<T> values = (HashSet<T>) invalidatedValues.get(var); + if (values == null) { + invalidatedValues.put(var, + new HashSet<T>(Arrays.asList(invalid))); + } else { + values.add(invalid); + } + } + + @Override + public String toString() { + return "StackItem [invalidatedValues=" + invalidatedValues + "]"; + } + } + + public Solver() { + stack.add(new StackFrame()); } public boolean solve() { - // TODO Auto-generated method stub - return false; + do { + solveStep(); + } while (!(contradiction || (dirtyVars.isEmpty() && unsolvedVars + .isEmpty()))); + return !contradiction; + } + + public void solveStep() { + if (unsolvedVars.isEmpty() && dirtyVars.isEmpty()) { + contradiction = true; + } else { + propagateAll(); + } + if (contradiction) { + if (stack.size() == 1) { + return; + } + backtrack(); + } else if (unsolvedVars.isEmpty()) { + return; + } else { + branch(); + } + } + + 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; + } + } + } + } + } + } + + public void propagateAll() { + while (!(dirtyVars.isEmpty() || contradiction)) { + propagateOnce(); + } + } + + public void addVar(Var<?> var) { + vars.add(var); + if (var.getRange().size() != 1) { + unsolvedVars.add(var); + } + } + + public void addConstraint(Constraint constraint) { + constraints.add(constraint); + + for (Var<?> var : constraint.getWatchedVars()) { + var.makeDirty(); + } + } + + // backtracking and logging + + void branch() { + branchOn(unsolvedVars.iterator().next()); + } + + @SuppressWarnings("unchecked") + void branchOn(Var<?> var) { + Object value = var.getRange().iterator().next(); + branchWith((Var<Object>) var, value); + } + + <T> void branchWith(Var<T> var, T value) { + StackFrame stackFrame = new StackFrame(); + stackFrame.branchVar = var; + stackFrame.branchValue = value; + stack.add(stackFrame); + var.choose(value); + } + + private StackFrame getTopStackFrame() { + return stack.get(stack.size() - 1); + } + + <T> void logInvalidation(Var<T> var, T invalid) { + getTopStackFrame().invalidate(var, invalid); + if (var.getRange().size() == 1) { + unsolvedVars.remove(var); + } + } + + @SuppressWarnings("unchecked") + // This would need rank-2 types which java lacks + private void rollback(StackFrame item) { + for (Map.Entry<Var<?>, HashSet<?>> entry : item.invalidatedValues + .entrySet()) { + Var<Object> var = (Var<Object>) entry.getKey(); + HashSet<Object> values = (HashSet<Object>) entry.getValue(); + var.getRange().addAll(values); + if (var.getRange().size() != 1) { + unsolvedVars.add(var); + } else { + unsolvedVars.remove(var); + } + } + } + + @SuppressWarnings("unchecked") + void backtrack() { + contradiction = false; + StackFrame topFrame = getTopStackFrame(); + rollback(topFrame); + stack.remove(stack.size() - 1); + ((Var<Object>) topFrame.branchVar).invalidate(topFrame.branchValue); + } + + // factory methods for vars + + public Var<Integer> makeRangeVar(int low, int high) { + ArrayList<Integer> range = new ArrayList<Integer>(); + for (int i = low; i <= high; i++) { + range.add(i); + } + return makeVar(range); + } + + public Var<Boolean> makeBoolVar() { + return makeVar(true, false); } - public void push() { - // TODO Auto-generated method stub - + public <T> Var<T> makeVar(Collection<T> range) { + Var<T> var = new Var<T>(this, range); + addVar(var); + return var; } - public void pop() { - // TODO Auto-generated method stub - + public <T> Var<T> makeVar(T... range) { + return makeVar(Arrays.asList(range)); } } diff --git a/src/jrummikub/ai/fdsolver/SolverMain.java b/src/jrummikub/ai/fdsolver/SolverMain.java new file mode 100644 index 0000000..4750675 --- /dev/null +++ b/src/jrummikub/ai/fdsolver/SolverMain.java @@ -0,0 +1,42 @@ +package jrummikub.ai.fdsolver; + + +public class SolverMain { + + /* + * eingabe: liste handsteinen + liste tischsteinen + * + * foreach stein: stein id (durchlaufend nummeriert) Var<Boolean> onTable = + * tisch ? {true}, {true, false} Var<Integer> value = {N} Var<StoneColor> + * color = {C} Var<Integer> nachbarL,R = {-1, 0...steinanzahl} Var<Boolean> + * groupOrRun + * + * nachbarR != -1 => nachbarL[nachbarR[id]] == id nachbarL != -1 => + * nachbarR[nachbarL[id]] == id + * + * nachbarR != -1 => gOR[nachbarR[id]] = gOR nachbarL != -1 => + * gOR[nachbarL[id]] = gOR + * + * nachbar{R,L} != -1 => group <=> value[{R,L}] == value nachbar{R,L} != -1 + * && group => color[{R,L}] {<,>} color // hier auch <=> ? + * + * nachbar{R,L} != -1 => run <=> color[{R,L}] == color nachbar{R,L} != -1 => + * run <=> value[{R,L}] == value {+,-} 1 + * + * Var<Integer> pos von {links, rechts} + constraints + * + * links + rechts >= 3 + * + * foreach handstein: Var<Integer> badness = onTable ? ### (z. B. 1) : 0 + * + * totalBadness = sum(all badness) + * + * foreach joker: Var<Integer> value = {-1, 1..13} Var<StoneColor> color = + * {F, C0..C3} onTable == false <=> value == -1 same with color + * + * joker sind sortiert + */ + public static void main(String[] args) { + } + +} diff --git a/src/jrummikub/ai/fdsolver/Var.java b/src/jrummikub/ai/fdsolver/Var.java index a2b5cd7..eb6f432 100644 --- a/src/jrummikub/ai/fdsolver/Var.java +++ b/src/jrummikub/ai/fdsolver/Var.java @@ -2,24 +2,77 @@ package jrummikub.ai.fdsolver; import java.util.Collection; import java.util.HashSet; -import java.util.Set; +import java.util.Iterator; public class Var<T> { - Set<T> range; - + private Solver solver; + private HashSet<T> range; + public Var(Solver solver, Collection<T> range) { + this.solver = solver; this.range = new HashSet<T>(range); } - public static <T> Var<T> range(Solver solver, T low, T high) { - // TODO todo todo todo - return null; - } - public T getValue() { if (range.size() != 1) return null; return range.iterator().next(); } + public HashSet<T> getRange() { + return range; + } + + public void choose(T value) { + for (Iterator<T> i = this.iterator(); i.hasNext();) { + if (i.next() != value) { + i.remove(); + } + } + } + + public void makeDirty() { + this.solver.dirtyVars.add(this); + } + + public void invalidate(T value) { + range.remove(value); + solver.logInvalidation(this, value); + makeDirty(); + } + + public Iterator<T> iterator() { + final Iterator<T> iterator = range.iterator(); + return new Iterator<T>() { + T lastValue; + + @Override + public boolean hasNext() { + return iterator.hasNext(); + } + + @Override + public T next() { + lastValue = iterator.next(); + return lastValue; + } + + @Override + public void remove() { + // TODO logging + iterator.remove(); + solver.logInvalidation(Var.this, lastValue); + makeDirty(); + if (range.size() == 0) { + solver.contradiction = true; + } + } + }; + } + + @Override + public String toString() { + return "Var" + range; + } + } diff --git a/src/jrummikub/ai/fdsolver/constraint/ComparatorConstraint.java b/src/jrummikub/ai/fdsolver/constraint/ComparatorConstraint.java new file mode 100644 index 0000000..24e7ecf --- /dev/null +++ b/src/jrummikub/ai/fdsolver/constraint/ComparatorConstraint.java @@ -0,0 +1,67 @@ +package jrummikub.ai.fdsolver.constraint; + +import static jrummikub.ai.fdsolver.Satisfiability.*; + +import java.util.Arrays; +import java.util.Collection; +import java.util.Collections; +import java.util.Comparator; + +import jrummikub.ai.fdsolver.Constraint; +import jrummikub.ai.fdsolver.Propagator; +import jrummikub.ai.fdsolver.Satisfiability; +import jrummikub.ai.fdsolver.Var; + +public class ComparatorConstraint<T> implements Constraint { + Var<T> x, y; + 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) { + this.x = x; + this.y = y; + this.comparator = comparator; + this.allowEqual = allowEqual; + reverseComparator = new Comparator<T>() { + @Override + public int compare(T o1, T o2) { + return comparator.compare(o2, o1); + } + }; + trueX = new ComparatorPropagator<T>(comparator, allowEqual, x, y); + trueY = new ComparatorPropagator<T>(reverseComparator, allowEqual, y, x); + 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); + } + + @Override + public Collection<Propagator> getPropagators(boolean negate) { + if (negate) { + return Arrays.<Propagator>asList(falseX,falseY); + } else { + 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)) { + return UNSAT; + } + return SAT; + } + +} diff --git a/src/jrummikub/ai/fdsolver/constraint/ComparatorPropagator.java b/src/jrummikub/ai/fdsolver/constraint/ComparatorPropagator.java new file mode 100644 index 0000000..b3a3089 --- /dev/null +++ b/src/jrummikub/ai/fdsolver/constraint/ComparatorPropagator.java @@ -0,0 +1,42 @@ +package jrummikub.ai.fdsolver.constraint; + +import java.util.Arrays; +import java.util.Collection; +import java.util.Collections; +import java.util.Comparator; +import java.util.HashSet; +import java.util.Iterator; +import java.util.List; + +import jrummikub.ai.fdsolver.Propagator; +import jrummikub.ai.fdsolver.Var; + +public class ComparatorPropagator<T> implements Propagator { + private Var<T> x, y; + private Comparator<T> comparator; + private boolean allowEqual; + public ComparatorPropagator(Comparator<T> comparator, boolean allowEqual, Var<T> x, Var<T> y) { + this.comparator = comparator; + this.allowEqual = allowEqual; + this.x = x; + this.y = y; + } + + @Override + public Collection<Var<?>> getWatchedVars() { + return Arrays.<Var<?>>asList(y); + } + + @Override + public void propagate() { + T maxY = Collections.max(y.getRange(), comparator); + + for(Iterator<T> i = x.iterator(); i.hasNext();) { + T value = i.next(); + int comparision = comparator.compare(value, maxY); + if (comparision > 0 || comparision == 0 && !allowEqual) { + i.remove(); + } + } + } +} diff --git a/src/jrummikub/ai/fdsolver/constraint/Filter.java b/src/jrummikub/ai/fdsolver/constraint/Filter.java new file mode 100644 index 0000000..59c880a --- /dev/null +++ b/src/jrummikub/ai/fdsolver/constraint/Filter.java @@ -0,0 +1,5 @@ +package jrummikub.ai.fdsolver.constraint; + +public interface Filter<T> { + public boolean accept(T value); +} diff --git a/src/jrummikub/ai/fdsolver/constraint/FilterConstraint.java b/src/jrummikub/ai/fdsolver/constraint/FilterConstraint.java new file mode 100644 index 0000000..e676882 --- /dev/null +++ b/src/jrummikub/ai/fdsolver/constraint/FilterConstraint.java @@ -0,0 +1,65 @@ +package jrummikub.ai.fdsolver.constraint; + +import static jrummikub.ai.fdsolver.Satisfiability.SAT; +import static jrummikub.ai.fdsolver.Satisfiability.TAUT; +import static jrummikub.ai.fdsolver.Satisfiability.UNSAT; + +import java.util.Arrays; +import java.util.Collection; + +import jrummikub.ai.fdsolver.Constraint; +import jrummikub.ai.fdsolver.Propagator; +import jrummikub.ai.fdsolver.Satisfiability; +import jrummikub.ai.fdsolver.Var; + +public class FilterConstraint<T> implements Constraint { + private Var<T> var; + private Propagator trueProp, falseProp; + private Filter<T> filter; + + public FilterConstraint(final Filter<T> filter, Var<T> var) { + this.var = var; + this.filter = filter; + trueProp = new FilterPropagator<T>(filter, var); + falseProp = new FilterPropagator<T>(new Filter<T>() { + @Override + public boolean accept(T value) { + return !filter.accept(value); + } + }, var); + } + + @Override + public Collection<Var<?>> getWatchedVars() { + return Arrays.<Var<?>> asList(var); + } + + @Override + public Collection<Propagator> getPropagators(boolean negate) { + return Arrays.asList(negate ? falseProp : trueProp); + } + + @Override + public Satisfiability getSatisfiability() { + boolean any = false; + boolean all = true; + + for (T value : var.getRange()) { + boolean accepted = filter.accept(value); + if (accepted) { + any = true; + } else { + all = false; + } + } + + if (all && any) { + return TAUT; + } else if (any) { + return SAT; + } else { + return UNSAT; + } + } + +} diff --git a/src/jrummikub/ai/fdsolver/constraint/FilterPropagator.java b/src/jrummikub/ai/fdsolver/constraint/FilterPropagator.java new file mode 100644 index 0000000..80518c9 --- /dev/null +++ b/src/jrummikub/ai/fdsolver/constraint/FilterPropagator.java @@ -0,0 +1,31 @@ +package jrummikub.ai.fdsolver.constraint; + +import java.util.Arrays; +import java.util.Collection; +import java.util.Iterator; + +import jrummikub.ai.fdsolver.Propagator; +import jrummikub.ai.fdsolver.Var; + +public class FilterPropagator<T> implements Propagator { + private Filter<T> filter; + private Var<T> var; + + public FilterPropagator(Filter<T> filter, Var<T> var) { + this.filter = filter; + this.var = var; + } + + @Override + public Collection<Var<?>> getWatchedVars() { + return Arrays.<Var<?>>asList(var); + } + + @Override + public void propagate() { + for(Iterator<T> i = var.iterator(); i.hasNext();) { + if(!filter.accept(i.next())) + i.remove(); + } + } +} diff --git a/src/jrummikub/ai/fdsolver/constraint/GreaterThan.java b/src/jrummikub/ai/fdsolver/constraint/GreaterThan.java new file mode 100644 index 0000000..9bdccd2 --- /dev/null +++ b/src/jrummikub/ai/fdsolver/constraint/GreaterThan.java @@ -0,0 +1,18 @@ +package jrummikub.ai.fdsolver.constraint; + +import java.util.Comparator; + +import jrummikub.ai.fdsolver.Var; + +public class GreaterThan<T extends Comparable<T>> extends + ComparatorConstraint<T> { + + public GreaterThan(boolean allowEqual, Var<T> x, Var<T> y) { + super(new Comparator<T>() { + @Override + public int compare(T o1, T o2) { + return o2.compareTo(o1); + } + }, allowEqual, x, y); + } +} diff --git a/src/jrummikub/ai/fdsolver/constraint/GreaterThanConst.java b/src/jrummikub/ai/fdsolver/constraint/GreaterThanConst.java new file mode 100644 index 0000000..6b00ee3 --- /dev/null +++ b/src/jrummikub/ai/fdsolver/constraint/GreaterThanConst.java @@ -0,0 +1,15 @@ +package jrummikub.ai.fdsolver.constraint; + +import jrummikub.ai.fdsolver.Var; + +public class GreaterThanConst<T extends Comparable<T>> extends + FilterConstraint<T> { + public GreaterThanConst(final boolean allowEqual, Var<T> x, final T y) { + super(new Filter<T>() { + @Override + public boolean accept(T value) { + return y.compareTo(value) < (allowEqual ? 1 : 0); + } + }, x); + } +} diff --git a/src/jrummikub/ai/fdsolver/constraint/LessThan.java b/src/jrummikub/ai/fdsolver/constraint/LessThan.java new file mode 100644 index 0000000..b79252c --- /dev/null +++ b/src/jrummikub/ai/fdsolver/constraint/LessThan.java @@ -0,0 +1,17 @@ +package jrummikub.ai.fdsolver.constraint; + +import java.util.Comparator; + +import jrummikub.ai.fdsolver.Var; + +public class LessThan<T extends Comparable<T>> extends ComparatorConstraint<T> { + + public LessThan(boolean allowEqual, Var<T> x, Var<T> y) { + super(new Comparator<T>() { + @Override + public int compare(T o1, T o2) { + return o1.compareTo(o2); + } + }, allowEqual, x, y); + } +} diff --git a/src/jrummikub/ai/fdsolver/constraint/LessThanConst.java b/src/jrummikub/ai/fdsolver/constraint/LessThanConst.java new file mode 100644 index 0000000..18d8827 --- /dev/null +++ b/src/jrummikub/ai/fdsolver/constraint/LessThanConst.java @@ -0,0 +1,18 @@ +package jrummikub.ai.fdsolver.constraint; + +import java.util.Collection; + +import jrummikub.ai.fdsolver.Propagator; +import jrummikub.ai.fdsolver.Solver; +import jrummikub.ai.fdsolver.Var; + +public class LessThanConst<T extends Comparable<T>> extends FilterConstraint<T> { + public LessThanConst(final boolean allowEqual, Var<T> x, final T y) { + super(new Filter<T>() { + @Override + public boolean accept(T value) { + return value.compareTo(y) < (allowEqual ? 1 : 0); + } + }, x); + } +} diff --git a/test/jrummikub/ai/fdsolver/SolverTest.java b/test/jrummikub/ai/fdsolver/SolverTest.java index 3798423..d03dfe4 100644 --- a/test/jrummikub/ai/fdsolver/SolverTest.java +++ b/test/jrummikub/ai/fdsolver/SolverTest.java @@ -1,8 +1,8 @@ package jrummikub.ai.fdsolver; import static org.junit.Assert.assertEquals; - -import java.util.Arrays; +import jrummikub.ai.fdsolver.constraint.LessThan; +import jrummikub.ai.fdsolver.constraint.LessThanConst; import org.junit.Test; @@ -11,18 +11,20 @@ public class SolverTest { public void test() { Solver solver = new Solver(); - Var<Integer> x = new Var<Integer>(solver, Arrays.asList(1, 2, 3)); - Var<Integer> y = Var.range(solver, 1,13); + Var<Integer> x = solver.makeVar(1, 2, 3); + Var<Integer> y = solver.makeRangeVar(1, 13); - Constraints.lessThan(solver, y, x); - - while(solver.solve()) { - solver.push(); - Constraints.lessThan(solver, x, x.getValue()); - } - solver.pop(); + solver.addConstraint(new LessThan<Integer>(false, y, x)); - assertEquals(2, (int)x.getValue()); - assertEquals(1, (int)y.getValue()); + int lastx = 0, lasty = 0; + while (solver.solve()) { + lastx = x.getValue(); + lasty = y.getValue(); + System.out.println("x = " + lastx + ", y = " + lasty); + solver.addConstraint(new LessThanConst<Integer>(false, x, x.getValue())); + } + + assertEquals(2, lastx); + assertEquals(1, lasty); } } |