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 |
| belt_balancer_net_free | Generate any n to n balancer |
| belt_balancer_net_free_power_of_2 | 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 5_to_5.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
make_block 16 16 --all --single-loop | head -n 50 | blueprint encode | blueprint_book pack --label "Blocks" > blueprint_book.txtTODO
- 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
\
\
