Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking