Fourier-Motzkin für SAT?

(Wiederholung F-M)

$\exists$ x : K₁ $\le$ x $\wedge$ ... $\wedge$ K_p $\le$ x $\wedge$ x $\le$ G₁ $\wedge$ ... $\wedge$ x $\le$ G_q

$\iff$ $\bigwedge_{{1\le i\le p, 1\le j\le q}}^{}$ K_i $\le$ G_j

vergleiche mit Resolution:

(A $\displaystyle \vee$ x) $\displaystyle \wedge$ (¬x $\displaystyle \vee$ B)	$\displaystyle \Rightarrow$	(A $\displaystyle \vee$ B)
(¬A $\displaystyle \to$ x) $\displaystyle \wedge$ (x $\displaystyle \to$ B)	$\displaystyle \Rightarrow$	(¬A $\displaystyle \to$ B)
(¬A $\displaystyle \le$ x) $\displaystyle \wedge$ (x $\displaystyle \le$ B)	$\displaystyle \Rightarrow$	(¬A $\displaystyle \le$ B)

Elimination von x durch vollständige Resolution

(A₁ $\vee$ x,..., A_p $\vee$ x) mit (¬x $\vee$ B₁,...,¬x $\vee$ B_q)

Übung: unit propagation als Spezialfall

Projekt: SAT-Solver bzw. Präprozessor bauen

2009-06-22