Day 4: The Ideal Stocking Stuffer
A very easy puzzle that can be brute-forced quickly.
The obvious approach to both parts of the puzzle is to run a bruteforce search for the smallest number N which, when appended to the input string S and hashed with MD5 produces an output beginning with five zeroes.
Unfortunately Picat doesn't come with an MD5 function in the standard library, so I wrote one based on a naieve copy of the pseudocode in Wikipedia's MD5 article and some of the implementations on Rosetta Code.
This went relatively quickly and I had a working MD5 function. The obvious thing to do now was to try a bruteforce attack starting with N=1 and running until a match is found. But I really wanted to try solving it more intelligently with Picat's constraint solvers, so I spent several days coming up with a version that works without mutating updates (by writing new values to fresh slots in a list rather than updating the same value), and replacing all the bitwise operations with versions the only use the basic arithmetic functions supported by Picat's constraint system.
Eventually, I got this running and producing the correct answer, but it's very slow. I'm not sure if that's due to my formulation of the problem, insufficient domain constraints or some other issue. Before getting to this point I spoke to Hakan Kjellerstrand who suggested treating the input as a list of boolean bits, since he has some example code for doing constrained bitwise operations in this format. I stuck with a list of integers representing byte values because that seemed simpler, but it may have been the wrong choice. The most successful of the constraint-solving version was with the sat module with the default options, which produced the correct answer for part 1 in 33 minutes, which I was happy to see, but it's not so impressive compared to the 15 seconds needed by the brute force version.
This required almost no changes from part 1, just checking for a match with "000000" at the beginning rather than "00000". I figured this would be impractical, but it completed in 6m 17s using my fairly naieve Picat implementation of MD5. I imagine this would only take a few seconds in Rust.
SAT/SMT/MIP solvers are magical but they aren't always the right tool. If you can bruteforce the answer in a couple of minutes, you should probably do that rather than spending hours or days converting the problem for SAT/MIP/SMT solvers.
Here are some of the more confusing errors I ran into while working on this. Again, most of these didn't produce any line numbers, so it was hard to localise the problem:
*** error(type_error(list,[a,b,c,d,e,f|]),length)
Caused by "abcdef" ++ chr(0x80) (should have appended [chr(0x80)])
*** error(type_error(evaluable,a/0),* /2)
*** error(integer_expected([1635778560]),to_radix_string)
*** error(instantiation_error,> /2)
No clue. The operator > isn't used anywhere in the program.
*** error(type_error(evaluable,length/1),(-)/2)