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.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