Fourier-Motzkin-Verfahren

Def.: eine Ungls. ist in x-Normalform, wenn jede Ungl.

• die Form „x ( ≤   |  ≥) (Ausdruck ohne x)`` hat
• oder x nicht enthält.

Satz: jedes Ungls. besitzt äquivalente x-Normalform.

Def: für Ungls. U in x-Normalform:

U_x^↓ : = {A | (x≥A)∈U}, U_x^↑ : = {B | (x≤B)∈U},

U_x^- = {C | C∈U,$C$ enthält $x$ nicht}.

Def: (x-Eliminations-Schritt) für U in x-Normalform:

U→_x{A≤B | A∈U_x^↓, B∈U_x^↑}∪U_x^-

Satz: (U erfüllbar und U→_xV) $\iff$ (V erfüllbar).

FM-Verfahren: Variablen nacheinander eliminieren.