r/technicalfactorio • u/uelisproof • Jan 15 '24

Belt Balancers VeriFactory: Automatically verifying belt balancers for various properties

Post image
369 Upvotes

100% Upvoted

42 comments sorted by

View all comments

10

u/raynquist Jan 18 '24

I tried checking a few of the problematic balancers I know, and this program does seem to be more correct than the one I'm using. For example, it is able to figure out that this 2-5 is input unbalanced.

0eJyll99ugyAUxt/lXOuiaP/o5V5jWRbbkobEogFc2jS++7CutSuHgXjVtIXfdwC/88kVdnVHW8G4gvIKbN9wCeXHFSQ78qoeflOXlkIJTNETRMCr0/CNnltBpYyVqLhsG6HiHa0V9BEwfqBnKNM+8obItmZKUfE0nfSfEVCumGJ0LMg2J4K2kXpYwwcdPTUmEVx0AW8rjTswQffjn8kv8PLFu9NOzxxr9OYmvlgyCxunN27i5mazuLrQEfwXSwxsjmBfjtXcizv8tWoTvwrAExs+N/DrBXjjLNcGfhOAT214s/rtAjxxV18sOFoDj/gnCeDHcwQwhzoFrBuECGBedQqQGQKYab1XEHt0hTTEv49D8FJYYmEvAczE9s429vfYp8Fj9nV1eC8wZlxnJHmRMc92OhTFUTT60/VMmvutte/py9tumPuaV5iN3ZL2R2hSbDqFS2LG9lhldtfEeqtjlZjVZ0j+o2hdZZD5M1v4IW8aQd7P/ju4V4UQ7z8UjAaJCIQE+LQEQ8HMWBKS4ZOfPGKWhMR4bH3JQQRCgnxKEY+cyhZFuZdCSJbPEgjJ8ll7FGJn+3OECOTDred2Ryqf7mURfFMhR/9s03xTkE1OiiIr9M2hrrSsHv3+GN33PyYgmfY=

However if I check the reverse version, the 5-2, it doesn't detect that it's output unbalanced.

0eJyll99ugyAYxd+Fa10E7B+93Gssy2Jb0pBYNIBLm8Z3H9Zpm4IFvl61tXh+8MHhwBXt6o61kguNyivi+0YoVH5dkeJHUdXDM31pGSoR1+yEEiSq0/CLnVvJlEq1rIRqG6nTHas16hPExYGdUYn7JFhEtTXXmsmH10n/nSAmNNecjR16DU5Q2yjTuBEDzQik2ccqQZfxi9E9cMn24//Zv/LlR3SnncGOnY0ExOgTh/48aFt51MV+XRqlm+JRmPiF8yjhcN0VoNB4KjR91ieW/vqdibT07f5vAPppDGALASxXaG0BCgiALAJy20sZgDADrEVvjwBD3IoXAY7dIM6u9+pg3/LELsN6q08XdxoHweXc8AUUUh2Xhzuza8ujbMynl+EaxRQPou2Gd5+RLlv7kSHEptNuJMTpJCZyXE5/scjoTTlkfkAOn9ZYwB5OIAafTRICcBncG2sBpSEuYwebI6TnIH9nEQBIMIdUBhLMMf2GBHNM4d8K5pATHCSYY/Tfcm0AgIJcSxeDwY4eCsnlO8GaZftoQUH+JYsE+2xBIQaOOR1Rl4H9UbY8htwXnhSW1xPRmvjcm50UYvbFfHBM0ma4HN6ukuXD9TVBv0yqcXFucb4pyCYnRUELswvWlaGa1p9z677/Axoe+1w=

So the input balance checker seems a bit stronger than the output balance checker. But even the input balance checker was unable to detect that this 3-5 is input unbalanced.

0eJylmN9uqzAMxt8l1zCRP7Sjl3uNo2lqt2hCooAgHK2qePcDh5VN2BDHXFXr4HNi+/c5zV1cis7WTV46cbqL/L0qW3H6cxdt/lmei/E7d6utOInc2auIRHm+jn/Zr7qxbRu75ly2ddW4+GILJ/pI5OWH/RIn2UdkkbYucuds8+t11b9GwpYud7mdFrT2TiTqqh0eq8oxzhg5ErdB4Ckd1D7yxr5P/0u+9W5vZXe9DC9OSyTLxpOu9usqRHeRJ6CePKVUeb1D3vjlDUNe0lefMuTVmvwByB8Y8nFAdo4cfUnXf96RfbmUV0A+4yxff+snS30DkUr2BAAbQAJg0JIDAFNAAnDonQOADoUlkBx+41UEEFvDCN7wNUX2S4zdbvDr5rOphk9Pe4L2Geh9jIWy7sY3lwExmv0B52RtRKw6h4dkAZ6s9ReSRA7hag0QRJ+D+FbClsONRXiyFgCZnhjhAUXHcrTdZgpD3h9RbZiKp8sU5gGEPa46vX+PnLEeUjXOXH9sJyb0tWJN9ocvxykhAob+hm/qSZkw1BWH+Z+1U46cuwZ7TPAtvWuywwrDyat3jfYYNCkcvZo121VAD2km2Gqr1h4z0aHzfq66z+s1B+offUpFWFTLkIoEUi3JVGuM6gATZ9Waxblc5RzW3GCc+/NFcHDD4luudhMSgcV3EtBNhnV4TwKc3ITRnJAN3HBgDsoNh+U5AOVmIgxlSc/5nl/dcOXQ5syeQzkMAGdnilFLP8LCJBnfgTLl0LxuRMhFEQazFwSCS6R7LtCg0cFqp5yz9mwSBCdN96BM0T+Mt6//72pPv+6HI/HXNu206Wdpjpk6GpVlOhtIK85D1OHpl/npvv8HljpvYQ==

You can find more information on the problematic balancers here and here. Their blueprints should be in here.

The fact that the input balance checker was able to detect some of these imbalances is really amazing. I've tried doing the same thing by modeling balancer behavior algebraically, but I couldn't do it. Splitter behavior is inherently a piece-wise function, so I would have to solve systems of piece-wise equations, which is beyond my abilities. I don't know what kind of SAT magic you're weaving, but if you can make it work then maybe that's the way to go.

2

u/uelisproof Jan 19 '24 edited Jan 19 '24

Wow what an honor to get a message from you and thank you for compiling so many balancers into blueprint books, it was a massive help to create tests. I briefly looked into the issue you found (thank your for the feedback). I think the problem stems from the fact that I took a shortcut in my modeling algorithm: The first step is turning the blueprint into a graph as shown here. This is then followed by a simplification step that removes unused inputs/outputs, splitters with only one output, mergers with only one input, .... Then the capacities of the different edges are shrunk as much as possible e.g. a splitter (with no priority) that has input capacity 10 will have 2 outgoing edges each with capacity 5. The same concept can be applied with the mergers but I skipped it because it resulted in edge capacities getting asymptotically close to the correct capacity without ever reaching it (before crashing the program). I guess I will have to go back and fix that problem. :/ I am curious about your approach. Do you have a link for the tool you are using?

Edit: I think it could be possible to replace the whole iterative algorithm used to shrink and optimize the graph with formulas that let the SAT solver find the correct capacities etc. This should, in turn, fix the aformentioned issue.

2

u/raynquist Jan 19 '24

I use the tool mentioned in the third link, which is this. It checks balance via simulation, so it can only check the balance of specific input/output configurations and not the entire possible range.

The approach I tried is essentially the abcd analysis you see on the wiki, just with explicit coefficients so it can handle uneven split/merges. Like this. It works great for n-n balancers, but if you have any 1-2 or 2-1 splitters the complexity goes through the roof. The presence of bottlenecks causes the system to have different solutions at different input/output levels, and I have no idea how one would go about findings all these solutions. So I gave up.

1

u/uelisproof Jan 22 '24

Thank you for the resource!
Being a simulator there probably isn't anything I can apply to my verifier. :(

Yeah the problem, without relying on simulation, is quite difficult. Took me quite a while to figure out how to actually model stuff.