A SAT-based decision procedure for ALC