Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis