We propose a “Sharp” disjunctive decomposition approach for language emptiness checking which is specifically targeted at “Large” or “Difficult” problems. Based on the SCC (Strongly-Connected Component) quotient graph of the property automaton, our method partitions the entire state space so that each state subspace accepts a subset of the language, the union of which is exactly the language accepted by the original system. The decomposition is “sharp” in that this allows BDD operations on the concrete model to be restricted to small subspaces, and also in the sense that unfair and unreachable parts of the submodules and automaton can be pruned away. We also propose “sharp” guided search algorithms for the traversal of the state subspaces, with its guidance the approximate distance to the fair SCCs.