Fourier-Motzkin-Verfahren

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

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


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

Ux : = {A | (xA)∈U}, Ux : = {B | (xB)∈U},

Ux- = {C | CU,$C$ enthält $x$ nicht}.


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

Ux{AB | AUx, BUx}∪Ux-


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


FM-Verfahren: Variablen nacheinander eliminieren.



2014-07-06