I cannot get over how viscerally brutal the difficulty options are. It is an elegant way to demonstrate the hardness of SAT.
On the contrary, I found even the “too hard” difficulty to be pretty easy to brute force. You rarely need to go more than two or three levels of assumption deep before those helpful arrows guide you to the solution / a contradiction.
Indeed. I start from the first line, keep choosing the left-most option on each row without green; when that causes a different line to be all red, I undo that selection, pick whichever one just went red, and even “too hard” solves itself mostly this way with a couple backtracks. Sometimes I can get stuck deeply wrong but following the arrows helps a lot.