/Factorio-SAT

Enhancing the Factorio experience with SAT solvers

Primary LanguagePythonGNU General Public License v3.0GPL-3.0

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