From 2b4ad89e72fdf9612854b27bc8dd818c8f062d35 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 13 Jun 2011 22:19:31 +0200 Subject: Restructured fdsolver api and made first test succeed git-svn-id: svn://sunsvr01.isp.uni-luebeck.de/swproj13/trunk@423 72836036-5685-4462-b002-a69064685172 --- src/jrummikub/ai/fdsolver/Constraint.java | 8 +- src/jrummikub/ai/fdsolver/Constraints.java | 13 -- src/jrummikub/ai/fdsolver/LessThan.java | 9 - src/jrummikub/ai/fdsolver/Propagator.java | 9 + src/jrummikub/ai/fdsolver/Satisfiability.java | 5 + src/jrummikub/ai/fdsolver/Solver.java | 192 +++++++++++++++++++-- src/jrummikub/ai/fdsolver/SolverMain.java | 42 +++++ src/jrummikub/ai/fdsolver/Var.java | 69 +++++++- .../fdsolver/constraint/ComparatorConstraint.java | 67 +++++++ .../fdsolver/constraint/ComparatorPropagator.java | 42 +++++ src/jrummikub/ai/fdsolver/constraint/Filter.java | 5 + .../ai/fdsolver/constraint/FilterConstraint.java | 65 +++++++ .../ai/fdsolver/constraint/FilterPropagator.java | 31 ++++ .../ai/fdsolver/constraint/GreaterThan.java | 18 ++ .../ai/fdsolver/constraint/GreaterThanConst.java | 15 ++ src/jrummikub/ai/fdsolver/constraint/LessThan.java | 17 ++ .../ai/fdsolver/constraint/LessThanConst.java | 18 ++ 17 files changed, 583 insertions(+), 42 deletions(-) delete mode 100644 src/jrummikub/ai/fdsolver/Constraints.java delete mode 100644 src/jrummikub/ai/fdsolver/LessThan.java create mode 100644 src/jrummikub/ai/fdsolver/Propagator.java create mode 100644 src/jrummikub/ai/fdsolver/Satisfiability.java create mode 100644 src/jrummikub/ai/fdsolver/SolverMain.java create mode 100644 src/jrummikub/ai/fdsolver/constraint/ComparatorConstraint.java create mode 100644 src/jrummikub/ai/fdsolver/constraint/ComparatorPropagator.java create mode 100644 src/jrummikub/ai/fdsolver/constraint/Filter.java create mode 100644 src/jrummikub/ai/fdsolver/constraint/FilterConstraint.java create mode 100644 src/jrummikub/ai/fdsolver/constraint/FilterPropagator.java create mode 100644 src/jrummikub/ai/fdsolver/constraint/GreaterThan.java create mode 100644 src/jrummikub/ai/fdsolver/constraint/GreaterThanConst.java create mode 100644 src/jrummikub/ai/fdsolver/constraint/LessThan.java create mode 100644 src/jrummikub/ai/fdsolver/constraint/LessThanConst.java (limited to 'src/jrummikub') 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> getWatchedVars(); + + public Collection 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 > void lessThan(Solver solver, Var x, Var y) { - // TODO Auto-generated method stub - } - - public static > void lessThan(Solver solver, Var 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 implements Constraint { - - public LessThan(Var x, Var 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> 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> vars = new HashSet>(); + + Set> dirtyVars = new HashSet>(); + + Set> unsolvedVars = new HashSet>(); + + Set constraints = new HashSet(); + + ArrayList stack = new ArrayList(); + + boolean contradiction = false; - public void add(Constraint constraint) { - // TODO Auto-generated method stub - + static private class StackFrame { + Map, HashSet> invalidatedValues = new HashMap, HashSet>(); + Var branchVar; + Object branchValue; + + public void invalidate(Var var, T invalid) { + HashSet values = (HashSet) invalidatedValues.get(var); + if (values == null) { + invalidatedValues.put(var, + new HashSet(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> 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) var, value); + } + + void branchWith(Var 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); + } + + void logInvalidation(Var 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, HashSet> entry : item.invalidatedValues + .entrySet()) { + Var var = (Var) entry.getKey(); + HashSet values = (HashSet) 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) topFrame.branchVar).invalidate(topFrame.branchValue); + } + + // factory methods for vars + + public Var makeRangeVar(int low, int high) { + ArrayList range = new ArrayList(); + for (int i = low; i <= high; i++) { + range.add(i); + } + return makeVar(range); + } + + public Var makeBoolVar() { + return makeVar(true, false); } - public void push() { - // TODO Auto-generated method stub - + public Var makeVar(Collection range) { + Var var = new Var(this, range); + addVar(var); + return var; } - public void pop() { - // TODO Auto-generated method stub - + public Var 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 onTable = + * tisch ? {true}, {true, false} Var value = {N} Var + * color = {C} Var nachbarL,R = {-1, 0...steinanzahl} Var + * 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 pos von {links, rechts} + constraints + * + * links + rechts >= 3 + * + * foreach handstein: Var badness = onTable ? ### (z. B. 1) : 0 + * + * totalBadness = sum(all badness) + * + * foreach joker: Var value = {-1, 1..13} Var 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 { - Set range; - + private Solver solver; + private HashSet range; + public Var(Solver solver, Collection range) { + this.solver = solver; this.range = new HashSet(range); } - public static Var 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 getRange() { + return range; + } + + public void choose(T value) { + for (Iterator 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 iterator() { + final Iterator iterator = range.iterator(); + return new Iterator() { + 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 implements Constraint { + Var x, y; + Comparator comparator, reverseComparator; + ComparatorPropagator trueX, trueY, falseX, falseY; + boolean allowEqual; + + ComparatorConstraint(final Comparator comparator, boolean allowEqual, Var x, Var y) { + this.x = x; + this.y = y; + this.comparator = comparator; + this.allowEqual = allowEqual; + reverseComparator = new Comparator() { + @Override + public int compare(T o1, T o2) { + return comparator.compare(o2, o1); + } + }; + trueX = new ComparatorPropagator(comparator, allowEqual, x, y); + trueY = new ComparatorPropagator(reverseComparator, allowEqual, y, x); + falseX = new ComparatorPropagator(reverseComparator, !allowEqual, x, y); + falseY = new ComparatorPropagator(comparator, !allowEqual, y, x); + } + + @Override + public Collection> getWatchedVars() { + return Arrays.>asList(x,y); + } + + @Override + public Collection getPropagators(boolean negate) { + if (negate) { + return Arrays.asList(falseX,falseY); + } else { + return Arrays.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 implements Propagator { + private Var x, y; + private Comparator comparator; + private boolean allowEqual; + public ComparatorPropagator(Comparator comparator, boolean allowEqual, Var x, Var y) { + this.comparator = comparator; + this.allowEqual = allowEqual; + this.x = x; + this.y = y; + } + + @Override + public Collection> getWatchedVars() { + return Arrays.>asList(y); + } + + @Override + public void propagate() { + T maxY = Collections.max(y.getRange(), comparator); + + for(Iterator 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 { + 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 implements Constraint { + private Var var; + private Propagator trueProp, falseProp; + private Filter filter; + + public FilterConstraint(final Filter filter, Var var) { + this.var = var; + this.filter = filter; + trueProp = new FilterPropagator(filter, var); + falseProp = new FilterPropagator(new Filter() { + @Override + public boolean accept(T value) { + return !filter.accept(value); + } + }, var); + } + + @Override + public Collection> getWatchedVars() { + return Arrays.> asList(var); + } + + @Override + public Collection 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 implements Propagator { + private Filter filter; + private Var var; + + public FilterPropagator(Filter filter, Var var) { + this.filter = filter; + this.var = var; + } + + @Override + public Collection> getWatchedVars() { + return Arrays.>asList(var); + } + + @Override + public void propagate() { + for(Iterator 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> extends + ComparatorConstraint { + + public GreaterThan(boolean allowEqual, Var x, Var y) { + super(new Comparator() { + @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> extends + FilterConstraint { + public GreaterThanConst(final boolean allowEqual, Var x, final T y) { + super(new Filter() { + @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> extends ComparatorConstraint { + + public LessThan(boolean allowEqual, Var x, Var y) { + super(new Comparator() { + @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> extends FilterConstraint { + public LessThanConst(final boolean allowEqual, Var x, final T y) { + super(new Filter() { + @Override + public boolean accept(T value) { + return value.compareTo(y) < (allowEqual ? 1 : 0); + } + }, x); + } +} -- cgit v1.2.3