@oe1cxw Found on Facebook (unfortunately). Solving it this way was more fun!pic.twitter.com/cYj8KBqx7P
Show this thread
-
Ohhh yes, that problem is a doozy. Good answer on Quora about it; the answer is like dozens of digits long if memory serves. I'd thought about trying that problem and seeing if z3 chokes on it, but seems like you already did :P.
Smallest Solution:
= 4373612677928697257861252602371390152816537558161613618621437993378423467772036
= 36875131794129999827197811565225474825492979968971970996283137471637224634055579
= 154476802108746166441951315019919837485664325669565431700026634898253202035277999
-
-
Re trying that problem: No, I did not try it. I just know that this is not the kind of stuff that SMT solvers are good at. However, I just wrote a short smt2 file in case you want to play with it: http://svn.clifford.at/handicraft/2018/ecsmt/ecsmt.smt2 …
-
But z3 even has a hard time with it when you assert concrete values for two of the three variables. And yices doesn't even support a logic that would allow this kind of arithmetic afaict. But you can use this to check the solution I gave above by asserting the solution.
- Show replies
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.