**FiniteSat **detection method** **is** **a linear programming based method for detecting finite satisfiability problems in class diagrams with *multiplicity constraints*, *class hierarchies* and *generalization set constraints. *The algorithm transforms class diagram constraints into an inequality system and returns *true* if the inequality system is solvable (the class diagram is finitely satisfiable) and *false* if otherwise.

*true*

*false*

**The algorithm**

**Example**

**Limitation: **The **FiniteSat** algorithm is *sound* and *complete* if class hierarchy cycles (i.e. the undirected graph of the class hierarchy is *cyclic*) do not include disjoint or complete constraints. Otherwise, **FiniteSat** is *sound* but *incomplete. *For example, consider the following four class diagrams below. The class diagram in Figures a and b are non finitely satisfiable. However, the **FiniteSat** algorithm returns a positive answer for both. The class diagrams in Figures c1 and c2 are semantically equivalent however their inequality systems are not.

*sound*

*complete*

*sound*

**Warning Method**: Due to the limitation of the **FiniteSat** algorithm, positive answers of **FiniteSatUSE** tool’s detection-method triggers an application that provides a *warning* if the class diagram includes class hierarchy cycles with disjoint or complete constraints (called **problematic*** cycles*) , and singles out all such cycles. The FiniteSatUSE tool suggests activating the propagation method if the class diagram includes **problematic**** cycles ** followed by reactivation the detection method.

*warning*

**problematic**

*cycles*)**problematic**