Skip to content

Instantly share code, notes, and snippets.

@LiveOverflow

LiveOverflow/hireme.ipynb

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.
Download ZIP
Hire me!!!!!!!!
Display the source blob
Display the rendered blob
Raw
hireme.ipynb
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
@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