3 ms·
Tried encoding it as an PBSAT problem. (It's actually relatively simple to encode as one. Just have a fixed upper number of digits, a constraint saying the bool
by TheLoneWolfling 11y ago
Tried encoding it as an PBSAT problem. (It's actually relatively simple to encode as one. Just have a fixed upper number of digits, a constraint saying the boolean must be >=2, and n-1 constraints saying the other n bases must equal the binary one. Double the number of digits each time until you get satisfiability, then binary search from there.)
For instance, this is the {2,3} case, with 2 digits:
* #variable= 4 #constraint= 2
1 x1 +2 x2 -1 x3 -3 x4 = 0;
1 x1 +2 x2 >= 2;
Unless I've done something wrong (which I probably have), the 2,3,4,5,6 case is unsatisfiable at least up to 8092 binary bits, or roughly 10^2435. Not surprising, but still, interesting. Can't go higher or sat4j runs out of memory on my machine.
And yes, it successfully recovers all of the other cases mentioned.
The wonders of punting everything to external solvers. Even considering that there's (massive) problems with this encoding.
Code: https://gist.github.com/TheLoneWolfling/da51e3da0045f53ecf85 https://gist.github.com/TheLoneWolfling/da51e3da0045f53ecf85
- TheLoneWolfling 11y agoI 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 ago32754 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.