@oe1cxw Found on Facebook (unfortunately). Solving it this way was more fun!pic.twitter.com/cYj8KBqx7P
Show this thread
Yes, I do that all the time. For example: http://svn.clifford.at/handicraft/2017/smtcode/smtcode.smt2 … solves http://svn.clifford.at/handicraft/2017/smtcode/smtcode.jpg … And of course also harder puzzles like this one: https://twitter.com/oe1cxw/status/954697912528855040 … But I'm still waiting for a solver that can solve this out of the box:pic.twitter.com/mkMrmwlXl7
-
-
Yes, there are specialized elliptic curve solvers of course. But nothing generic that just looks at that (i.e. an equivalent set of formal constraints) and knows what to do with it.
-
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.
- Show replies
New conversation -
-
-
The combination lock one is a bit tougher for me (I haven't looked at your solution- trying it myself). How do I create an "3-long array of Ints" constant in SMTv2? If I can't, do I need to create tuples using (declare-datatype) to represent lock combinations?
-
You don't need arrays for this. Simply use three variables and (to keep the code short) helper functions like those below. (You could use arrays and for-all expressions. But the best case scenario is that the solver figures out how to unroll this to code using 3 simple vars.)pic.twitter.com/jMMma26PwT
- 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.