Fourier-Motzkin-Verfahren

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

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

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

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

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

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

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

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

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

FM-Verfahren: Variablen nacheinander eliminieren.