unsat, Resolution

Satz: F in CNF nicht erfüllbar $\iff$ es gibt eine Resolutions-Ableitung der leeren Klausel.

ein Resolutions-Schritt:

$${\frac{{(x_1 \vee \ldots \vee x_m \vee y), (\neg y \vee z_1 \vee \ldots \vee z_n)}}{{x_1 \vee \ldots \vee x_m \vee z_1 \vee \ldots \vee z_n}}}$$

Beweis: 1. Korrektheit ( $\Leftarrow$), 2. Vollständigkeit ( $\Rightarrow$)

• moderne SAT-Solver können solche Beweise ausgeben
• es gibt nicht erfüllbare F mit (exponentiell) großen Resolutionsbeweisen (sonst wäre NP = co-NP)
• falls Konflikt durch Unit Progagation: (kurzer) Resolutionsbeweis $\Rightarrow$ neue Klausel