In larger, more complicated models, Simulink® Design Verifier™ uses mathematical techniques to simplify the analysis:
It identifies portions of the model that do not affect the desired objectives.
It discovers relationships within the model that reduce the complexity of the search.
It reuses intermediate results from one objective to another.
In this way, the problem is reduced to a search though the logical values that describe your model.
For detailed information about analyzing large models, see Analyze a Large Model.