non-transitive-dices/src/main/java/fr/holt59/App.java

111 lines
4.0 KiB
Java

package fr.holt59;
import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.IOException;
import java.io.OutputStream;
import java.io.PrintStream;
import java.nio.file.Files;
import java.nio.file.Path;
import java.nio.file.Paths;
import java.util.Arrays;
import java.util.List;
import java.util.stream.IntStream;
import org.chocosolver.solver.Model;
import org.chocosolver.solver.Solution;
import org.chocosolver.solver.variables.BoolVar;
import org.chocosolver.solver.variables.IntVar;
/**
* Hello world!
*/
public class App {
public static class NonTransitiveDiceModel extends Model {
private final IntVar[][] dices;
public NonTransitiveDiceModel(final int nDices, final int nFaces) {
super("Non-Transitive Dices");
final int nVars = nDices * nFaces;
this.dices = IntStream.range(0, nDices)
.mapToObj(i -> IntStream.range(0, nFaces).mapToObj(
f -> this.intVar(String.format("x_%d_%d", i, f), 1, nVars))
.toArray(IntVar[]::new))
.toArray(IntVar[][]::new);
// values are used once each
this.allDifferent(Arrays.stream(dices).flatMap(dice -> Arrays.stream(dice))
.toArray(IntVar[]::new)).post();
// ordered values on each dice
for (final IntVar[] dice : dices) {
for (int iFace = 0; iFace < nFaces - 1; ++iFace) {
this.arithm(dice[iFace], "<", dice[iFace + 1]).post();
}
}
// avoid symmetric solutions
for (int iDice = 0; iDice < nDices - 1; ++iDice) {
this.arithm(dices[iDice][0], "<", dices[iDice + 1][0]).post();
}
// winning probabilities
for (int iDice = 0; iDice < nDices; ++iDice) {
final BoolVar[] winning = new BoolVar[nDices];
winning[iDice] = this.boolVar(false);
for (int otherDice = 0; otherDice < nDices; ++otherDice) {
if (otherDice == iDice) {
continue;
}
final BoolVar[] compare = IntStream.range(0, nFaces * nFaces)
.mapToObj(i -> this.boolVar()).toArray(BoolVar[]::new);
for (int iFace = 0; iFace < nFaces; ++iFace) {
for (int otherFace = 0; otherFace < nFaces; ++otherFace) {
this.reifyXleY(dices[otherDice][otherFace],
dices[iDice][iFace],
compare[iFace * nFaces + otherFace]);
}
}
winning[otherDice] =
this.sum(compare, ">", compare.length / 2).reify();
}
this.addClausesBoolOrArrayEqualTrue(winning);
}
}
public int[][] getDices(final Solution solution) {
return Arrays.stream(this.dices)
.map(dice -> Arrays.stream(dice)
.mapToInt(face -> solution.getIntVal(face)).toArray())
.toArray(int[][]::new);
}
}
public static void main(String[] args) throws IOException {
final int nDices = 3;
final int nFaces = 6;
final NonTransitiveDiceModel model = new NonTransitiveDiceModel(nDices, nFaces);
final List<Solution> solutions = model.getSolver().findAllSolutions();
System.out.println(String.format("Found %d solutions.", solutions.size()));
try (final PrintStream outputStream = new PrintStream(Files.newOutputStream(
Paths.get(String.format("./dices-%dx%d.txt", nDices, nFaces))))) {
for (final Solution solution : solutions) {
final int[][] dices = model.getDices(solution);
outputStream.println(String.join(", ", Arrays.stream(dices)
.map(Arrays::toString).toArray(String[]::new)));
}
}
}
}