Factorio SAT

Enhancing the Factorio experience with SAT solvers.

How it works

* A balancer size is selected * Tiles get represented as a list of boolean (true/false) variables (input direction, output direction, underground state, splitter side, splitter id, colour) * Clauses (rules/constraints) are written to restrict solutions to only valid balancers: * Belts don't intersect * Colour along a belt is consistent * The ends of the balancer have the correct input/output colours * For each splitter in the splitter network, there are splitters in the solution that have the same input/output colours as the abstract network splitter * Clauses are passed into a SAT solver which either returns the solution or proves there is no solution * If no solution is found then a new size is selected

Caveats

* Currently uses the assumption that the inputs/outputs of the balancer need to be covered by splitters. This should result in balancers that are within 1 tile of optimal and in practice no balancers have been found that exhibit this worst case. * There is no proof that the clauses generated by this program are consistent with the rules of Factorio * Generating balancers gets exponentially harder as more splitters are added to the network. At least until someone proves P = NP

Setup

# Create virtual environment
python -m venv .venv
Activate environment
source .venv/bin/activate # Unix/macOS
or
.venv\Scripts\activate # Windows
NOTE: Activating needs to be done for every new terminal session
pip install --editable .
Get textures
fetch_assets /path/to/factorio/install
Factorio install directory should look something like:
Factorio/
├── bin/
├── data/
│   ├── base/
│   ├── core/
│   ...
...

For rendering splitter networks graphviz needs to be installed. This can be done via a package manager or with the lastest install package available at https://graphviz.org/download/.

Tools

| Tool | Usage | | ------------------------------------ | -------------------------------------------------------------------------------- | | fetch | Load textures (required for render.py) | | blueprint | Import/Export blueprints | | blueprint_book | Pack/Unpack blueprint books | | render | Render generated balancers | | network | Tools for managing balancer networks | | belt_balancer | Generate balancer from a network | | beltbalancernet_free | Generate any n to n balancer | | beltbalancernetfreepowerof2 | Generates n to n balancers where n is a power of 2 (faster than generic version) | | interchange | Generate an interchange for building composite balancers | | make_block | Generate random blocks of belts | | calculate_optimal | Find optimal balancers | | rotate | Rotate a balancer 90 degrees | | stringifier | Convert balancers to and from text | | test_runner | Run the test suite |

Controls (render.py)

| Key | Usage | | --- | ------------------------------ | | I | Go to next | | K | Go to previous | | S | Save animation of balancer | | E | Export balancer as a blueprint |

Example Usages

# Find and render all 4 to 4 balancers that fit in a 10x4 square
belt_balancer --fast --all networks/4x4 10 4 | render
Start computing the optimal by length with maximum underground length of 16
calculate_optimal compute 16 length
Render optimal area balancers with maximum underground length 4
calculate_optimal query 4 area | render
Generate and render interchanges for a 22 to 22 balancer made of two 11 to 11 balancers
interchange --alternating --underground-length 8 --all 8 22 | render
Render a network graph
network render networks/5x5 5to5.png
Save an animation of a blueprint to a file
cat blueprint.txt | blueprint decode | render --export-all
Generate 50 random blocks and save to a blueprint book
makeblock 16 16 --all --single-loop | head -n 50 | blueprint encode | blueprintbook pack --label "Blocks" > blueprint_book.txt

TODO

* Solve the remaining balancers (8 to 7, 7 to 5, 5 to 7, 8 to 5, 7 to 8, 5 to 8) * Go bigger * Add support for finding the optimal factory units

Examples

\ \