@oe1cxw Found on Facebook (unfortunately). Solving it this way was more fun!pic.twitter.com/cYj8KBqx7P
Show this thread
-
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 …
= 4373612677928697257861252602371390152816537558161613618621437993378423467772036
= 36875131794129999827197811565225474825492979968971970996283137471637224634055579
= 154476802108746166441951315019919837485664325669565431700026634898253202035277999But 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.
-
-
Ahh right. I was gonna do something a little less restrictive like: (assert (> A 4373612677928697257861252602371390152816537558161613618621437993378423467772030)) etc Can't make the solver's job too easy, right?
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
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.