A SAT-based Decision Procedure for ALC