Several speed optimizations
git-svn-id: svn://sunsvr01.isp.uni-luebeck.de/swproj13/trunk@438 72836036-5685-4462-b002-a69064685172
This commit is contained in:
parent
0a63df955e
commit
99c3d48f10
9 changed files with 130 additions and 84 deletions
|
@ -1,5 +1,15 @@
|
||||||
package jrummikub.ai;
|
package jrummikub.ai;
|
||||||
|
|
||||||
|
import static jrummikub.ai.fdsolver.Constraints.constant;
|
||||||
|
import static jrummikub.ai.fdsolver.Constraints.index;
|
||||||
|
import static jrummikub.ai.fdsolver.Constraints.lessThan;
|
||||||
|
import static jrummikub.ai.fdsolver.Constraints.lessThanEq;
|
||||||
|
import static jrummikub.ai.fdsolver.Constraints.offset;
|
||||||
|
import static jrummikub.ai.fdsolver.Constraints.same;
|
||||||
|
import static jrummikub.ai.fdsolver.Constraints.sum;
|
||||||
|
import static jrummikub.ai.fdsolver.Constraints.unless;
|
||||||
|
import static jrummikub.ai.fdsolver.Constraints.when;
|
||||||
|
|
||||||
import java.util.ArrayList;
|
import java.util.ArrayList;
|
||||||
import java.util.Collection;
|
import java.util.Collection;
|
||||||
import java.util.HashSet;
|
import java.util.HashSet;
|
||||||
|
@ -9,13 +19,9 @@ import java.util.Set;
|
||||||
import jrummikub.ai.fdsolver.Constraint;
|
import jrummikub.ai.fdsolver.Constraint;
|
||||||
import jrummikub.ai.fdsolver.Solver;
|
import jrummikub.ai.fdsolver.Solver;
|
||||||
import jrummikub.ai.fdsolver.Var;
|
import jrummikub.ai.fdsolver.Var;
|
||||||
import jrummikub.ai.fdsolver.constraint.IfConstraint;
|
|
||||||
import jrummikub.ai.fdsolver.constraint.IndexConstraint;
|
|
||||||
import jrummikub.ai.fdsolver.constraint.LessThan;
|
|
||||||
import jrummikub.model.GameSettings;
|
import jrummikub.model.GameSettings;
|
||||||
import jrummikub.model.Stone;
|
import jrummikub.model.Stone;
|
||||||
import jrummikub.model.StoneColor;
|
import jrummikub.model.StoneColor;
|
||||||
import static jrummikub.ai.fdsolver.Constraints.*;
|
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Provides Humanlike Advanced Logic (HAL) that models the options given to a
|
* Provides Humanlike Advanced Logic (HAL) that models the options given to a
|
||||||
|
|
|
@ -10,4 +10,8 @@ public abstract class Constraint {
|
||||||
public abstract Collection<Propagator> getPropagators(boolean negate);
|
public abstract Collection<Propagator> getPropagators(boolean negate);
|
||||||
|
|
||||||
public abstract Satisfiability getSatisfiability();
|
public abstract Satisfiability getSatisfiability();
|
||||||
|
|
||||||
|
public boolean isSatisfiable() {
|
||||||
|
return getSatisfiability() != Satisfiability.UNSAT;
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -7,6 +7,7 @@ import java.util.Collections;
|
||||||
import java.util.HashMap;
|
import java.util.HashMap;
|
||||||
import java.util.HashSet;
|
import java.util.HashSet;
|
||||||
import java.util.Iterator;
|
import java.util.Iterator;
|
||||||
|
import java.util.List;
|
||||||
import java.util.Map;
|
import java.util.Map;
|
||||||
import java.util.Set;
|
import java.util.Set;
|
||||||
import static jrummikub.ai.fdsolver.Satisfiability.*;
|
import static jrummikub.ai.fdsolver.Satisfiability.*;
|
||||||
|
@ -24,6 +25,8 @@ public class Solver {
|
||||||
|
|
||||||
Set<Constraint> constraints = new HashSet<Constraint>();
|
Set<Constraint> constraints = new HashSet<Constraint>();
|
||||||
|
|
||||||
|
Set<Constraint> dirtyConstraints = new HashSet<Constraint>();
|
||||||
|
|
||||||
ArrayList<StackFrame> stack = new ArrayList<StackFrame>();
|
ArrayList<StackFrame> stack = new ArrayList<StackFrame>();
|
||||||
|
|
||||||
boolean contradiction = false;
|
boolean contradiction = false;
|
||||||
|
@ -83,27 +86,19 @@ public class Solver {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
public void propagateOnce() {
|
public void propagateEach() {
|
||||||
Var<?> dirtyVar = Collections.min(dirtyVars);
|
List<Var<?>> oldDirtyVars = new ArrayList<Var<?>>(dirtyVars);
|
||||||
dirtyVars.remove(dirtyVar);
|
dirtyVars.clear();
|
||||||
outerLoop: for (Iterator<Constraint> i = dirtyVar.getConstraints()
|
Collections.sort(oldDirtyVars);
|
||||||
.iterator(); i.hasNext();) {
|
outerLoop: for(Var<?> dirtyVar : oldDirtyVars) {
|
||||||
Constraint constraint = i.next();
|
for (Constraint constraint : dirtyVar.getConstraints()) {
|
||||||
Satisfiability sat = constraint.getSatisfiability();
|
dirtyConstraints.add(constraint);
|
||||||
if (sat == UNSAT) {
|
for (Propagator propagator : constraint.cachedPropagators) {
|
||||||
contradiction = true;
|
if (propagator.getWatchedVars().contains(dirtyVar)) {
|
||||||
break;
|
propagator.propagate();
|
||||||
}
|
if (contradiction) {
|
||||||
if (sat == TAUT) {
|
break outerLoop;
|
||||||
i.remove();
|
}
|
||||||
finishedConstraint(constraint, dirtyVar);
|
|
||||||
continue;
|
|
||||||
}
|
|
||||||
for (Propagator propagator : constraint.cachedPropagators) {
|
|
||||||
if (propagator.getWatchedVars().contains(dirtyVar)) {
|
|
||||||
propagator.propagate();
|
|
||||||
if (contradiction) {
|
|
||||||
break outerLoop;
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -111,9 +106,31 @@ public class Solver {
|
||||||
}
|
}
|
||||||
|
|
||||||
public void propagateAll() {
|
public void propagateAll() {
|
||||||
|
int i = 0;
|
||||||
while (!(dirtyVars.isEmpty() || contradiction)) {
|
while (!(dirtyVars.isEmpty() || contradiction)) {
|
||||||
propagateOnce();
|
i++;
|
||||||
|
if (i == 50) {
|
||||||
|
cleanUpConstraints();
|
||||||
|
i = 0;
|
||||||
|
} else {
|
||||||
|
propagateEach();
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
cleanUpConstraints();
|
||||||
|
}
|
||||||
|
|
||||||
|
private void cleanUpConstraints() {
|
||||||
|
for (Constraint constraint : dirtyConstraints) {
|
||||||
|
Satisfiability sat = constraint.getSatisfiability();
|
||||||
|
if (sat == UNSAT) {
|
||||||
|
contradiction = true;
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
if (sat == TAUT) {
|
||||||
|
finishedConstraint(constraint, null);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
dirtyConstraints.clear();
|
||||||
}
|
}
|
||||||
|
|
||||||
public void addVar(Var<?> var) {
|
public void addVar(Var<?> var) {
|
||||||
|
|
|
@ -99,18 +99,12 @@ public class Var<T> implements Comparable<Var<T>> {
|
||||||
return constraints.size();
|
return constraints.size();
|
||||||
}
|
}
|
||||||
|
|
||||||
private double fitness() {
|
|
||||||
return range.size();//neighborCount();
|
|
||||||
}
|
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public int compareTo(Var<T> other) {
|
public int compareTo(Var<T> other) {
|
||||||
return ((Double)fitness()).compareTo(other.fitness());
|
|
||||||
/*
|
|
||||||
int rangeCompare = ((Integer)range.size()).compareTo(other.range.size());
|
int rangeCompare = ((Integer)range.size()).compareTo(other.range.size());
|
||||||
if (rangeCompare != 0)
|
if (rangeCompare != 0)
|
||||||
return rangeCompare;
|
return rangeCompare;
|
||||||
return -((Integer)neighborCount()).compareTo(other.neighborCount());*/
|
return -((Integer)neighborCount()).compareTo(other.neighborCount());
|
||||||
}
|
}
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
|
@ -6,6 +6,7 @@ import java.util.Arrays;
|
||||||
import java.util.Collection;
|
import java.util.Collection;
|
||||||
import java.util.Collections;
|
import java.util.Collections;
|
||||||
import java.util.Comparator;
|
import java.util.Comparator;
|
||||||
|
import java.util.NoSuchElementException;
|
||||||
|
|
||||||
import jrummikub.ai.fdsolver.Constraint;
|
import jrummikub.ai.fdsolver.Constraint;
|
||||||
import jrummikub.ai.fdsolver.Propagator;
|
import jrummikub.ai.fdsolver.Propagator;
|
||||||
|
@ -17,8 +18,9 @@ public class ComparatorConstraint<T> extends Constraint {
|
||||||
Comparator<T> comparator, reverseComparator;
|
Comparator<T> comparator, reverseComparator;
|
||||||
ComparatorPropagator<T> trueX, trueY, falseX, falseY;
|
ComparatorPropagator<T> trueX, trueY, falseX, falseY;
|
||||||
boolean allowEqual;
|
boolean allowEqual;
|
||||||
|
|
||||||
ComparatorConstraint(final Comparator<T> comparator, boolean allowEqual, Var<T> x, Var<T> y) {
|
ComparatorConstraint(final Comparator<T> comparator, boolean allowEqual,
|
||||||
|
Var<T> x, Var<T> y) {
|
||||||
this.x = x;
|
this.x = x;
|
||||||
this.y = y;
|
this.y = y;
|
||||||
this.comparator = comparator;
|
this.comparator = comparator;
|
||||||
|
@ -31,37 +33,42 @@ public class ComparatorConstraint<T> extends Constraint {
|
||||||
};
|
};
|
||||||
trueX = new ComparatorPropagator<T>(comparator, allowEqual, x, y);
|
trueX = new ComparatorPropagator<T>(comparator, allowEqual, x, y);
|
||||||
trueY = new ComparatorPropagator<T>(reverseComparator, allowEqual, y, x);
|
trueY = new ComparatorPropagator<T>(reverseComparator, allowEqual, y, x);
|
||||||
falseX = new ComparatorPropagator<T>(reverseComparator, !allowEqual, x, y);
|
falseX = new ComparatorPropagator<T>(reverseComparator, !allowEqual, x,
|
||||||
|
y);
|
||||||
falseY = new ComparatorPropagator<T>(comparator, !allowEqual, y, x);
|
falseY = new ComparatorPropagator<T>(comparator, !allowEqual, y, x);
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public Collection<Var<?>> getWatchedVars() {
|
public Collection<Var<?>> getWatchedVars() {
|
||||||
return Arrays.<Var<?>>asList(x,y);
|
return Arrays.<Var<?>> asList(x, y);
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public Collection<Propagator> getPropagators(boolean negate) {
|
public Collection<Propagator> getPropagators(boolean negate) {
|
||||||
if (negate) {
|
if (negate) {
|
||||||
return Arrays.<Propagator>asList(falseX,falseY);
|
return Arrays.<Propagator> asList(falseX, falseY);
|
||||||
} else {
|
} else {
|
||||||
return Arrays.<Propagator>asList(trueX,trueY);
|
return Arrays.<Propagator> asList(trueX, trueY);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public Satisfiability getSatisfiability() {
|
public Satisfiability getSatisfiability() {
|
||||||
T maxX = Collections.max(x.getRange(), comparator);
|
try {
|
||||||
T minY = Collections.min(y.getRange(), comparator);
|
T maxX = Collections.max(x.getRange(), comparator);
|
||||||
if (comparator.compare(maxX, minY) < (allowEqual ? 1 : 0)) {
|
T minY = Collections.min(y.getRange(), comparator);
|
||||||
return TAUT;
|
if (comparator.compare(maxX, minY) < (allowEqual ? 1 : 0)) {
|
||||||
}
|
return TAUT;
|
||||||
T minX = Collections.min(x.getRange(), comparator);
|
}
|
||||||
T maxY = Collections.max(y.getRange(), comparator);
|
T minX = Collections.min(x.getRange(), comparator);
|
||||||
if (comparator.compare(maxY, minX) < (allowEqual ? 0 : 1)) {
|
T maxY = Collections.max(y.getRange(), comparator);
|
||||||
|
if (comparator.compare(maxY, minX) < (allowEqual ? 0 : 1)) {
|
||||||
|
return UNSAT;
|
||||||
|
}
|
||||||
|
return SAT;
|
||||||
|
} catch (NoSuchElementException e) {
|
||||||
return UNSAT;
|
return UNSAT;
|
||||||
}
|
}
|
||||||
return SAT;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
|
@ -63,7 +63,7 @@ public class IfConstraint extends Constraint {
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public void propagate() {
|
public void propagate() {
|
||||||
if (child.getSatisfiability() == Satisfiability.UNSAT) {
|
if (!child.isSatisfiable()) {
|
||||||
condition.invalidate(!negateCond);
|
condition.invalidate(!negateCond);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -8,6 +8,8 @@ import java.util.HashSet;
|
||||||
import java.util.Iterator;
|
import java.util.Iterator;
|
||||||
import java.util.List;
|
import java.util.List;
|
||||||
|
|
||||||
|
import org.w3c.dom.ranges.Range;
|
||||||
|
|
||||||
import jrummikub.ai.fdsolver.Constraint;
|
import jrummikub.ai.fdsolver.Constraint;
|
||||||
import jrummikub.ai.fdsolver.Propagator;
|
import jrummikub.ai.fdsolver.Propagator;
|
||||||
import jrummikub.ai.fdsolver.Satisfiability;
|
import jrummikub.ai.fdsolver.Satisfiability;
|
||||||
|
@ -47,16 +49,16 @@ public class IndexConstraint<T> extends Constraint {
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public void propagate() {
|
public void propagate() {
|
||||||
HashSet<T> union = new HashSet<T>();
|
HashSet<T> invUnion = new HashSet<T>(target.getRange());
|
||||||
for (int i : index.getRange()) {
|
for (int i : index.getRange()) {
|
||||||
union.addAll(list.get(i).getRange());
|
invUnion.removeAll(list.get(i).getRange());
|
||||||
}
|
if (invUnion.isEmpty()) {
|
||||||
for (Iterator<T> i = target.iterator(); i.hasNext();) {
|
return;
|
||||||
T val = i.next();
|
|
||||||
if (!union.contains(val)) {
|
|
||||||
i.remove();
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
for (T val : invUnion) {
|
||||||
|
target.invalidate(val);
|
||||||
|
}
|
||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -70,9 +72,8 @@ public class IndexConstraint<T> extends Constraint {
|
||||||
public void propagate() {
|
public void propagate() {
|
||||||
for (Iterator<Integer> i = index.iterator(); i.hasNext();) {
|
for (Iterator<Integer> i = index.iterator(); i.hasNext();) {
|
||||||
int id = i.next();
|
int id = i.next();
|
||||||
HashSet<T> range = new HashSet<T>(target.getRange());
|
Var<T> item = list.get(id);
|
||||||
range.retainAll(list.get(id).getRange());
|
if (Collections.disjoint(item.getRange(), target.getRange())) {
|
||||||
if (range.isEmpty()) {
|
|
||||||
i.remove();
|
i.remove();
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -107,28 +108,33 @@ public class IndexConstraint<T> extends Constraint {
|
||||||
}
|
}
|
||||||
return Arrays.<Propagator> asList(new UnionProp(), new IndexProp(), new VarProp());
|
return Arrays.<Propagator> asList(new UnionProp(), new IndexProp(), new VarProp());
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public boolean isSatisfiable() {
|
||||||
|
for (int i : index.getRange()) {
|
||||||
|
if(!Collections.disjoint(list.get(i).getRange(), target.getRange())) {
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
return false;
|
||||||
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public Satisfiability getSatisfiability() {
|
public Satisfiability getSatisfiability() {
|
||||||
HashSet<T> union = new HashSet<T>();
|
boolean sat = isSatisfiable();
|
||||||
for (int i : index.getRange()) {
|
if (!sat) {
|
||||||
union.addAll(list.get(i).getRange());
|
|
||||||
}
|
|
||||||
boolean isSat = false;
|
|
||||||
for (T val : target.getRange()) {
|
|
||||||
if (union.contains(val)) {
|
|
||||||
isSat = true;
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (!isSat) {
|
|
||||||
return Satisfiability.UNSAT;
|
return Satisfiability.UNSAT;
|
||||||
} else {
|
}
|
||||||
if (union.size() == 1 && target.getRange().size() == 1) {
|
if (target.getRange().size() > 1)
|
||||||
return Satisfiability.TAUT;
|
return Satisfiability.SAT;
|
||||||
} else {
|
for (int i : index.getRange()) {
|
||||||
|
Var<T> var = list.get(i);
|
||||||
|
if (var.getRange().size() > 1)
|
||||||
|
return Satisfiability.SAT;
|
||||||
|
if(var.getValue() != target.getValue()) {
|
||||||
return Satisfiability.SAT;
|
return Satisfiability.SAT;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
return Satisfiability.TAUT;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -2,6 +2,7 @@ package jrummikub.ai.fdsolver.constraint;
|
||||||
|
|
||||||
import java.util.Arrays;
|
import java.util.Arrays;
|
||||||
import java.util.Collection;
|
import java.util.Collection;
|
||||||
|
import java.util.Collections;
|
||||||
import java.util.HashSet;
|
import java.util.HashSet;
|
||||||
import java.util.Iterator;
|
import java.util.Iterator;
|
||||||
|
|
||||||
|
@ -60,12 +61,24 @@ public class OffsetConstraint extends Constraint {
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public Satisfiability getSatisfiability() {
|
public Satisfiability getSatisfiability() {
|
||||||
HashSet<Integer> shiftedRange = new HashSet<Integer>();
|
boolean disjoint = true;
|
||||||
for (int val : x.getRange()) {
|
if (x.getRange().size() < y.getRange().size()) {
|
||||||
shiftedRange.add(val + offset);
|
for (int xv : x.getRange()) {
|
||||||
|
if (y.getRange().contains(xv + offset)) {
|
||||||
|
disjoint = false;
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
} else {
|
||||||
|
for (int yv : y.getRange()) {
|
||||||
|
if (x.getRange().contains(yv - offset)) {
|
||||||
|
disjoint = false;
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
shiftedRange.retainAll(y.getRange());
|
|
||||||
if (shiftedRange.isEmpty()) {
|
if (disjoint) {
|
||||||
return Satisfiability.UNSAT;
|
return Satisfiability.UNSAT;
|
||||||
} else if (x.getRange().size() == 1 && y.getRange().size() == 1) {
|
} else if (x.getRange().size() == 1 && y.getRange().size() == 1) {
|
||||||
return Satisfiability.TAUT;
|
return Satisfiability.TAUT;
|
||||||
|
|
|
@ -2,6 +2,7 @@ package jrummikub.ai.fdsolver.constraint;
|
||||||
|
|
||||||
import java.util.Arrays;
|
import java.util.Arrays;
|
||||||
import java.util.Collection;
|
import java.util.Collection;
|
||||||
|
import java.util.Collections;
|
||||||
import java.util.HashSet;
|
import java.util.HashSet;
|
||||||
import java.util.Iterator;
|
import java.util.Iterator;
|
||||||
|
|
||||||
|
@ -56,9 +57,7 @@ public class SameConstraint<T> extends Constraint {
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public Satisfiability getSatisfiability() {
|
public Satisfiability getSatisfiability() {
|
||||||
HashSet<T> range = new HashSet<T>(x.getRange());
|
if (Collections.disjoint(x.getRange(), y.getRange())) {
|
||||||
range.retainAll(y.getRange());
|
|
||||||
if (range.isEmpty()) {
|
|
||||||
return Satisfiability.UNSAT;
|
return Satisfiability.UNSAT;
|
||||||
} else if (x.getRange().size() == 1 && y.getRange().size() == 1) {
|
} else if (x.getRange().size() == 1 && y.getRange().size() == 1) {
|
||||||
return Satisfiability.TAUT;
|
return Satisfiability.TAUT;
|
||||||
|
|
Reference in a new issue