Factorio-SAT searches for belt balancers with a SAT solver

The balancer becomes a boolean formula

The pipeline is described in six steps and each one is a translation you can follow. A balancer size is selected. Tiles get represented as a list of boolean variables, and the README names them, with input direction, output direction, underground state, splitter side, splitter id and colour. Then clauses, which are the rules and constraints, are written to restrict solutions to only valid balancers. The clauses encode that belts do not intersect, that colour along a belt is consistent, that the ends of the balancer have the correct input and output colours, and that for each splitter in the abstract splitter network there are splitters in the solution with the same input and output colours as the abstract network splitter. Those clauses go into a SAT solver, which either returns a solution or proves there is no solution, and if no solution is found a new size is selected and the process repeats. The abstraction is the interesting part, because the solver never simulates Factorio, it solves a formula whose satisfying assignment happens to be a valid layout.

The caveats are the honest part of the README

Three caveats are stated, and they are worth reading closely because they bound the correctness of the output. First, the program currently assumes that the inputs and outputs of the balancer need to be covered by splitters, which the author says should result in balancers within one tile of optimal, and in practice no balancers have been found that exhibit this worst case. Second, there is no proof that the clauses generated by the program are consistent with the rules of Factorio, which is a different and more serious statement, because it means a satisfying assignment is only as good as the author's reading of the game. Third, generating balancers gets exponentially harder as more splitters are added to the network, and the author appends the observation about P = NP. In other words, the tool proves a solution does not exist with respect to its own encoding, which is a stronger statement than proving no valid balancer exists in the game.

Thirteen command line tools, not one script

The package installs a set of console entry points, and the tool table in the README is the real feature list. There is fetch to load the textures that the renderer needs, blueprint and blueprint_book to import, export, pack and unpack, render to draw a generated balancer, network for managing balancer networks, belt_balancer to generate a balancer from a network, belt_balancer_net_free to generate any n to n balancer, belt_balancer_net_free_power_of_2 for the power of two case which the README says is faster than the generic version, interchange to generate an interchange for building composite balancers, make_block for random blocks of belts, calculate_optimal to find optimal balancers, rotate for a 90 degree rotation, stringifier to convert balancers to and from text, and test_runner for the test suite. The division is sensible, because the expensive part is the generation and everything else is a transformation of the result, and a pipeline of small commands composes better than one monolith.

Setting up needs a virtual environment, the Factorio install and graphviz

The setup is a standard Python project install with two extra pieces of context. The environment is created and activated, and the package is installed in editable mode.

python -m venv .venv

# Activate environment
source .venv/bin/activate # Unix/macOS
# or
.venv\Scripts\activate # Windows

The install step and the asset fetch follow.

pip install --editable .

# Get textures
fetch_assets /path/to/factorio/install

The README shows the expected shape of the Factorio install directory, with a bin/ folder and a data/ folder containing base/ and core/, which is what the asset fetcher reads. For rendering splitter networks, graphviz needs to be installed, and the README points at the graphviz download page for the package. The dependency list in pyproject.toml explains the stack, with python-sat for the solving, numpy for the geometry, luaparser because Factorio blueprints are Lua, pygame and PyOpenGL with pillow for the renderer, graphviz for the network diagrams, and ffmpeg-python for the animations.

The command line composes, and the examples show it

The example usages section is a set of pipelines, and they show the intended workflow. To find and render all four to four balancers that fit in a ten by four square, you generate with a fast flag and an all flag and pipe into render. To start computing the optimal by length with a maximum underground length of sixteen, you call calculate_optimal with compute and a length. To render optimal area balancers with a maximum underground length of four, you query and pipe to render. Interchanges for a twenty-two to twenty-two balancer made of two eleven to eleven balancers are generated with an alternating flag and an underground length, then rendered. Random blocks are generated and saved into a blueprint book by chaining make_block, head, blueprint encode and blueprint_book pack. The pipes are the point, and the fact that generate, render, encode and pack are separate commands is what makes them composable that way.

Where the tool stops being useful

The first limit is search cost, and it is the reason the TODO list still contains 8 to 7, 7 to 5, 5 to 7, 8 to 5, 7 to 8 and 5 to 8, alongside a Go bigger item. Every additional splitter makes the formula harder, so the sizes that remain unsolved are the ones where the search space explodes. The tool is therefore best at the small and medium balancers where a human would have drawn it anyway, and worst at exactly the configurations a player most wants. The second limit is that the output is a found solution rather than a designed one, so the result is whatever the solver returns first, and if you want a specific shape or a specific aesthetic, the tool does not help. The third is the correctness caveat again, with a practical edge. The clauses are the author's encoding of the rules, and if that encoding is subtly wrong, the solver will confidently produce a layout that does not work in the game, and the failure will look like a Factorio problem rather than a tool problem. Finally, the project is pre-1.0 in practice, with a version of 1.0.0 in the metadata but a Development Status of 4, Beta, and no GitHub releases at all, so there is no version history to consult when a result changes.

Editorial conclusion

Factorio-SAT suits a Factorio player who wants compact, provably valid belt balancers and is willing to accept the solver's runtime, and it suits a reader who wants a clean example of encoding a game mechanic as satisfiability. It is the wrong tool if you want a specific hand-drawn design, since the tool searches rather than draws, and it is the wrong tool for a large network, because the generation cost grows exponentially with the number of splitters. Before running it, read the caveats section, because the encoding is not proven consistent with the game rules and the optimality claim depends on an assumption about splitter coverage, and note that the last push was on 2026-08-18 with no tagged releases, so you are building from a moving repository. The package version is 1.0.0 and the licence is GPL-3.0.

Frequently asked questions

Official sources

1. Issues
2. License: GPL-3.0
3. README
4. R-O-C-K-E-T/Factorio-SAT on GitHub