R_O_C_K_E_T

Sounds interesting, if the problem could be encoded at a higher level efficiently that would be sweet. I'm not sure that a more numerical perspective will help all that much....

The interchange problem is to design a belt layout that takes input from two different balancers with n outputs and mixes them together. Such that a final layer of splitters...

I've provided a table of values below (options used are `--alternating --underground-length 8`). Memory and time values are self reported by kissat. The remaining time+space should be linear in the...

Great that you got it to work. I do have some spare time, so I may be able to help out some. The format is not too complex. I've linked...

Using some command line solvers (e.g. `--solver "cmd:kissat"`) will give some indication of how much progress has been made, though no ETA. They also tend to have much better performance...

Could try running python with `-X` to force utf8. e.g. `python3.9.exe -X belt_balancer.py --fast --all networks/4x4 10 4 | python3.9.exe -X render.py`. If that fixes it, then I think you...

Thanks for taking interest in the project! Probably best to put them in their own repo. If you've found an improved balancer design, then feel free to merge in the...

It looks like they're not quite equivalent. Plumbing some test designs into https://github.com/d4rkc0d3r/FactorioSimulation gives an equal min-throughput, but more limited throughput combinations on the variant that pulls from different output...

You could use IPASIR-UP to bridge the two projects. Which can designate some SAT literals to be constrained by an external solver. Was looking into using it in this project...

You're probably right, I have not managed to get any kind of decent results out of IPASIR-UP. I had a go a tweaking the cardinality constraint encoding and I didn't...