Whilst SAT is NP-complete, I'm surprised to learn that 2-satisfiability can be solved with a linear algorithm: http://t.co/6oSPONVeoY