Added TurnLogic with rule variables and constraints
git-svn-id: svn://sunsvr01.isp.uni-luebeck.de/swproj13/trunk@436 72836036-5685-4462-b002-a69064685172
This commit is contained in:
parent
79767f762e
commit
7568f37824
9 changed files with 864 additions and 12 deletions
345
src/jrummikub/ai/TurnLogic.java
Normal file
345
src/jrummikub/ai/TurnLogic.java
Normal file
|
@ -0,0 +1,345 @@
|
||||||
|
package jrummikub.ai;
|
||||||
|
|
||||||
|
import java.util.ArrayList;
|
||||||
|
import java.util.Collection;
|
||||||
|
import java.util.HashSet;
|
||||||
|
import java.util.List;
|
||||||
|
import java.util.Set;
|
||||||
|
|
||||||
|
import jrummikub.ai.fdsolver.Constraint;
|
||||||
|
import jrummikub.ai.fdsolver.Solver;
|
||||||
|
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.Stone;
|
||||||
|
import jrummikub.model.StoneColor;
|
||||||
|
import static jrummikub.ai.fdsolver.Constraints.*;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Provides Humanlike Advanced Logic (HAL) that models the options given to a
|
||||||
|
* player in a turn to the Solver MCP.
|
||||||
|
*/
|
||||||
|
public class TurnLogic {
|
||||||
|
private Solver solver = new Solver();
|
||||||
|
private GameSettings settings;
|
||||||
|
private int stoneCount;
|
||||||
|
private int maxSetSize;
|
||||||
|
|
||||||
|
private Var<Boolean> trueVar;
|
||||||
|
|
||||||
|
private List<Var<Boolean>> onTable = new ArrayList<Var<Boolean>>();
|
||||||
|
|
||||||
|
private List<Var<Integer>> stoneValue = new ArrayList<Var<Integer>>();
|
||||||
|
private List<Var<Integer>> leftStoneValue = new ArrayList<Var<Integer>>();
|
||||||
|
private List<Var<Integer>> rightStoneValue = new ArrayList<Var<Integer>>();
|
||||||
|
|
||||||
|
private List<Var<StoneColor>> stoneColor = new ArrayList<Var<StoneColor>>();
|
||||||
|
private List<Var<StoneColor>> leftStoneColor = new ArrayList<Var<StoneColor>>();
|
||||||
|
private List<Var<StoneColor>> rightStoneColor = new ArrayList<Var<StoneColor>>();
|
||||||
|
|
||||||
|
private List<Var<Integer>> lowCount = new ArrayList<Var<Integer>>();
|
||||||
|
private List<Var<Integer>> leftLowCount = new ArrayList<Var<Integer>>();
|
||||||
|
private List<Var<Integer>> rightLowCount = new ArrayList<Var<Integer>>();
|
||||||
|
|
||||||
|
private List<Var<Integer>> highCount = new ArrayList<Var<Integer>>();
|
||||||
|
private List<Var<Integer>> leftHighCount = new ArrayList<Var<Integer>>();
|
||||||
|
private List<Var<Integer>> rightHighCount = new ArrayList<Var<Integer>>();
|
||||||
|
|
||||||
|
private List<Var<Integer>> setSize = new ArrayList<Var<Integer>>();
|
||||||
|
|
||||||
|
private List<Var<Boolean>> isRun = new ArrayList<Var<Boolean>>();
|
||||||
|
|
||||||
|
private List<Var<Integer>> leftNeighbor = new ArrayList<Var<Integer>>();
|
||||||
|
private List<Var<Integer>> rightNeighbor = new ArrayList<Var<Integer>>();
|
||||||
|
|
||||||
|
private List<Var<Integer>> stoneID = new ArrayList<Var<Integer>>();
|
||||||
|
|
||||||
|
private List<Var<Boolean>> hasLeftNeighbor = new ArrayList<Var<Boolean>>();
|
||||||
|
private List<Var<Boolean>> hasRightNeighbor = new ArrayList<Var<Boolean>>();
|
||||||
|
|
||||||
|
private List<Boolean> isJoker = new ArrayList<Boolean>();
|
||||||
|
|
||||||
|
public TurnLogic(GameSettings settings, Collection<Stone> tableStones,
|
||||||
|
Collection<Stone> handStones) {
|
||||||
|
this.settings = settings;
|
||||||
|
stoneCount = tableStones.size() + handStones.size();
|
||||||
|
maxSetSize = Math.max(settings.getHighestValue(), settings
|
||||||
|
.getStoneColors().size());
|
||||||
|
|
||||||
|
trueVar = solver.makeVar(true);
|
||||||
|
|
||||||
|
int i = 0;
|
||||||
|
for (Stone stone : tableStones) {
|
||||||
|
addStone(i, true, stone);
|
||||||
|
i++;
|
||||||
|
}
|
||||||
|
for (Stone stone : handStones) {
|
||||||
|
addStone(i, false, stone);
|
||||||
|
i++;
|
||||||
|
}
|
||||||
|
|
||||||
|
for (i = 0; i < stoneCount; i++) {
|
||||||
|
addConstraints(i);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
private void addStone(int i, boolean table, Stone stone) {
|
||||||
|
if (table) {
|
||||||
|
onTable.add(trueVar);
|
||||||
|
} else {
|
||||||
|
onTable.add(solver.makeBoolVar());
|
||||||
|
}
|
||||||
|
isJoker.add(stone.isJoker());
|
||||||
|
if (stone.isJoker()) {
|
||||||
|
stoneValue.add(solver.makeRangeVar(1, settings.getHighestValue()));
|
||||||
|
stoneColor.add(solver.makeVar(settings.getStoneColors()));
|
||||||
|
} else {
|
||||||
|
stoneValue.add(solver.makeVar(stone.getValue()));
|
||||||
|
stoneColor.add(solver.makeVar(stone.getColor()));
|
||||||
|
}
|
||||||
|
|
||||||
|
leftStoneValue.add(solver.makeRangeVar(1, settings.getHighestValue()));
|
||||||
|
rightStoneValue.add(solver.makeRangeVar(1, settings.getHighestValue()));
|
||||||
|
leftStoneColor.add(solver.makeVar(settings.getStoneColors()));
|
||||||
|
rightStoneColor.add(solver.makeVar(settings.getStoneColors()));
|
||||||
|
|
||||||
|
lowCount.add(solver.makeRangeVar(0, maxSetSize - 1));
|
||||||
|
leftLowCount.add(solver.makeRangeVar(0, maxSetSize - 1));
|
||||||
|
rightLowCount.add(solver.makeRangeVar(0, maxSetSize - 1));
|
||||||
|
|
||||||
|
highCount.add(solver.makeRangeVar(0, maxSetSize - 1));
|
||||||
|
leftHighCount.add(solver.makeRangeVar(0, maxSetSize - 1));
|
||||||
|
rightHighCount.add(solver.makeRangeVar(0, maxSetSize - 1));
|
||||||
|
|
||||||
|
setSize.add(solver.makeRangeVar(2, maxSetSize - 1));
|
||||||
|
|
||||||
|
isRun.add(solver.makeBoolVar());
|
||||||
|
|
||||||
|
leftNeighbor.add(solver.makeRangeVar(0, stoneCount - 1));
|
||||||
|
rightNeighbor.add(solver.makeRangeVar(0, stoneCount - 1));
|
||||||
|
|
||||||
|
stoneID.add(solver.makeVar(i));
|
||||||
|
|
||||||
|
hasLeftNeighbor.add(solver.makeBoolVar());
|
||||||
|
hasRightNeighbor.add(solver.makeBoolVar());
|
||||||
|
}
|
||||||
|
|
||||||
|
private void add(Constraint c) {
|
||||||
|
solver.addConstraint(c);
|
||||||
|
}
|
||||||
|
|
||||||
|
private void addConstraints(int i) {
|
||||||
|
// Linking of neighbors
|
||||||
|
add(when(hasLeftNeighbor.get(i),
|
||||||
|
index(stoneID.get(i), leftNeighbor.get(i), rightNeighbor)));
|
||||||
|
add(unless(hasLeftNeighbor.get(i), constant(leftNeighbor.get(i), 0)));
|
||||||
|
add(when(hasLeftNeighbor.get(i),
|
||||||
|
index(trueVar, leftNeighbor.get(i), hasRightNeighbor)));
|
||||||
|
add(when(hasRightNeighbor.get(i),
|
||||||
|
index(stoneID.get(i), rightNeighbor.get(i), leftNeighbor)));
|
||||||
|
add(unless(hasRightNeighbor.get(i), constant(rightNeighbor.get(i), 0)));
|
||||||
|
add(when(hasRightNeighbor.get(i),
|
||||||
|
index(trueVar, rightNeighbor.get(i), hasLeftNeighbor)));
|
||||||
|
// hand stones have no neighbors
|
||||||
|
add(unless(onTable.get(i), constant(hasLeftNeighbor.get(i), false)));
|
||||||
|
add(unless(onTable.get(i), constant(hasRightNeighbor.get(i), false)));
|
||||||
|
|
||||||
|
// low/high counts and size
|
||||||
|
add(unless(hasLeftNeighbor.get(i), constant(lowCount.get(i), 0)));
|
||||||
|
add(unless(hasRightNeighbor.get(i), constant(highCount.get(i), 0)));
|
||||||
|
|
||||||
|
add(when(hasLeftNeighbor.get(i),
|
||||||
|
index(leftLowCount.get(i), leftNeighbor.get(i), lowCount)));
|
||||||
|
add(unless(hasLeftNeighbor.get(i), constant(leftLowCount.get(i), 0)));
|
||||||
|
|
||||||
|
add(when(hasRightNeighbor.get(i),
|
||||||
|
index(rightLowCount.get(i), rightNeighbor.get(i), lowCount)));
|
||||||
|
add(unless(hasRightNeighbor.get(i), constant(rightLowCount.get(i), 0)));
|
||||||
|
|
||||||
|
add(when(hasLeftNeighbor.get(i),
|
||||||
|
index(leftHighCount.get(i), leftNeighbor.get(i), highCount)));
|
||||||
|
add(unless(hasLeftNeighbor.get(i), constant(leftHighCount.get(i), 0)));
|
||||||
|
|
||||||
|
add(when(hasRightNeighbor.get(i),
|
||||||
|
index(rightHighCount.get(i), rightNeighbor.get(i), highCount)));
|
||||||
|
add(unless(hasRightNeighbor.get(i), constant(rightHighCount.get(i), 0)));
|
||||||
|
|
||||||
|
add(when(hasLeftNeighbor.get(i),
|
||||||
|
index(setSize.get(i), leftNeighbor.get(i), setSize)));
|
||||||
|
|
||||||
|
add(when(hasRightNeighbor.get(i),
|
||||||
|
index(setSize.get(i), rightNeighbor.get(i), setSize)));
|
||||||
|
|
||||||
|
add(when(hasLeftNeighbor.get(i),
|
||||||
|
offset(1, leftLowCount.get(i), lowCount.get(i))));
|
||||||
|
add(when(hasRightNeighbor.get(i),
|
||||||
|
offset(1, lowCount.get(i), rightLowCount.get(i))));
|
||||||
|
|
||||||
|
add(when(hasRightNeighbor.get(i),
|
||||||
|
offset(1, rightHighCount.get(i), highCount.get(i))));
|
||||||
|
add(when(hasLeftNeighbor.get(i),
|
||||||
|
offset(1, highCount.get(i), leftHighCount.get(i))));
|
||||||
|
|
||||||
|
add(when(onTable.get(i),
|
||||||
|
sum(lowCount.get(i), highCount.get(i), setSize.get(i))));
|
||||||
|
|
||||||
|
add(unless(onTable.get(i), constant(setSize.get(i), 2)));
|
||||||
|
|
||||||
|
// set same rules
|
||||||
|
add(when(hasLeftNeighbor.get(i),
|
||||||
|
index(isRun.get(i), leftNeighbor.get(i), isRun)));
|
||||||
|
add(when(hasRightNeighbor.get(i),
|
||||||
|
index(isRun.get(i), rightNeighbor.get(i), isRun)));
|
||||||
|
|
||||||
|
add(unless(onTable.get(i), constant(isRun.get(i), false)));
|
||||||
|
|
||||||
|
// rule neighbors
|
||||||
|
add(when(hasLeftNeighbor.get(i),
|
||||||
|
index(leftStoneColor.get(i), leftNeighbor.get(i), stoneColor)));
|
||||||
|
add(unless(hasLeftNeighbor.get(i),
|
||||||
|
constant(leftStoneColor.get(i), StoneColor.RED)));
|
||||||
|
add(when(hasRightNeighbor.get(i),
|
||||||
|
index(rightStoneColor.get(i), rightNeighbor.get(i), stoneColor)));
|
||||||
|
add(unless(hasRightNeighbor.get(i),
|
||||||
|
constant(rightStoneColor.get(i), StoneColor.RED)));
|
||||||
|
|
||||||
|
add(when(hasLeftNeighbor.get(i),
|
||||||
|
index(leftStoneValue.get(i), leftNeighbor.get(i), stoneValue)));
|
||||||
|
add(unless(hasLeftNeighbor.get(i), constant(leftStoneValue.get(i), 1)));
|
||||||
|
add(when(hasRightNeighbor.get(i),
|
||||||
|
index(rightStoneValue.get(i), rightNeighbor.get(i), stoneValue)));
|
||||||
|
add(unless(hasRightNeighbor.get(i), constant(rightStoneValue.get(i), 1)));
|
||||||
|
// general rules
|
||||||
|
|
||||||
|
add(when(
|
||||||
|
hasLeftNeighbor.get(i),
|
||||||
|
when(isRun.get(i),
|
||||||
|
lessThanEq(leftStoneValue.get(i), stoneValue.get(i)))));
|
||||||
|
add(when(
|
||||||
|
hasRightNeighbor.get(i),
|
||||||
|
when(isRun.get(i),
|
||||||
|
lessThanEq(stoneValue.get(i), rightStoneValue.get(i)))));
|
||||||
|
|
||||||
|
add(when(
|
||||||
|
hasLeftNeighbor.get(i),
|
||||||
|
when(isRun.get(i),
|
||||||
|
lessThanEq(leftStoneColor.get(i), stoneColor.get(i)))));
|
||||||
|
add(when(
|
||||||
|
hasRightNeighbor.get(i),
|
||||||
|
when(isRun.get(i),
|
||||||
|
lessThanEq(stoneColor.get(i), rightStoneColor.get(i)))));
|
||||||
|
|
||||||
|
// run rules
|
||||||
|
|
||||||
|
add(when(
|
||||||
|
hasLeftNeighbor.get(i),
|
||||||
|
when(isRun.get(i),
|
||||||
|
offset(1, leftStoneValue.get(i), stoneValue.get(i)))));
|
||||||
|
add(when(
|
||||||
|
hasRightNeighbor.get(i),
|
||||||
|
when(isRun.get(i),
|
||||||
|
offset(1, stoneValue.get(i), rightStoneValue.get(i)))));
|
||||||
|
|
||||||
|
add(when(
|
||||||
|
hasLeftNeighbor.get(i),
|
||||||
|
when(isRun.get(i),
|
||||||
|
same(leftStoneColor.get(i), stoneColor.get(i)))));
|
||||||
|
add(when(
|
||||||
|
hasRightNeighbor.get(i),
|
||||||
|
when(isRun.get(i),
|
||||||
|
same(stoneColor.get(i), rightStoneColor.get(i)))));
|
||||||
|
|
||||||
|
// group rules
|
||||||
|
add(when(
|
||||||
|
hasLeftNeighbor.get(i),
|
||||||
|
unless(isRun.get(i),
|
||||||
|
same(leftStoneValue.get(i), stoneValue.get(i)))));
|
||||||
|
add(when(
|
||||||
|
hasRightNeighbor.get(i),
|
||||||
|
unless(isRun.get(i),
|
||||||
|
same(stoneValue.get(i), rightStoneValue.get(i)))));
|
||||||
|
|
||||||
|
add(when(
|
||||||
|
hasLeftNeighbor.get(i),
|
||||||
|
unless(isRun.get(i),
|
||||||
|
lessThan(leftStoneColor.get(i), stoneColor.get(i)))));
|
||||||
|
add(when(
|
||||||
|
hasRightNeighbor.get(i),
|
||||||
|
unless(isRun.get(i),
|
||||||
|
lessThan(stoneColor.get(i), rightStoneColor.get(i)))));
|
||||||
|
|
||||||
|
// joker defaulting
|
||||||
|
if (isJoker.get(i)) {
|
||||||
|
add(unless(onTable.get(i), constant(stoneValue.get(i), 1)));
|
||||||
|
add(unless(onTable.get(i),
|
||||||
|
constant(stoneColor.get(i), StoneColor.RED)));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
public boolean solve() {
|
||||||
|
Set<Integer> tableIDs = new HashSet<Integer>();
|
||||||
|
Set<Integer> leftIDs = new HashSet<Integer>();
|
||||||
|
boolean res = solver.solve();
|
||||||
|
if (!res)
|
||||||
|
return false;
|
||||||
|
System.out.println("== Hand ==");
|
||||||
|
for (int i = 0; i < stoneCount; i++) {
|
||||||
|
if (onTable.get(i).getValue()) {
|
||||||
|
tableIDs.add(i);
|
||||||
|
if (!hasLeftNeighbor.get(i).getValue()) {
|
||||||
|
leftIDs.add(i);
|
||||||
|
}
|
||||||
|
} else {
|
||||||
|
outputStone(i);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
System.out.println("");
|
||||||
|
System.out.println("== Table ==");
|
||||||
|
boolean newLine = false;
|
||||||
|
boolean first = true;
|
||||||
|
int nextID = -1; // leftIDs.iterator().next();
|
||||||
|
while (!tableIDs.isEmpty()) {
|
||||||
|
if (tableIDs.contains(nextID)) {
|
||||||
|
tableIDs.remove(nextID);
|
||||||
|
leftIDs.remove(nextID);
|
||||||
|
if (newLine) {
|
||||||
|
if (!first) {
|
||||||
|
System.out.println("");
|
||||||
|
}
|
||||||
|
first = false;
|
||||||
|
newLine = false;
|
||||||
|
}
|
||||||
|
outputStone(nextID);
|
||||||
|
if (!hasRightNeighbor.get(nextID).getValue()) {
|
||||||
|
newLine = true;
|
||||||
|
nextID = -1;
|
||||||
|
} else {
|
||||||
|
nextID = rightNeighbor.get(nextID).getValue();
|
||||||
|
}
|
||||||
|
} else {
|
||||||
|
if (leftIDs.isEmpty()) {
|
||||||
|
nextID = tableIDs.iterator().next();
|
||||||
|
} else {
|
||||||
|
nextID = leftIDs.iterator().next();
|
||||||
|
}
|
||||||
|
newLine = true;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
System.out.println("");
|
||||||
|
System.out.println("");
|
||||||
|
return res;
|
||||||
|
}
|
||||||
|
|
||||||
|
private void outputStone(int i) {
|
||||||
|
System.out.print("["
|
||||||
|
+ stoneColor.get(i).getValue().toString().substring(0, 1)
|
||||||
|
+ stoneValue.get(i).getValue() + "]");
|
||||||
|
// + "," + leftNeighbor.get(i).getValue() +
|
||||||
|
// hasLeftNeighbor.get(i).getValue() + lowCount.get(i).getValue() + ","
|
||||||
|
// + rightNeighbor.get(i).getValue() +
|
||||||
|
// hasRightNeighbor.get(i).getValue() + highCount.get(i).getValue() +
|
||||||
|
// "]");
|
||||||
|
}
|
||||||
|
}
|
56
src/jrummikub/ai/fdsolver/Constraints.java
Normal file
56
src/jrummikub/ai/fdsolver/Constraints.java
Normal file
|
@ -0,0 +1,56 @@
|
||||||
|
package jrummikub.ai.fdsolver;
|
||||||
|
|
||||||
|
import java.util.List;
|
||||||
|
|
||||||
|
import jrummikub.ai.fdsolver.constraint.Filter;
|
||||||
|
import jrummikub.ai.fdsolver.constraint.FilterConstraint;
|
||||||
|
import jrummikub.ai.fdsolver.constraint.IfConstraint;
|
||||||
|
import jrummikub.ai.fdsolver.constraint.IndexConstraint;
|
||||||
|
import jrummikub.ai.fdsolver.constraint.LessThan;
|
||||||
|
import jrummikub.ai.fdsolver.constraint.OffsetConstraint;
|
||||||
|
import jrummikub.ai.fdsolver.constraint.SameConstraint;
|
||||||
|
import jrummikub.ai.fdsolver.constraint.SumConstraint;
|
||||||
|
|
||||||
|
public class Constraints {
|
||||||
|
public static Constraint when(Var<Boolean> cond, Constraint c) {
|
||||||
|
return new IfConstraint(false, cond, c);
|
||||||
|
}
|
||||||
|
|
||||||
|
public static Constraint unless(Var<Boolean> cond, Constraint c) {
|
||||||
|
return new IfConstraint(true, cond, c);
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
public static <T> Constraint index(Var<T> target, Var<Integer> index, List<Var<T>> list) {
|
||||||
|
return new IndexConstraint<T>(target, index, list);
|
||||||
|
}
|
||||||
|
|
||||||
|
public static <T> Constraint constant(Var<T> target, final T constant) {
|
||||||
|
return new FilterConstraint<T>(new Filter<T>() {
|
||||||
|
@Override
|
||||||
|
public boolean accept(T value) {
|
||||||
|
return value.equals(constant);
|
||||||
|
}
|
||||||
|
}, target);
|
||||||
|
}
|
||||||
|
|
||||||
|
public static Constraint offset(int offset, Var<Integer> x, Var<Integer> y) {
|
||||||
|
return new OffsetConstraint(offset, x, y);
|
||||||
|
}
|
||||||
|
|
||||||
|
public static <T> Constraint same(Var<T> x, Var<T> y) {
|
||||||
|
return new SameConstraint<T>(x, y);
|
||||||
|
}
|
||||||
|
|
||||||
|
public static Constraint sum(Var<Integer> x, Var<Integer> y, Var<Integer> z) {
|
||||||
|
return new SumConstraint(x, y, z);
|
||||||
|
}
|
||||||
|
|
||||||
|
public static <T extends Comparable<T>> Constraint lessThan(Var<T> x, Var<T> y) {
|
||||||
|
return new LessThan<T>(false, x, y);
|
||||||
|
}
|
||||||
|
|
||||||
|
public static <T extends Comparable<T>> Constraint lessThanEq(Var<T> x, Var<T> y) {
|
||||||
|
return new LessThan<T>(true, x, y);
|
||||||
|
}
|
||||||
|
}
|
|
@ -11,6 +11,10 @@ import java.util.Map;
|
||||||
import java.util.Set;
|
import java.util.Set;
|
||||||
import static jrummikub.ai.fdsolver.Satisfiability.*;
|
import static jrummikub.ai.fdsolver.Satisfiability.*;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* The Solver class is the Main Constraint Propagator (MCP) that tries to find a
|
||||||
|
* labeling of all variables that satisfies all given constraints.
|
||||||
|
*/
|
||||||
public class Solver {
|
public class Solver {
|
||||||
Set<Var<?>> vars = new HashSet<Var<?>>();
|
Set<Var<?>> vars = new HashSet<Var<?>>();
|
||||||
|
|
||||||
|
@ -80,9 +84,10 @@ public class Solver {
|
||||||
}
|
}
|
||||||
|
|
||||||
public void propagateOnce() {
|
public void propagateOnce() {
|
||||||
Var<?> dirtyVar = Collections.max(dirtyVars);
|
Var<?> dirtyVar = Collections.min(dirtyVars);
|
||||||
dirtyVars.remove(dirtyVar);
|
dirtyVars.remove(dirtyVar);
|
||||||
outerLoop: for (Iterator<Constraint> i = dirtyVar.getConstraints().iterator(); i.hasNext();) {
|
outerLoop: for (Iterator<Constraint> i = dirtyVar.getConstraints()
|
||||||
|
.iterator(); i.hasNext();) {
|
||||||
Constraint constraint = i.next();
|
Constraint constraint = i.next();
|
||||||
Satisfiability sat = constraint.getSatisfiability();
|
Satisfiability sat = constraint.getSatisfiability();
|
||||||
if (sat == UNSAT) {
|
if (sat == UNSAT) {
|
||||||
|
@ -130,14 +135,14 @@ public class Solver {
|
||||||
// backtracking and logging
|
// backtracking and logging
|
||||||
|
|
||||||
void branch() {
|
void branch() {
|
||||||
branchOn(unsolvedVars.iterator().next());
|
branchOn(Collections.min(unsolvedVars));
|
||||||
}
|
}
|
||||||
|
|
||||||
@SuppressWarnings("unchecked")
|
@SuppressWarnings("unchecked")
|
||||||
void branchOn(Var<?> var) {
|
void branchOn(Var<?> var) {
|
||||||
|
|
||||||
Set<?> range = var.getRange();
|
Set<?> range = var.getRange();
|
||||||
int n = (int)(Math.random() * range.size());
|
int n = (int) (Math.random() * range.size());
|
||||||
Iterator<?> it = range.iterator();
|
Iterator<?> it = range.iterator();
|
||||||
for (int i = 0; i < n; i++) {
|
for (int i = 0; i < n; i++) {
|
||||||
it.next();
|
it.next();
|
||||||
|
@ -230,13 +235,13 @@ public class Solver {
|
||||||
public <T> Var<T> makeVar(T... range) {
|
public <T> Var<T> makeVar(T... range) {
|
||||||
return makeVar(Arrays.asList(range));
|
return makeVar(Arrays.asList(range));
|
||||||
}
|
}
|
||||||
|
|
||||||
public void record() {
|
public void record() {
|
||||||
for (Var<?> var : vars) {
|
for (Var<?> var : vars) {
|
||||||
var.record();
|
var.record();
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
public void restore() {
|
public void restore() {
|
||||||
for (Var<?> var : vars) {
|
for (Var<?> var : vars) {
|
||||||
var.restore();
|
var.restore();
|
||||||
|
|
|
@ -38,7 +38,7 @@ public class Var<T> implements Comparable<Var<T>> {
|
||||||
this.solver.dirtyVars.add(this);
|
this.solver.dirtyVars.add(this);
|
||||||
}
|
}
|
||||||
|
|
||||||
void invalidate(T value) {
|
public void invalidate(T value) {
|
||||||
range.remove(value);
|
range.remove(value);
|
||||||
solver.logInvalidation(this, value);
|
solver.logInvalidation(this, value);
|
||||||
makeDirty();
|
makeDirty();
|
||||||
|
@ -92,19 +92,25 @@ public class Var<T> implements Comparable<Var<T>> {
|
||||||
}
|
}
|
||||||
|
|
||||||
private int neighborCount() {
|
private int neighborCount() {
|
||||||
int count = 0;
|
/* int count = 0;
|
||||||
for (Constraint constraint : constraints) {
|
for (Constraint constraint : constraints) {
|
||||||
count += constraint.getWatchedVars().size();
|
count += constraint.getWatchedVars().size();
|
||||||
}
|
} */
|
||||||
return count;
|
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());*/
|
||||||
}
|
}
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
108
src/jrummikub/ai/fdsolver/constraint/IfConstraint.java
Normal file
108
src/jrummikub/ai/fdsolver/constraint/IfConstraint.java
Normal file
|
@ -0,0 +1,108 @@
|
||||||
|
package jrummikub.ai.fdsolver.constraint;
|
||||||
|
|
||||||
|
import java.util.ArrayList;
|
||||||
|
import java.util.Collection;
|
||||||
|
import java.util.List;
|
||||||
|
import java.util.concurrent.locks.Condition;
|
||||||
|
|
||||||
|
|
||||||
|
import jrummikub.ai.fdsolver.Constraint;
|
||||||
|
import jrummikub.ai.fdsolver.Propagator;
|
||||||
|
import jrummikub.ai.fdsolver.Satisfiability;
|
||||||
|
import jrummikub.ai.fdsolver.Var;
|
||||||
|
|
||||||
|
public class IfConstraint implements Constraint {
|
||||||
|
Var<Boolean> condition;
|
||||||
|
Constraint child;
|
||||||
|
Collection<Var<?>> vars;
|
||||||
|
boolean negateCond;
|
||||||
|
|
||||||
|
public IfConstraint(boolean negateCond, Var<Boolean> condition, Constraint child) {
|
||||||
|
this.condition = condition;
|
||||||
|
this.child = child;
|
||||||
|
this.negateCond = negateCond;
|
||||||
|
vars = new ArrayList<Var<?>>();
|
||||||
|
vars.addAll(child.getWatchedVars());
|
||||||
|
vars.add(condition);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public Collection<Var<?>> getWatchedVars() {
|
||||||
|
return vars;
|
||||||
|
}
|
||||||
|
|
||||||
|
private class IfPropagator implements Propagator {
|
||||||
|
Propagator child;
|
||||||
|
Collection<Var<?>> vars;
|
||||||
|
public IfPropagator(Propagator child) {
|
||||||
|
this.child = child;
|
||||||
|
vars = new ArrayList<Var<?>>();
|
||||||
|
vars.addAll(child.getWatchedVars());
|
||||||
|
vars.add(condition);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public Collection<Var<?>> getWatchedVars() {
|
||||||
|
return vars;
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public void propagate() {
|
||||||
|
if(condition.getRange().contains(negateCond)) {
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
child.propagate();
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
private class FailPropagator implements Propagator {
|
||||||
|
@Override
|
||||||
|
public Collection<Var<?>> getWatchedVars() {
|
||||||
|
return child.getWatchedVars();
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public void propagate() {
|
||||||
|
if (child.getSatisfiability() == Satisfiability.UNSAT) {
|
||||||
|
condition.invalidate(!negateCond);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public Collection<Propagator> getPropagators(boolean negate) {
|
||||||
|
List<Propagator> props = new ArrayList<Propagator>();
|
||||||
|
if (negate) {
|
||||||
|
props.add(new FilterPropagator<Boolean>(new Filter<Boolean>() {
|
||||||
|
@Override
|
||||||
|
public boolean accept(Boolean value) {
|
||||||
|
return value ^ negateCond;
|
||||||
|
}
|
||||||
|
}, condition));
|
||||||
|
props.addAll(child.getPropagators(true));
|
||||||
|
} else {
|
||||||
|
for (Propagator p : child.getPropagators(false)) {
|
||||||
|
props.add(new IfPropagator(p));
|
||||||
|
}
|
||||||
|
props.add(new FailPropagator());
|
||||||
|
}
|
||||||
|
return props;
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public Satisfiability getSatisfiability() {
|
||||||
|
if (condition.getRange().contains(negateCond)) {
|
||||||
|
if (condition.getRange().size() == 1) {
|
||||||
|
return Satisfiability.TAUT;
|
||||||
|
} else {
|
||||||
|
if (child.getSatisfiability() == Satisfiability.TAUT) {
|
||||||
|
return Satisfiability.TAUT;
|
||||||
|
} else {
|
||||||
|
return Satisfiability.SAT;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
return child.getSatisfiability();
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
134
src/jrummikub/ai/fdsolver/constraint/IndexConstraint.java
Normal file
134
src/jrummikub/ai/fdsolver/constraint/IndexConstraint.java
Normal file
|
@ -0,0 +1,134 @@
|
||||||
|
package jrummikub.ai.fdsolver.constraint;
|
||||||
|
|
||||||
|
import java.util.ArrayList;
|
||||||
|
import java.util.Arrays;
|
||||||
|
import java.util.Collection;
|
||||||
|
import java.util.Collections;
|
||||||
|
import java.util.HashSet;
|
||||||
|
import java.util.Iterator;
|
||||||
|
import java.util.List;
|
||||||
|
|
||||||
|
import jrummikub.ai.fdsolver.Constraint;
|
||||||
|
import jrummikub.ai.fdsolver.Propagator;
|
||||||
|
import jrummikub.ai.fdsolver.Satisfiability;
|
||||||
|
import jrummikub.ai.fdsolver.Var;
|
||||||
|
|
||||||
|
public class IndexConstraint<T> implements Constraint {
|
||||||
|
Var<T> target;
|
||||||
|
Var<Integer> index;
|
||||||
|
List<Var<T>> list;
|
||||||
|
Collection<Var<?>> vars = new ArrayList<Var<?>>();
|
||||||
|
Collection<Var<?>> varsNoTarget = new ArrayList<Var<?>>();
|
||||||
|
Collection<Var<?>> varsNoIndex = new ArrayList<Var<?>>();
|
||||||
|
|
||||||
|
public IndexConstraint(Var<T> target, Var<Integer> index, List<Var<T>> list) {
|
||||||
|
this.target = target;
|
||||||
|
this.index = index;
|
||||||
|
this.list = list;
|
||||||
|
vars.addAll(list);
|
||||||
|
vars.add(index);
|
||||||
|
vars.add(target);
|
||||||
|
varsNoTarget.addAll(list);
|
||||||
|
varsNoTarget.add(index);
|
||||||
|
varsNoIndex.addAll(list);
|
||||||
|
varsNoIndex.add(target);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public Collection<Var<?>> getWatchedVars() {
|
||||||
|
return vars;
|
||||||
|
}
|
||||||
|
|
||||||
|
private class UnionProp implements Propagator {
|
||||||
|
@Override
|
||||||
|
public Collection<Var<?>> getWatchedVars() {
|
||||||
|
return varsNoTarget;
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public void propagate() {
|
||||||
|
HashSet<T> union = new HashSet<T>();
|
||||||
|
for (int i : index.getRange()) {
|
||||||
|
union.addAll(list.get(i).getRange());
|
||||||
|
}
|
||||||
|
for (Iterator<T> i = target.iterator(); i.hasNext();) {
|
||||||
|
T val = i.next();
|
||||||
|
if (!union.contains(val)) {
|
||||||
|
i.remove();
|
||||||
|
}
|
||||||
|
}
|
||||||
|
};
|
||||||
|
}
|
||||||
|
|
||||||
|
private class IndexProp implements Propagator {
|
||||||
|
@Override
|
||||||
|
public Collection<Var<?>> getWatchedVars() {
|
||||||
|
return varsNoIndex;
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public void propagate() {
|
||||||
|
for (Iterator<Integer> i = index.iterator(); i.hasNext();) {
|
||||||
|
int id = i.next();
|
||||||
|
HashSet<T> range = new HashSet<T>(target.getRange());
|
||||||
|
range.retainAll(list.get(id).getRange());
|
||||||
|
if (range.isEmpty()) {
|
||||||
|
i.remove();
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
private class VarProp implements Propagator {
|
||||||
|
@Override
|
||||||
|
public Collection<Var<?>> getWatchedVars() {
|
||||||
|
return Arrays.asList(target, index);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public void propagate() {
|
||||||
|
if (index.getRange().size() != 1)
|
||||||
|
return;
|
||||||
|
int id = index.getValue();
|
||||||
|
Var<T> var = list.get(id);
|
||||||
|
for(Iterator<T> i = var.iterator(); i.hasNext();) {
|
||||||
|
if (!target.getRange().contains(i.next())) {
|
||||||
|
i.remove();
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public Collection<Propagator> getPropagators(boolean negate) {
|
||||||
|
if (negate) {
|
||||||
|
return Collections.emptyList();
|
||||||
|
}
|
||||||
|
return Arrays.<Propagator> asList(new UnionProp(), new IndexProp(), new VarProp());
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public Satisfiability getSatisfiability() {
|
||||||
|
HashSet<T> union = new HashSet<T>();
|
||||||
|
for (int i : index.getRange()) {
|
||||||
|
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;
|
||||||
|
} else {
|
||||||
|
if (union.size() == 1 && target.getRange().size() == 1) {
|
||||||
|
return Satisfiability.TAUT;
|
||||||
|
} else {
|
||||||
|
return Satisfiability.SAT;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
77
src/jrummikub/ai/fdsolver/constraint/OffsetConstraint.java
Normal file
77
src/jrummikub/ai/fdsolver/constraint/OffsetConstraint.java
Normal file
|
@ -0,0 +1,77 @@
|
||||||
|
package jrummikub.ai.fdsolver.constraint;
|
||||||
|
|
||||||
|
import java.util.Arrays;
|
||||||
|
import java.util.Collection;
|
||||||
|
import java.util.HashSet;
|
||||||
|
import java.util.Iterator;
|
||||||
|
|
||||||
|
import jrummikub.ai.fdsolver.Constraint;
|
||||||
|
import jrummikub.ai.fdsolver.Propagator;
|
||||||
|
import jrummikub.ai.fdsolver.Satisfiability;
|
||||||
|
import jrummikub.ai.fdsolver.Var;
|
||||||
|
|
||||||
|
public class OffsetConstraint implements Constraint {
|
||||||
|
private Var<Integer> x, y;
|
||||||
|
int offset;
|
||||||
|
Propagator propX, propY;
|
||||||
|
|
||||||
|
public OffsetConstraint(int offset, Var<Integer> x, Var<Integer> y) {
|
||||||
|
this.offset = offset;
|
||||||
|
this.x = x;
|
||||||
|
this.y = y;
|
||||||
|
propX = new OffsetProp(offset, x, y);
|
||||||
|
propY = new OffsetProp(-offset, y, x);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public Collection<Var<?>> getWatchedVars() {
|
||||||
|
return Arrays.<Var<?>> asList(x, y);
|
||||||
|
}
|
||||||
|
|
||||||
|
private class OffsetProp implements Propagator {
|
||||||
|
private Var<Integer> x, y;
|
||||||
|
private int offset;
|
||||||
|
public OffsetProp(int offset, Var<Integer> x, Var<Integer> y) {
|
||||||
|
this.offset = offset;
|
||||||
|
this.x = x;
|
||||||
|
this.y = y;
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public Collection<Var<?>> getWatchedVars() {
|
||||||
|
return Arrays.<Var<?>>asList(y);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public void propagate() {
|
||||||
|
for(Iterator<Integer> i = x.iterator(); i.hasNext();) {
|
||||||
|
if(!y.getRange().contains(i.next() + offset)) {
|
||||||
|
i.remove();
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public Collection<Propagator> getPropagators(boolean negate) {
|
||||||
|
return Arrays.asList(propX, propY);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public Satisfiability getSatisfiability() {
|
||||||
|
HashSet<Integer> shiftedRange = new HashSet<Integer>();
|
||||||
|
for (int val : x.getRange()) {
|
||||||
|
shiftedRange.add(val + offset);
|
||||||
|
}
|
||||||
|
shiftedRange.retainAll(y.getRange());
|
||||||
|
if (shiftedRange.isEmpty()) {
|
||||||
|
return Satisfiability.UNSAT;
|
||||||
|
} else if (x.getRange().size() == 1 && y.getRange().size() == 1) {
|
||||||
|
return Satisfiability.TAUT;
|
||||||
|
} else {
|
||||||
|
return Satisfiability.SAT;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
70
src/jrummikub/ai/fdsolver/constraint/SameConstraint.java
Normal file
70
src/jrummikub/ai/fdsolver/constraint/SameConstraint.java
Normal file
|
@ -0,0 +1,70 @@
|
||||||
|
package jrummikub.ai.fdsolver.constraint;
|
||||||
|
|
||||||
|
import java.util.Arrays;
|
||||||
|
import java.util.Collection;
|
||||||
|
import java.util.HashSet;
|
||||||
|
import java.util.Iterator;
|
||||||
|
|
||||||
|
import jrummikub.ai.fdsolver.Constraint;
|
||||||
|
import jrummikub.ai.fdsolver.Propagator;
|
||||||
|
import jrummikub.ai.fdsolver.Satisfiability;
|
||||||
|
import jrummikub.ai.fdsolver.Var;
|
||||||
|
|
||||||
|
public class SameConstraint<T> implements Constraint {
|
||||||
|
private Var<T> x, y;
|
||||||
|
Propagator propX, propY;
|
||||||
|
|
||||||
|
public SameConstraint(Var<T> x, Var<T> y) {
|
||||||
|
this.x = x;
|
||||||
|
this.y = y;
|
||||||
|
propX = new SameProp<T>(x, y);
|
||||||
|
propY = new SameProp<T>(y, x);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public Collection<Var<?>> getWatchedVars() {
|
||||||
|
return Arrays.<Var<?>> asList(x, y);
|
||||||
|
}
|
||||||
|
|
||||||
|
private class SameProp<T> implements Propagator {
|
||||||
|
private Var<T> x, y;
|
||||||
|
public SameProp(Var<T> x, Var<T> y) {
|
||||||
|
this.x = x;
|
||||||
|
this.y = y;
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public Collection<Var<?>> getWatchedVars() {
|
||||||
|
return Arrays.<Var<?>>asList(y);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public void propagate() {
|
||||||
|
for(Iterator<T> i = x.iterator(); i.hasNext();) {
|
||||||
|
if(!y.getRange().contains(i.next())) {
|
||||||
|
i.remove();
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public Collection<Propagator> getPropagators(boolean negate) {
|
||||||
|
return Arrays.asList(propX, propY);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public Satisfiability getSatisfiability() {
|
||||||
|
HashSet<T> range = new HashSet<T>(x.getRange());
|
||||||
|
range.retainAll(y.getRange());
|
||||||
|
if (range.isEmpty()) {
|
||||||
|
return Satisfiability.UNSAT;
|
||||||
|
} else if (x.getRange().size() == 1 && y.getRange().size() == 1) {
|
||||||
|
return Satisfiability.TAUT;
|
||||||
|
} else {
|
||||||
|
return Satisfiability.SAT;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
51
src/jrummikub/ai/fdsolver/constraint/SumConstraint.java
Normal file
51
src/jrummikub/ai/fdsolver/constraint/SumConstraint.java
Normal file
|
@ -0,0 +1,51 @@
|
||||||
|
package jrummikub.ai.fdsolver.constraint;
|
||||||
|
|
||||||
|
import java.util.Arrays;
|
||||||
|
import java.util.Collection;
|
||||||
|
import java.util.Collections;
|
||||||
|
import java.util.HashSet;
|
||||||
|
|
||||||
|
import jrummikub.ai.fdsolver.Constraint;
|
||||||
|
import jrummikub.ai.fdsolver.Propagator;
|
||||||
|
import jrummikub.ai.fdsolver.Satisfiability;
|
||||||
|
import jrummikub.ai.fdsolver.Var;
|
||||||
|
|
||||||
|
public class SumConstraint implements Constraint {
|
||||||
|
Var<Integer> x, y, z;
|
||||||
|
|
||||||
|
public SumConstraint(Var<Integer> x, Var<Integer> y, Var<Integer> z) {
|
||||||
|
this.x = x;
|
||||||
|
this.y = y;
|
||||||
|
this.z = z;
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public Collection<Var<?>> getWatchedVars() {
|
||||||
|
return Arrays.<Var<?>> asList(x, y, z);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public Collection<Propagator> getPropagators(boolean negate) {
|
||||||
|
// TODO Auto-generated method stub
|
||||||
|
return Collections.emptyList();
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public Satisfiability getSatisfiability() {
|
||||||
|
// HashSet<Integer> intersection = new HashSet<Integer>();
|
||||||
|
for (int xv : x.getRange()) {
|
||||||
|
for (int yv : y.getRange()) {
|
||||||
|
if (z.getRange().contains(xv + yv)) {
|
||||||
|
if (z.getRange().size() == 1 && x.getRange().size() == 1
|
||||||
|
&& y.getRange().size() == 1) {
|
||||||
|
return Satisfiability.TAUT;
|
||||||
|
} else {
|
||||||
|
return Satisfiability.SAT;
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
return Satisfiability.UNSAT;
|
||||||
|
}
|
||||||
|
}
|
Reference in a new issue