Generating intransitive dice using Z3¶

Intransitive dice are a set of dice where the usual order of winning is disrupted; for example, die A can beat die B, die B can beat die C, but die C can beat die A.

In this Julia notebook, the we'll use the Z3 theorem prover to generate a set of 3 intransitive dice.

Z3 is an efficient theorem prover developed by Microsoft Research. It's primarily used for checking the satisfiability of logical formulas over various theories, such as integers, real numbers, and arrays. In this notebook, the Satisfiability.jl package is used as interface between Julia and Z3.

In [1]:
using Satisfiability

The dice generated [dice_a, dice_b, dice_c], should be generated such that dice_a has advantage over dice_b, dice_b over dice_c, and dice_c over dice_a.

First generate the variables for Z3 to solve, in this case the face values for each dice. Each dice is represented as an array of integer variables, 1 variable for each face.

In [2]:
n_faces = 6

@satvariable(dice_a[1:n_faces], Int);
@satvariable(dice_b[1:n_faces], Int);
@satvariable(dice_c[1:n_faces], Int);

Now add the constraints. The first constraint makes sure that a face value is not used in multiple dice, making sure that there can't be ties when rolling 2 different dice.

In [3]:
constraint_no_ties = and(
    and([face_a != face_b for face_a in dice_a for face_b in dice_b]),
    and([face_b != face_c for face_b in dice_b for face_c in dice_c]),
    and([face_c != face_a for face_c in dice_c for face_a in dice_a]),
);

The next constraint limits the face values to "reasonable numbers". At most each face of each die would be different, so all face values can be limited between 1 and n_dice * n_faces_per_dice.

In [4]:
constraint_face_values = and(
    and([and(face >= 1, face <= (3 * n_faces)) for face in dice_a]),
    and([and(face >= 1, face <= (3 * n_faces)) for face in dice_b]),
    and([and(face >= 1, face <= (3 * n_faces)) for face in dice_c]),
);

Add a constraint that each dice's face number are in ascending order (not directly required, but nice or ascetics).

In [5]:
constraint_order = and(
    and([dice_a[n] <= dice_a[n+1] for n in 1:n_faces-1]),
    and([dice_b[n] <= dice_b[n+1] for n in 1:n_faces-1]),
    and([dice_c[n] <= dice_c[n+1] for n in 1:n_faces-1]),
);

Finally add the constraints that dice_a must win, on average, from dice_b, dice_b from dice_c, and dice_c from dice_a. We also want that all those odds are equal, for example not that dice_a would win 75% of the time from dice_b, but dice_b would win only 55% of the time from dice_c.

The odds of 1 dice vs another are calculated using the n_wins function. These odds are calculated by comparing each possible dice result between the 2 dice and counting the number of wins for the first dice.

We want to find a result with the highest odds between dice. The best odds possible would be n_faces^2, e.g. 36 (out of 36) for a 6-sided dice. Iteratively, with decreasing odds, we try to find a solution for the die faces, until a solution is found.

In [6]:
n_wins(dice_x, dice_y) = sum([face_x > face_y for face_x in dice_x for face_y in dice_y])

max_odds = Int(n_faces^2)
min_odds = Int(max_odds / 2)

for odds in max_odds:-1:min_odds
    constraint_odds = and(
        n_wins(dice_a, dice_b) == Int(odds),
        n_wins(dice_b, dice_c) == Int(odds),
        n_wins(dice_c, dice_a) == Int(odds),
    )
    status = sat!(constraint_no_ties, constraint_face_values, constraint_order, constraint_odds, solver=Z3())
    if status == :SAT
        println("odds: $(odds) out of $(max_odds)")
        println("dice_a = $(value(dice_a))")
        println("dice_b = $(value(dice_b))")
        println("dice_c = $(value(dice_c))")
        break
    end
end

odds: 21 out of 36
dice_a = [3, 3, 3, 5, 5, 8]
dice_b = [2, 2, 2, 7, 7, 7]
dice_c = [1, 4, 4, 6, 6, 6]

To show these dice actually have the properties we like to have:

dice_a vs dice_b: 21/36 wins:

↓ a | b → 2 2 2 7 7 7
3 + + + - - -
3 + + + - - -
3 + + + - - -
5 + + + - - -
5 + + + - - -
8 + + + + + +

dice_b vs dice_c: 21/26 wins:

↓ b | c → 1 4 4 6 6 6
2 + - - - - -
2 + - - - - -
2 + - - - - -
7 + + + + + +
7 + + + + + +
7 + + + + + +

dice_c vs dice_a: 21/36 wins:

↓ c | a → 3 3 3 5 5 8
1 - - - - - -
4 + + + - - -
4 + + + - - -
6 + + + + + -
6 + + + + + -
6 + + + + + -

Generating "Rock, Paper, Scissors, Lizard, Spock" dice¶

The previous example can be thought of as a set of "rock, paper, scissors" dice. Now we can take the same logic to try and generate a set of "Rock, Paper, Scissors, Lizard, Spock" dice.

5 dice are defined, and these dice should have the following odds against each other:

V Player | Opponent > dice_a dice_b dice_c dice_d dice_e
dice_a O + - + -
dice_b - O + - +
dice_c + - O + -
dice_d - + - O +
dice_e + - + - O
In [7]:
n_faces = 6

@satvariable(dice_a[1:n_faces], Int)
@satvariable(dice_b[1:n_faces], Int)
@satvariable(dice_c[1:n_faces], Int)
@satvariable(dice_d[1:n_faces], Int)
@satvariable(dice_e[1:n_faces], Int)

constraint_no_ties = and(
    and([face_a != face_b for face_a in dice_a for face_b in dice_b]),
    and([face_a != face_c for face_a in dice_a for face_c in dice_c]),
    and([face_a != face_d for face_a in dice_a for face_d in dice_d]),
    and([face_a != face_e for face_a in dice_a for face_e in dice_e]),
    and([face_b != face_c for face_b in dice_b for face_c in dice_c]),
    and([face_b != face_d for face_b in dice_b for face_d in dice_d]),
    and([face_b != face_e for face_b in dice_b for face_e in dice_e]),
    and([face_c != face_d for face_c in dice_c for face_d in dice_d]),
    and([face_c != face_e for face_c in dice_c for face_e in dice_e]),
    and([face_d != face_e for face_d in dice_d for face_e in dice_e]),
)

constraint_face_values = and(
    and([and(face >= 1, face <= (5 * n_faces)) for face in dice_a]),
    and([and(face >= 1, face <= (5 * n_faces)) for face in dice_b]),
    and([and(face >= 1, face <= (5 * n_faces)) for face in dice_c]),
    and([and(face >= 1, face <= (5 * n_faces)) for face in dice_d]),
    and([and(face >= 1, face <= (5 * n_faces)) for face in dice_e]),
)

constraint_order = and(
    and([dice_a[n] <= dice_a[n+1] for n in 1:n_faces-1]),
    and([dice_b[n] <= dice_b[n+1] for n in 1:n_faces-1]),
    and([dice_c[n] <= dice_c[n+1] for n in 1:n_faces-1]),
    and([dice_d[n] <= dice_d[n+1] for n in 1:n_faces-1]),
    and([dice_e[n] <= dice_e[n+1] for n in 1:n_faces-1]),
)

n_wins(dice_x, dice_y) = sum([face_x > face_y for face_x in dice_x for face_y in dice_y])

max_odds = Int(n_faces^2)
min_odds = Int(max_odds / 2)

for odds in max_odds:-1:min_odds
    constraint_odds = and(
        n_wins(dice_a, dice_b) == Int(odds),
        n_wins(dice_b, dice_c) == Int(odds),
        n_wins(dice_c, dice_d) == Int(odds),
        n_wins(dice_d, dice_e) == Int(odds),
        n_wins(dice_e, dice_a) == Int(odds),
        n_wins(dice_a, dice_d) == Int(odds),
        n_wins(dice_b, dice_e) == Int(odds),
        n_wins(dice_c, dice_a) == Int(odds),
        n_wins(dice_d, dice_b) == Int(odds),
        n_wins(dice_e, dice_c) == Int(odds),
    )
    status = sat!(constraint_no_ties, constraint_face_values, constraint_order, constraint_odds, solver=Z3())
    if status == :SAT
        println("odds: $(odds) out of $(max_odds)")
        println("dice_a = $(value(dice_a))")
        println("dice_b = $(value(dice_b))")
        println("dice_c = $(value(dice_c))")
        println("dice_d = $(value(dice_d))")
        println("dice_e = $(value(dice_e))")
        break
    end
end

odds: 20 out of 36
dice_a = [4, 4, 9, 9, 11, 11]
dice_b = [2, 2, 7, 7, 15, 15]
dice_c = [5, 5, 5, 5, 14, 14]
dice_d = [3, 3, 8, 8, 13, 13]
dice_e = [1, 6, 6, 10, 12, 12]