flix-cube-solvers

Rubik's cube solving for Flix: a cube model, a solver contract, and a pocket cube engine whose distance table is a Datalog fixpoint and whose solutions are shortest.

The first consumer is wstein/flix-cube. This package exists to be depended on, so the contract is the product and the engines are implementations of it.

Status

Early, but the whole path works: stickers in, cubies, table, search, moves out.

Module	What it is	State
CubeSolvers	Faces, turns, moves, notation, inversion	Done
CubeSolvers.Solver	Facelets, Invalid, Options, Outcome, and the Solver trait	Done
CubeSolvers.Turning	Turning any cube at sticker level, 2x2 through 5x5	Done
CubeSolvers.Pocket	The 2x2x2 as cubies: permutation, twist, the three faces that turn	Done
CubeSolvers.Pocket.Stickers	Cubies to facelets and back	Done
CubeSolvers.Pocket.Search	Datalog distance table, and shortest solutions from it	Done
CubeSolvers.Pocket.Engine	A prepared solver; the first Solver instance	Done
CubeSolvers.Pocket.Scramble	Seeded uniform 2x2 random-state scrambles, with certified shortest length	Done
CubeSolvers.Rubik	The 3x3x3 as cubies: corners, edges, twists, flips, all six faces	Done
CubeSolvers.Rubik.Stickers	54 stickers to cubies and back, with the three laws	Done
CubeSolvers.Rubik.Coordinate	Twist, flip and slice as numbers, and the tables moves walk them through	Done
CubeSolvers.Rubik.Pruning	Exact distances in two coordinates at a time	Done
CubeSolvers.Rubik.Reduce	The search into the subgroup no side quarter turn is needed from	Done
CubeSolvers.Rubik.Finish	The finish, using only U, D and half turns	Done
CubeSolvers.Rubik.Engine	A prepared 3x3 solver; the second Solver instance	Done
CubeSolvers.Rubik.Easy	Compact exact-distance table through five 3x3 moves	Done
CubeSolvers.Rubik.Scramble	Secure random-state and exact shallow 3x3 scrambles	Done
CubeSolvers.Revenge.Centers	Tsai's first phase: R and L colours onto R and L	Done
CubeSolvers.Revenge.Separate	Tsai's second phase: the other centres, and where R/L may stop	Done
CubeSolvers.Revenge.Reduce	Tsai's third phase, centres half: 58,800 states	Done
CubeSolvers.Revenge.Wings	The 4x4 wings: which piece is where, and the permutation's parity	Done
CubeSolvers.Revenge.Corners	The 4x4 corners, for their permutation's parity	Done
CubeSolvers.Revenge.Pairs	How far the wings are from being paired, as one permutation of twelve	Done
CubeSolvers.Revenge.Walk	Walking a phase downhill through its table	Done
—	4x4 edge pairing, then the 3x3 finish and its parities	In progress
—	The 5x5	Not started

Checked against the Java implementation in wstein/cube-solvers, at two different levels:

• Solutions. Cubes written out here, solved there: the same lengths, and so far the same moves. Four are pinned in TestCrossCheck.
• Move semantics. test/fixtures/replay-vectors.tsv is generated by that repository's TCK oracle — a scramble and the stickers it produces from solved — and TestVectors replays all ten pocket and all five 3x3 vectors here and compares sticker for sticker. Agreeing on answers is not the same as agreeing on what the question said; this is where the second kind of disagreement would show. Every one of the fifteen matches.

Quick start

./flixw test         # 98 tests, about 15s: the tables are built and checked
./flixw check        # type-check; the fast loop
./flixw format       # reformat in place before committing

The only prerequisite is a JDK, Java 21 or newer. flixw fetches the compiler pinned in .flixw/lock.toml, verifies its SHA-256 and caches it outside the repository; see wstein/flixw.

What is in here

.
├── src/
│   ├── CubeSolvers.flix              the model: Kind, Face, Turn, Move, notation both ways
│   └── CubeSolvers/
│   │   ├── Solver.flix               the contract: Facelets, Invalid, Options, Outcome, Solver
│   │   ├── Pocket.flix               the 2x2x2 cubie model and its move tables
│   │   ├── Pocket/
│   │   │   ├── Stickers.flix         the facelet boundary, both directions
│   │   │   ├── Search.flix           the Datalog distance table and the search over it
│   │   │   ├── Coordinate.flix       states packed into one Int64, and what that buys
│   │   │   └── Engine.flix           a prepared solver, and the Solver instance
│   │   ├── Rubik.flix                the 3x3x3 cubie model and its move tables
│   │   └── Rubik/
│   │       ├── Stickers.flix         the 3x3 facelet boundary and the three laws
│   │       ├── Coordinate.flix       twist, flip and slice, and their move tables
│   │       ├── Pruning.flix          exact distances in two coordinates at a time
│   │       ├── Reduce.flix           the search into the subgroup
│   │       ├── Finish.flix           the finish inside it
│   │       └── Engine.flix           both phases, and the Solver instance
└── test/
    ├── TestCube.flix                 notation, inversion, depth rules
    ├── TestSolver.flix               what the validator can and cannot see
    ├── TestPocket.flix               move mechanics: orders, inverses, what is not a move
    ├── TestPocketStickers.flix       the round trip, and the states that are not cubes
    ├── TestPocketSearch.flix         table sizes against the published figures, and optimality
    ├── TestPocketCoordinate.flix     the packing is injective and agrees with the cubie table
    ├── TestPocketEngine.flix         the contract as a caller meets it
    ├── TestRubikCoordinate.flix      the tables agree with the cube, move for move
    ├── TestRubikEngine.flix          the 3x3 end to end
    ├── TestCrossCheck.flix           cubes solved no worse than another engine
    ├── TestVectors.flix              scrambles replayed against the Java oracle's own vectors
    └── fixtures/                     replay-vectors.tsv, shared with wstein/cube-solvers

Directories mirror module paths, which is what the rest of the Flix ecosystem does — flix-json has src/Json/FromJson.flix for Json.FromJson — and it is why no file needs a prefix to stay unique.

Solving one, end to end:

let stickers = "FUBRDRLBDFLDUFDLURLFBRUB"
    |> String.toList |> List.filterMap(CubeSolvers.faceOfToken) |> List.toVector;
match CubeSolvers.Solver.facelets(CubeSolvers.Kind.Cube2x2, stickers) {
    case Err(why) => ...                       // not a cube, and why
    case Ok(cube) =>
        let engine = CubeSolvers.Pocket.Engine.standard();
        CubeSolvers.Solver.search(engine, cube, CubeSolvers.Solver.defaultOptions())
        //=> Solved(R :: F2 :: U :: R' :: Nil)
}

2x2 random-state scrambles

CubeSolvers.Pocket.Scramble.wca produces a reproducible 2x2 scramble from a caller-provided seed. It samples uniformly from the fixed-corner state space, rejects states solvable in fewer than four moves, and returns the reverse of the exact solver's shortest route. The output is therefore guaranteed to be a shortest scramble for its resulting state.

let engine = CubeSolvers.Pocket.Engine.standard();
let (scramble, nextSeed) = CubeSolvers.Pocket.Scramble.wca(engine, 42i64);
CubeSolvers.render(scramble)

This matches the WCA's random-state and minimum-distance requirement for 2x2, but it is not an official WCA scramble program. Official competitions must use the current TNoodle release.

For deliberately easier practice, choose an exact proven distance, or have the library choose uniformly from three, four, and five moves:

let (scramble, nextSeed) = CubeSolvers.Pocket.Scramble.easy(42i64);
// `List.length(scramble)` is exactly 3, 4, or 5 -- never just a literal count.

For actual use, prefer entropy from SecureRandom rather than choosing a seed yourself:

let scramble = CubeSolvers.Pocket.Scramble.secureEasy(); // \ IO

3x3 random-state scrambles

CubeSolvers.Rubik.Scramble.secure samples a legal 3x3 state with SecureRandom, rejects the solved and one-move states, and uses the prepared two-phase engine to render a sequence that reaches it:

let engine = CubeSolvers.Rubik.Engine.prepared();
let scramble = CubeSolvers.Rubik.Scramble.secure(engine); // \ IO

The state distribution fulfils the WCA minimum-distance rule, but the 3x3 engine is deliberately not optimal, so its printed sequence is not certified shortest. As with 2x2, official WCA competitions must use TNoodle.

Proven 3x3 easy scrambles

CubeSolvers.Rubik.Easy.standard() builds the complete half-turn-metric table through five moves: 621,649 states in total, including 3,240 states at three moves, 43,239 at four, and 574,908 at five. It retains compact permutation-orientation keys, not whole cubie vectors. Prepare it once, then draw as many certified-minimum scrambles as needed:

let table = CubeSolvers.Rubik.Easy.standard();
let scramble = CubeSolvers.Rubik.Scramble.secureEasy(table); // \ IO
// The resulting state is exactly 3, 4, or 5 moves from solved.

For reproducible output, use Scramble.atDistance(table, seed, distance) or Scramble.easy(table, seed), each returning the next seed with its scramble.

The model

Move is a face, a depth and a turn. Depth counts layers from the face, so depth = 1 is the outer layer and depth = 2 is the Uw of standard notation. A depth that reaches the far face turns the whole cube, which is a rotation and not a move — CubeSolvers.validate rejects it, and it needs the Kind to know where that line falls.

Turn has three cases and no identity: a turn that changes nothing is not a turn. The same reasoning puts the size inside Kind rather than beside it, so an unsupported cube cannot be constructed and then rejected later.

Two Flix facts shaped the code more than any design taste:

• Records do not derive traits. Move began as { face = Face, depth = Int32, turn = Turn } and could not derive Eq or ToString, which makes it useless in a test or a set. Domain types here are enums with accessor functions.
• solve and run are both keywords — the Datalog fixpoint and the effect handler. The trait method is search.

The contract

Outcome carries the solution in the one case that has one:

pub enum Outcome with Eq, ToString {
    case Solved(MoveSequence)
    case Rejected(Invalid)
    case BudgetSpent
    case Exhausted
}

Exhausted means the engine searched what it can search and there is nothing there. BudgetSpent means it ran out of the caller's time or moves and makes no claim either way. Conflating the two is how a solver ends up reporting a solvable cube as unsolvable.

Invalid splits what a validator can see from what it cannot. Sticker counts are checkable without knowing how pieces are built; reachability is not. CubeSolvers.Solver.facelets does the first and leaves the second to the engine — and an engine that finds an unreachable state reports Unsolvable, never that it is unavailable. TestSolver pins that boundary with a state that has perfect counts and cannot exist.

search has no fixed effect. The trait carries an associated effect and each engine states its own:

pub trait Solver[t] {
    type Aef: Eff
    pub def kind(solver: t): Kind
    pub def search(solver: t, cube: Facelets, options: Options): Outcome \ Solver.Aef[t]
}

The pocket engine declares type Aef = {} — no clock, no file, no state outliving the call — so it can be used from a pure function. Declaring IO on the trait would have taken that from every caller of every solver for the benefit of the engines that do not have it.

That decision removed a field. Options had a time budget, and a pure engine cannot read a clock, so no engine could ever have honoured it. It is gone; maxMoves remains, and it is what makes BudgetSpent reachable.

The engine

A pocket cube is eight corners, and holding one still spends the freedom to rotate the whole cube — so a state is a permutation and a twist, and the only moves are U, R and F.

The distance table is a Datalog fixpoint. Seed the solved state, let one rule walk the move graph, and read off the shortest distance to everything within reach:

let facts = #{
    Dist(solved(); Down.Down(0)).
    Dist(next; deeper(d)) :-
        Dist(s; d),
        if (shallowerThan(d, depth)),
        let next = CubeSolvers.Pocket.neighbours(s).
};
query facts select (s, d) from Dist(s; d)

No queue, no visited set, no loop. Two things about that rule are worth knowing:

• Down[Int32], not Int32. In a lattice position Flix joins Int32 upwards, so a plain count converges on the longest walk found rather than the shortest. Down reverses the order. Nothing type-checks differently; the table is simply wrong.
• let next = neighbours(s) is a generator, not a binding: the function returns a Vector and the rule fires once per element. It is what lets the fixpoint walk a graph that was never materialised as facts.

The table checks out against the published pocket cube figures — 1, 9, 54, 321, 1847, 9992, 50136 new states per level in the half-turn metric — which is what TestSearch asserts, and what makes the move tables trustworthy.

Solving meets the table in the middle: walk out from the scrambled state until you land on a state the table knows, then follow the table downhill. Lengths are tried in order, so the first solution found is a shortest one. God's number for the pocket cube is 11, so a table t moves deep leaves at most 11 - t to find.

Is Datalog worth it here?

Measured, not assumed. Building the depth-6 table (62,360 states) on an M-series laptop, wall clock minus the ~3.1s compile:

Implementation	Time	CPU
Datalog fixpoint	~5.8s	689%
Breadth-first, mutable MutMap in a region	~14.8s	272%
Breadth-first, immutable Map	~32.6s	192%

The engine parallelises semi-naive evaluation; the hand-written loops do not. The breadth-first version survives as tableMut, where it earns its keep as the fixpoint's oracle: TestSearch asserts the two agree state for state.

Where it stops

That result invites the obvious next question — if the fixpoint is the fastest thing here, why stop at six moves? So we packed a state into one Int64 (CubeSolvers.Pocket.Coord, seven positions and seven twists, three and two bits each) and asked for the complete table: every one of the 3,674,160 states a pocket cube has.

	Result
States	3,674,160 — the exact known count, which is its own correctness check
Wall clock	307s
Peak memory	3.1GB

Packing bought about 1.4× at depth 6, not the order of magnitude that would have made this viable. So the honest boundary is: the fixpoint is the best way to build a table that fits, and is not a way to build one that does not. A 3x3 needs pruning tables of a few million entries each, and on these numbers they want packed arrays, not a Map and a fixpoint. CubeSolvers.Pocket.Coord stays because the encoding is worth having — a table that is ever written to disk will need it — and because the measurement should be repeatable.

The 3x3

Two phases, after Kociemba. The first turns any cube into one that needs no quarter turn of R, L, F or B — corners untwisted, edges unflipped, the four middle-layer edges home. The second finishes it using only turns of U and D and half turns of the rest.

Neither phase searches the cube. Each works on a handful of small numbers:

Phase	Coordinates	Sizes
One	corner twist, edge flip, which four positions the middle edges occupy	2187, 2048, 495
Two	corner order, U/D edge order, middle edge order	40320, 40320, 24

A move takes each number somewhere, and where is a table. Pruning tables then give the exact distance in two coordinates at a time — 1,082,565 and 1,013,760 entries for the first phase — and the true distance is never less, so the search can cut a branch the moment the bound exceeds what is left.

All four tables build in about six seconds, breadth-first over arrays indexed by the coordinate itself. That is the shape the pocket cube's failed spike pointed at: a fixpoint over boxed states did 3.67M states in 307s, and this does roughly 2M in about five, because an index is not a state.

Solutions are short, not shortest. The engine tries every first-phase length from the shortest upwards and finishes each as far as the best answer so far allows, then simplifies the seam — but the shortest solution to a cube need not have the shape "reduce, then finish" at all. CubeSolvers.Pocket promises optimality; this does not, and says so in its own documentation.

On the one cube checked against min2phase, both return the same eleven moves.

The 4x4, so far

Tsai's method, by way of TPR-4x4x4-Solver, which averages 44.39 moves. Two of the three phases are built; see docs/four-by-four.md for the whole chain.

Phase	Goal	Moves	States	Deepest
1	R and L colours onto R and L	36	735,471	8
2	U/D and F/B centres home, R/L left finishable, parities matched	28	1,801,800	9
3, centres	the centres finished, parities still matched	20	117,600	10
3, edges	the edges paired	17	31,006,080	13

Every table is complete — each state reaches a goal — which is what makes the walk down them a solution rather than an attempt. On the three shared 4x4 vectors the first two phases take 10, 10 and 13 moves, and the third finishes the centres: a test counts the stray centre stickers afterwards and finds none.

A reduced 4x4 can show a position no 3x3 ever does — two edges swapped and nothing else wrong — and what rules it out is the edge permutation's parity agreeing with the corners'. Both phases carry that agreement as a single bit. The second establishes it; the third has to restore it, because it may turn F, B, U and D a quarter and a quarter turn is odd on corners and even on wings. One cube in three pays a move for it.

Tsai's second step leaves the R and L centres "in one of 12 positions that can be solved in later steps". Twelve is not written down here. An arrangement qualifies exactly when the third phase's moves can still carry it home, so it is found by walking those moves from solved — and twelve is what comes back, which is a pleasant way to be told the reading was right.

What is left is the edges. They are paired in the third phase, against a table of 31 million states at two bits each — where TPR's 20MB mostly goes, and which needs a byte-wide table type before it can be built at all. Its shape is Tsai's: four paired edges placed at BR, BL, FL and FR (11,880 placements, 1,538 after symmetry), against the arrangement of the remaining eight (20,160).

Depending on it

Flix resolves package dependencies from GitHub releases. There is no release yet; when there is:

[dependencies]
"github:wstein/flix-cube-solvers" = "0.1.0"

License

GPL-3.0-or-later. See LICENSE and NOTICE.md.

The 4x4 follows Tsai's method by way of TPR-4x4x4-Solver, whose coordinates are involved enough that reading the reference implementation is the honest way to get them right. TPR offers MIT OR GPL-3.0-or-later; this project takes the GPL option and applies it to the whole package, a Flix package being one artifact that a consumer links whole.