Awesome, thanks for mentioning this! I completely forgot about 2-literal watching and I hadn't ever thought about the idea that it'd be difficult to implement f

Awesome, thanks for mentioning this! I completely forgot about 2-literal watching and I hadn't ever thought about the idea that it'd be difficult to implement functionally. It's absolutely clever. And one other intuition I would like to add to it is that, from the way I see it at least, it is a cheap "detector" for when 3-SAT degenerates into 2-SAT, which finally becomes polynomial-time solvable -- which is exactly the kind of thing you want to have a detector for!