New BPs for 5x6 and 6x7

[tcosprojects]

Hello, I saw your post about your balancer book update and Factorio-SAT. Inspired by your post, I've started experimenting with running several SAT solvers in parallel to see which one wins based on the portfolio parallelism strategy. It seems MapleLCMDistChronoBT does well with the balancer problem and it claims to have found solutions for 5x6 and 6x7 inline. Attached are the blueprints for those.

Also, if possible, can you share your optimal_balancers.json? It seems you have solutions for ones I still do not have, and I'd like to test running parallel SAT solvers, plingeling and cryptominisat, on a many core machine (40+ cores), focused on the remaining balancers needed.

Thanks!
5x6.txt
6x7.txt

[raynquist]

Very cool! It appears that Factorio-SAT still has some of the old balancer networks bundled. I'll see if I can get them updated. I assume those were the networks you used. The 5-6 and 6-7 are not input balanced at certain throughputs. Attached are networks that I've fixed.

I don't actually maintain an optimal_balancers.json. I've given up on using it since it's overwritten every time the program is run. The ones I don't have are 5-6, 5-7, 6-7, and 7-8 (and their inverses). The only really slows ones I've found solutions for are 6-8 and 5-8, with 6-8 taking an hour or so and 5-8 taking I think it was like a week or two. R-O-C-K-E-T is the one that generated the 16-16. He hardcoded the first few rows that get that solution.

I'm very interested in seeing if you're able to find any solutions.

fixed_networks.zip

[tcosprojects]

After running the parallel solver for about a week against the updated networks in the latest Factorio-SAT, it has produced a potential solution for 8x7.

8x7_inline.txt

[tcosprojects]

Also, I've noticed that for some reason the larger to smaller 8x7, 7x6, 7x5 and 6x5 balancers seem to be progressing faster than the smaller to larger balancers. Can these all be hand inverted if I just focus on the faster ones?

[raynquist]

Nice! That 8-7 is definitely an improvement. I would've never found an 8x14 solution using the default solver. Which solver found this solution?

Inverting the downsizing balancers does produce valid upsizing balancers, but they may not be the optimal ones. The downsizing balancers have an additional restriction: the tile in front of unused splitter outputs cannot be occupied by other belts. In contrast the space behind unused splitter inputs can be used by other belts, and many upsizing balancers make use of that space. So it'd be faster to eliminate a particular impossible size when solving a downsizing balancer, but that wouldn't tell us if that size is also impossible for the reciprocal upsizing balancer.

If the upsizing solver is solving a size that the downsizing solver has already found a solution for, then it is indeed fairly pointless to continue running the upsizing solver. The only good we'd get out of finding the upsizing solution in this case is if it happens to be marginally better than the downsizing one, like being downgradeable to slower belts or using less material. In fact I would even say that if the upsizing solver is solving a size that has the same area as an existing solution then it can be stopped. Unless the existing solution is not inline perhaps. People do like inline solutions.

The other scenario is if the upsizing solutions are never found, then inverting the downsizing solutions is better than nothing.

[tcosprojects]

This was found with plingeling running on 5 threads and a few GB of ram for about a week. The amount of memory it needs increases with the number of threads and over time. My testing with 24 threads used 12GB of ram after just 12 hours. I compiled it from arminbiere/lingeling and ran with --solver "cmd:./plingeling -t 5". This was done on Ubuntu Linux 22.04.

Thanks for the detailed explanation on inverting balancers, I'll focus on the 3 remaining downsizing ones first since it should come back with a solution sooner by increasing the solver to 12 threads. The solver for 7x8 has not excluded a length of 13 though, so I'll keep that on the list for later.