In the MDD approaches, models become the primary artifact
of the development process and the basis for code generation. Identifying
defects early, at the model-level, can help to reduce development costs
and improve software quality. There is an emerging need for verica-
tion techniques usable in practice, i.e. able to nd and notify defects in
real-life models without requiring a strong verication background or ex-
tensive model annotations. Some promising approaches revolve around
the satisability property of a model, i.e. deciding whether it is possible
to create a well-formed instantiation of the model. We will discuss ex-
isting solutions to this problem in the UML/OCL context. Our claim is
that this problem has not yet been satisfactorily addressed.