Using a SAT Solver to optimize balancers

[deep_remi]

I saw this on Twitter today. Not my creation, but I could not find a discussion about it in the forum. Sorry if it was posted before:
https://github.com/R-O-C-K-E-T/Factorio-SAT

Example of a 16-16 balancer found by the solver, shorter than the previous best known by 1 tile:
https://twitter.com/wren6991/status/1516925406007410690

[Qon]

That's cool! Maybe I should update my N-to-N-belt-belt balancer code (post with img, img) to include these, and maybe clean them up a bit and maybe make bigger than 2048 belt balancers.

But a lot more than just balancers should be solvable. This could be applied to any other constraints and factory building.

[FuryoftheStars]

This is certainly interesting and I thank you for posting it.

I am curious on the throughput potential of the solutions it comes up with, though, in the event of not full inputs or backed up outputs. I think I had read somewhere a discussion taking place that any balancer above 2-2 is not / cannot be UTU, though I don't know where that went to anymore....