Polynomial-Time Decidability of 2-SAT