3 ms·

I spent a bit of time optimizing it (mainly writing the problem file incrementally). Currently chugging through d=16371. Rather amusing in a way - 81855 variab

I spent a bit of time optimizing it (mainly writing the problem file incrementally). Currently chugging through d=16371. Rather amusing in a way - 81855 variables, only 9 constraints. (Actually, only 5 constraints, but sat4j seems to split some of them.) EDIT: 16371 is unsatisfiable. Continuing... EDIT: 2.1GB PBS file. 6 lines. I now see why the PBS file specification suggests not reading in files line-by-line. EDIT: 640.572s to read in the problem, versus 101.481s last time. Now solving... If the ratios remain constant this'll take ~4 hours, 25 minutes.

TheLoneWolfling 11y ago
32754 is also unsatisfiable. My machine won't handle 65521, unfortunately. If someone with more RAM could run https://gist.github.com/TheLoneWolfling/da51e3da0045f53ecf85 https://gist.github.com/TheLoneWolfling/da51e3da0045f53ecf85 (changing -Xmx4g to something higher in the process), I'd be happy. In other words, unless I'm doing something wrong, there are no solutions to the 2,3,4,5,6 case below 2^32755, at least.