Skip to content

Instantly share code, notes, and snippets.

@LiveOverflow
Created November 20, 2020 10:46
Show Gist options
  • Star 13 You must be signed in to star a gist
  • Fork 1 You must be signed in to fork a gist
  • Save LiveOverflow/683181b72b4123fdb325956d6f038e72 to your computer and use it in GitHub Desktop.
Save LiveOverflow/683181b72b4123fdb325956d6f038e72 to your computer and use it in GitHub Desktop.
Hire me!!!!!!!!
Display the source blob
Display the rendered blob
Raw
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
@LiveOverflow
Copy link
Author

LiveOverflow commented Nov 20, 2020

Install z3 in the notebook sage environment:

import sys
!{sys.executable} -m pip install z3-solver

@DevMind89
Copy link

U are the best!

@shreyansh26
Copy link

Does the code work correctly for everyone? For me the loop stops at "best inp[ca]" and the values are different for me as well for every step. At this point, I am just running this exact notebook.
Anybody else facing the same issue?

@LiveOverflow
Copy link
Author

That's weird, it shouldn't stop. What is the error message you see? If you just mean the output doesn't continue, then it's probably just not done yet. The code can easily take 30min to run. Maybe much longer if you have a slow system. Generally it's useful if you can provide more technical details when asking for technical advice. "loop stops at ..." is not really helpful.

@shreyansh26
Copy link

shreyansh26 commented Nov 29, 2020

Sure. What I mean is that, the solver never gets to the "SOLVED" stage. I get the following output

best inp[fe]: e572ddecd35496e3a90a87e4740b95d3bdbe478b34f2d7551dc9d84a6370fbdd
best inp[fd]: 8dd28fa4d913844f63a77bfab098ce62a59e03d7291714f9787d2dde9b0df48c
best inp[fc]: 749dc07035936b190c6c62a1ad898e1a021c8486272ac6e7a0ead4e458a73687
best inp[fb]: c0298b653341f6908af91cb3645358c5a7b44f8294d2f15b9f98668f55454394
best inp[fa]: 84482bb68c4c89c774982ffff72d80666390060e0754132ce22da95fcc037f08
best inp[f9]: bc5d7f8cc50786a512fa883b96f76cb4a73d74633f155d1007704113fbd9a5a5
best inp[f8]: bb1377362027c10245ae57e88ef608b69d87d7c022a155c65c1ffd9dcb9f3f4b
best inp[f7]: 45ebf683a6bfaa839b5651de5dff5283398081f812a6fb19f915687427938103
best inp[f6]: 7ef89cdbefbd88d84f16562f2c25d71077648a9d9de7a4781a0fbe1c4f58c19c
best inp[f5]: 33b693af431a507314c69e6b238e32bc3af63ac503f86a65e2cd4d0f7284c39f
best inp[f4]: a3de909c4d145d331ccca08a49ea5981786d66f94f2724d69221ce2092811617
best inp[f3]: 6f29b87a5d4692fa5362dd356e09d8127ff7694574e3dd59824e18586fdef66f
best inp[f2]: 4da632ffd4a6c91432574ddbf274a14be4be042adfc1412b650b53a8ef9919b2
best inp[f1]: c4e5f80459b61e688ae9af9e4b6e100b3278c50284d9cc464f386f5fa1b7e6ba
best inp[f0]: 898588afd43a27c34f7820000606be25af257fbc6417905da1afa1b97db416f5
best inp[ef]: f9f50aa62be4a40879ddf2aadbec0e76a484a4f452033889441c5a30689ed30d
best inp[ee]: 7f10a15b2a0708531a155b00057bd80a36df3cd7af776d3150d4061f48414895
best inp[ed]: 190682836491c5058ea78a1d75c1185c27606b833611d78a6042d6b6b9db907f
best inp[ec]: c9ecc512254408207438d244f1af00a6f0b280c848f4a466cee2e7eb0b75e5ac
best inp[eb]: adc628188862ccbdbe7562dadfee0dbe1ab034fde504a0f91de249bf66f049a1
best inp[ea]: 2f44ba13c7f7b3029893c0f46f36f872de3fd86c2a790ba8bc42fc1150c505ee
best inp[e9]: d5a85c07877860bf2f42ae2883beb39b02b41003c599e17e4f51bc2f2fae091a
best inp[e8]: 27e356e282a156eca6ea77779304482ac486aa4649618d94762d538344a139c7
best inp[e7]: d2a7b1942f2b4e2f4fa0eaff8bc3748aec59daa9858eaf24743f19c4fcb6f658
best inp[e6]: 089b87f6dde948e6c54448d389f106a5251920fa7e51da61c711fd76f596f450
best inp[e5]: e1daa83063e45cd35c0153deb98aea2ba4e7bf4c9900e2cb0305533ed81177ff
best inp[e4]: 762c7ed0fbba2f7934b439f07b76b202e7834e9ddabeb417ded3ad86a3fa077f
best inp[e3]: 0670b1d7cc28b6d5e272822eb20d16814d88a828b617042a72a936e629b21816
best inp[e2]: 6124eefd81259c8d184d86df954177f809d4b364ebc147263b8accd804bd3889
best inp[e1]: b3f8e60e2577df15396bb6b462b7dfd6c945e93389a180f7fae5655fa1822fba
best inp[e0]: d90c1d933319f68c8d15266aad7f104c73c9b2e39f2784e57b841c1d2cc56c43
best inp[df]: 54e13d74c834881331937a0da96db7342f32b373b7add9aa354d049041528345
best inp[de]: 6dc09d500fbb422230d7f5139be8ec692644be58efae458d7892ac1330d00d52
best inp[dd]: 6f1dfb14246292f47b67636a9c8321c3d05d969d6b2269b48e6eceaf58038f11
best inp[dc]: f26f1817d00152a76c1c7976468e3c79419110af96bd046c47ad9bf1ee417fc7
best inp[db]: cbeb5550b1054e30e20118d329e9be81da762952587845fceb8cbb4bc0c043a7
best inp[da]: 0363ce0ea1278a9894e7c36b7a584a0a1572068b3ae60734812de28a815c5bbc
best inp[d9]: 3b70594b29b9817f4f1b7b8b38486a54c40a187b776d9fc3c472ce4aba7b1a99
best inp[d8]: a49c444d780681ef5d617d566c13064d103ca037a42344fdd02e1177520ea7bb
best inp[d7]: 1fb435ec4fd27e86e41024e2186a3d91265a4d1515f2666ac915ae8c9b187761
best inp[d6]: 2fa1915824d01ac7967ff106a8864d45d96fa78b8e5b633178f823bf3a0e4572
best inp[d5]: 7a54222568f1184b9288ad61b7f1016a346631c9bca1f4e8b11df038690af200
best inp[d4]: 57948cb4f88ff2c824954ac4396072474d1ed69cfcfb700ecab803ad0c8a2a76
best inp[d3]: 4254f13f07f80fdf7e2dbdf528bda707fdfd30807ac735b183dbbe5b43de9f47
best inp[d2]: 492df52b175bf14ea5180b518614572264e81a30bbb44ac4a458fda42cad5594
best inp[d1]: 6cd4375a4ca80a4dfb2f85e1c0d8d80c03f87d5ff900a0a96f82b9c449c86c9d
best inp[d0]: 266a9ef1b054c7b02edf4b993f06a1689566d77ec147b70acb0cb8f4b127474c
best inp[cf]: 443f140c6127249c7477748a31df29d014251e296c9b33418575ca55d88b3148
best inp[ce]: 52754d15fce9c843a947138e050dfa6693a97892fcfb8f9d0099505fcc5ab44a
best inp[cd]: 37f03e579652c0081d561b1caaf7d632e5574cb4e5e5be9ebeec5fa04d3f7ff6
best inp[cc]: 5b5c213ab0fa9cc624d0804e6e086bbc7e6de6072e0e2b8e1907724718ace8e8
best inp[cb]: 0c33148bd80f9845000dc8122c5332f143d3a59089c9ef57c1e36a066033e32d
best inp[ca]: 16bc33485c327724086acc6f44babe61f22315d494087d5c72e60fb70b944445
done: 15 attempts 1606621709.38508-1606621801.5408595 = 92.15577936172485
it took 1 minutes...

It also means that in the recursion step in solve_round, it never gets a True value for res as there is no output that is beginning with inp.

Also I am running SageMath 9.0 with a Python3.7 backend.

@shreyansh26
Copy link

Nevermind, it works now. There was a bug in my installation. Some obvious features were working incorrectly. Reinstalled in a new environment and now it works.
Thanks!

@TeWu
Copy link

TeWu commented Jan 10, 2021

It seems like you are incorrectly excluding a model from the solver. Instead of:

solver.add([i!=model[i] for i in inp])

it should be:

solver.add(Or(
  [inp[i] != model[inp[i]] for i in range(0, 32)]
))

See this gist for an example.

By doing this incorrectly you're overly limiting the number of input candidates generated by Z3 solver. That is - you're not guaranteed that the solver will generate any input candidate, that could be used (in solve_round) to calculate the solution. I guess, in example above, you were able to get the solution, because fortunately the valid input candidate had not been eliminated, before it was generated (and used). I wonder if you've tried target strings other than "Hire me!!!!!!!!\x00"? Like "LiveOverflow!!!\x00", that you mention in the comment.

FYI: I don't have sage installed, so I haven't run the code in its entirety. But I've run the 'Z3 model exclusion' part, like you can see in a gist linked above.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment