elijahahianyo / factorio-sat

Enhancing the Factorio experience with SAT solvers

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

# Install dependencies
python -m pip install -r requirements.txt

# Get textures
cd assets
python fetch.py /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.py	Load textures (required for render.py)
blueprint.py	Import/Export blueprints
blueprint_book.py	Pack/Unpack blueprint books
render.py	Render generated balancers
network.py	Tools for managing balancer networks
belt_balancer.py	Generate balancer from a network
belt_balancer_net_free.py	Generate any n to n balancer
belt_balancer_net_free_power_of_2.py	Generates n to n balancers where n is a power of 2 (faster than generic version)
interchange.py	Generate an interchange for building composite balancers
make_block.py	Generate random blocks of belts
calculate_optimal.py	Find optimal balancers
rotate.py	Rotate a balancer 90 degrees
stringifier.py	Convert balancers to and from text
test_runner.py	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
python belt_balancer.py --fast --all networks/4x4 10 4 | python render.py

# Start computing the optimal by length with maximum underground length of 16
python calculate_optimal.py compute 16 length

# Render optimal area balancers with maximum underground length 4
python calculate_optimal.py query 4 area | python render.py

# Generate and render interchanges for a 22 to 22 balancer made of two 11 to 11 balancers
python interchange.py --alternating --underground-length 8 22 --all 8 22 | python render.py

# Render a network graph
python network.py render networks/5x5 5_to_5.png

# Save an animation of a blueprint to a file
cat blueprint.txt | python blueprint.py decode | python render.py --export-all

# Generate 50 random blocks and save to a blueprint book
python make_block.py 16 16 --all --single-loop | head -n 50 | python blueprint.py encode | python blueprint_book.py 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