The challenge description for this one tells us that there is a server running at the address that will load a given regex and only return the flag if the string supplied does not match the loaded regex. The regex file starts by specifying that the string must be composed of only the letters in ‘plaidctf’ and 171 characters long. It is then followed by thousands of OR-ed regex statements specifying which characters can be in each position.
The first thing I did was write a parser to break up each of the regex statements and determine constraints being placed on each character in the 171 length string. I toiled around for a couple hours, naively trying to brute force the string by iteratively passing strings through the regex statements. After I good while I decided I needed to turn this regex into a system of boolean equations and hope there was a solution.
Parsing the regex into boolean equations yields over 2500 equations that read as this, (index != these values) OR-ed together. I determined that I needed a fancy SAT solver like Z3 to plug these equations into.
After perusing the documentation, I decided I probably needed to script the creation of the SAT solving script since there were so many equations and variables. I created a mapping from the allowed letters to numbers so Z3 could operate on them more easily. The script transcribes each regex into a boolean equation like the example below. Once I got the SAT solving script setup, I went to bed and woke up to my solution.
Or( And( c88 != 0, c88 != 2, c88 != 4, c88 != 6), And( c149 != 1, c149 != 3, c149 != 5, c149 != 7), And( c156 != 0, c156 != 1, c156 != 2, c156 != 3))