Literál je buď proměnná nebo její negace.

Pozitivní literál je každá proměnná <math>x</math> .

Negativní literál je každá negace proměnnej <math>\overline x</math>.

Klauzule je disjunkcí literálů, která neobsahuje dva literály s touž proměnnou <math>x ∨ \overline y ∨ \overline z</math>.

Formule <math>φ</math> je v konjunktivně normální formě (KNF), pokud je konjunkcí klauzulí <math>(x ∨ y) ∧ \overline z</math>.

Je-li <math>φ</math> formulí na n proměnných a <math>t ∈ \{0, 1\}^n</math> , pak <math>φ(t)</math> značí hodnotu <math>φ</math> v ohodnocení <math>t</math>.

Splnitelnost formule v KNF (SAT)

• Instance: Formule <math>φ</math> na <math>n</math> proměnných v KNF

• Otázka: ∃ ohodnocení, pro které je <math>φ</math> splněná?

Důkaz transformací KACHL ∝ SAT: pomocí proměnných <math>x_{ijk}</math>, kde <math>x_{ijk} = 1</math>, pokud na pozici <math>[i,j]</math> se nachází kachlík typu <math>k</math>. Jednotlivé klauzule se vytvoří tak, aby zaručovaly, že na každé pozici je právě jeden kachlík, že kachlíky navazují horizontálně, vertikálně i na kraje stěny.

{{theorem

| SAT je NP-úplný problém | NP-úplnost SAT

}}

Dk (KACHL → SAT - myšlenka)

pomocí proměnných <math>x_{ijk}</math>, kde <math>x_{ijk} = 1</math>, pokud na pozici <math>[i,j]</math> se nachází kachlík typu <math>k</math>. Jednotlivé klauzule se vytvoří tak, aby zaručovaly, že na každé pozici je právě jeden kachlík, že kachlíky navazují horizontálně, vertikálně i na kraje stěny.

Dk (KACHL → SAT)

To, že <math>SAT</math> patří do NP, plyne z toho, že pokud dostaneme vektor <math>t ∈ {0, 1}^n</math>, můžeme spočítat hodnotu φ(t) v polynomiálním čase. Certifikátem kladné odpovědi je tedy splňující ohodnocení. Toto ohodnocení je ve skutečnosti řešením úlohy splnitelnosti, v níž chceme splňující ohodnocení nalézt a ne jen zjistit, zda existuje, tato úloha tedy patří do NPF. <math>NP</math>-těžkost splnitelnosti ukážeme převodem z problému Kachlíkování. Uvažme instanci Kachlíkování danou množinou barev <math>B</math>, přirozeným číslem <math>s</math>, čtvercovou sítí <math>S</math> velikosti <math>s × s</math>, jejíž okraje jsou obarveny barvami z <math>B</math>, a množinou typů kachlíků <math>K = \{T1, . . . , T|K|\}</math>. Popíšeme, jak zkonstruovat formuli <math>φ</math> v KNF, která bude splnitelná právě tehdy, když tato instance má přípustné vykachlíkování. Formule <math>φ</math> bude využívat <math>\{ s . |K| \}</math> proměnných <math>x_{i,j,k}</math> pro <math>\{ i, j = 1, . . . , s, \}</math> a <math>\{ k = 1, . . . , |K| \}</math>. Konstrukcí formule <math>φ</math> zabezpečíme, že ve splňujícím ohodnocení bude hodnota <math>xi, j, k = 1</math> odpovídat tomu, že na políčko <math>S[i, j]</math> umístíme kachlík Tk. V konstrukci použijeme následující dvě množiny určující nekompatibilní dvojice kachlíků: ::<math>V</math> = {(p, q) | spodní barva Tp se neshoduje s horní barvou Tq},

::<math>H</math> = {(p, q) | pravá barva Tp se neshoduje s levou barvou Tq}. Množina V obsahuje dvojice typů, jež nemohou být umístěny nad sebe, tedy vertikálně. Množina H obsahuje dvojice typů, jež nemohou být umístěny vedle sebe, tedy horizontálně.

Podobné množiny si definujeme i pro barvy na okrajích, pro i = 1, . . . , s definujeme Ui, Bi, Li, Ri. ::<math>U_j</math> = {k | horní barva Tk se shoduje s barvou horního okraje S v j-tém sloupci}

::<math>B_j</math> = {k | spodní barva Tk se shoduje s barvou spodního okraje S v j-tém sloupci} ::<math>L_j</math> = {k | levá barva Tk se shoduje s barvou levého okraje S na j-tém řádku}

::<math>R_j</math> = {k | pravá barva Tk se shoduje s barvou pravého okraje S na j-tém řádku} Množina <math>Ui</math> tedy obsahuje typy kachlíků, jež mohou být umístěny na políčko <math>S[1, i]</math>, množina <math>Bi</math>

obsahuje typy kachlíků, jež mohou být umístěny na políčko <math>S[s, i]</math>, množina <math>Li</math> obsahuje typy kachlíků, jež mohou být umístěny na políčko <math>S[i, 1]</math>, a konečně <math>Ri</math> obsahuje typy kachlíků, jež

mohou být umístěny na políčko <math>S[i, s]</math>. Konstrukci formule <math>φ</math> popíšeme po částech. Formule KNF je definovaná množinou svých klauzulí (jejich konjunkcí získáme danou formuli). Konjunkce několika KNF je KNF.

1. Pro <math>\{ i, j = 1, . . . , s \}</math> definujeme: <math>C_{i, j} = (x_{i,j,1}\vee x_{i,j,2} \vee ... \vee x_{i,j,K} )</math>. Tyto klauzule v budoucí CNF vynucují, že na každém políčku je aspoň 1 typ kachlíku.

2. Pro <math>\{ i, j = 1, . . . , s \}</math> definujeme: <math>\alpha_{i, j} = \wedge_{k = 1..K} \wedge_{l=(k+1)..K}(\neg x_{i,j,k} \vee \neg x_{i,j,l})</math>. Tyto klauzule vynucují, že každému políčku <math>S[i, j]</math> je přiřazen nejvýš jeden typ kachlíku.

3. Pro <math>\{ i, j = 1, . . . , s \}</math> definujeme: <math>\beta_{i, j} = C_{i, j} \wedge \alpha_{i,j}</math>. Formule <math>βi, j</math> je tedy splněna, pokud políčku <math>S[i, j]</math> přiřadíme právě jeden typ kachlíku.

4. Pro <math>\{ 1 ≤ i ≤ (s – 1) \}, \{ 1 ≤ j ≤ s \}</math> definujeme: <math>\gamma_{i, j} = \wedge_{(p, q) \in V} (\neg x_{i, j,p} \vee \neg x_{(i + 1),j,q})</math>. Formule <math>\gamma_{i, j}</math> je splněna, pokud nad sebou umístěným políčkům <math>S[i, j], S[(i + 1), j]</math> nejsou přiřazeny nekompatibilní typy kachlíků.

5. Pro <math>\{ 1 ≤ i ≤ s \}, \{ 1 ≤ j ≤ (s – 1) \}</math> definujeme: <math>\delta_{i, j} = \wedge_{(p, q) \in H} (\neg x_{i, j,p} \vee \neg x_{i,(j + 1),q})</math>. Formule <math>\delta_{i, j}</math> je splněna, pokud vedle sebe umístěným políčkům <math>S[i, j], S[i, (j + 1)]</math> nejsou přiřazeny nekompatibilní typy kachlíků.

6. Definujeme: <math>\epsilon_u = \wedge_{j=1..s} [ \vee_{k\in U_j} x_{1, j, k}]</math>. Formule je splněna, pokud je na každém políčku v prvním řádku kachlík s barvou shodnou s příslušným horním okrajem.

7. Definujeme: <math>\epsilon_b = \wedge_{j=1..s} [ \vee_{k\in B_j} x_{s, j, k}]</math>. Formule je splněna, pokud je na každém políčku v nejspodnějším řádku kachlík s barvou shodnou s příslušným spodním okrajem.

8. Definujeme: <math>\epsilon_l = \wedge_{i=1..s} [ \vee_{k\in L_i} x_{i, 1, k}]</math>. Formule je splněna, pokud je na každém políčku v nejlevějším sloupci kachlík s barvou shodnou s příslušným levým okrajem.

9. Definujeme: <math>\epsilon_r = \wedge_{i=1..s} [ \vee_{k\in R_i} x_{i, s, k}]</math>. Formule je splněna, pokud je na každém políčku v nejlevějším sloupci kachlík s barvou shodnou s příslušným levým okrajem.

Formuli <math>φ</math> dostaneme jako konjunkci všech formulí výše: ::<math>φ = [\wedge_{i = 1..s; j = 1..s} \beta_{i, j}] \wedge [\wedge_{i = 1..(s - 1); j = 1..s} (\gamma_{i, j} \wedge \delta_{j,i})]

\wedge \epsilon_u \wedge \epsilon_b \wedge \epsilon_r \wedge \epsilon_l</math>. Z konstrukce okamžitě vyplývá, že <math>φ</math> je formule v KNF a že velikost <math>φ</math> je polynomiální v s a <math>|K|</math>, a v polynomiálním čase lze <math>φ</math> i zkonstruovat. Zbývá ukázat, že pro výchozí instanci problému Kachlíkování existuje přípustné vykachlíčkování, právě když <math>φ</math> je splnitelná formule. Ve skutečnosti ukážeme, že ze splňujícího ohodnocení formule <math>φ</math> lze vyčíst přípustné vykachlíkování čtvercové sítě <math>S</math> a naopak z přípustného vykachlíkování lze určit splňující ohodnocení formule <math>φ</math>.

Předpokládejme nejprve, že existuje přípustné vykachlíčkování S kachlíky z <math>K</math>. Označme pomocí <math>S[i, j]</math> index typu kachlíku, který je na i-tém řádku a j-tém sloupci. Definujme <math>xi, j, k = 1</math> právě když je na políčku <math>S[i, j]</math> umístňen kachlík <math>Tk</math>. Není těžké ověřit, že každá z podformulí <math>βi ,j, γi, j, δi, j, εu, εb, εl, εr</math> je tímto ohodnocením splněna, a tedy že i celá formule <math>φ</math> je splněna. Předpokládejme na druhou stranu, že existuje splňující ohodnocení formule <math>φ</math> a pomocí <math>v[i, j, k]</math> označme hodnotu přiřazenou proměnné <math>xi, j, k</math> ve splňujícím ohodnocení. Díky tomu, že ohodnocení splňuje i formuli <math>βi,j</math>, existuje pro každé <math>\{ i, j = 1, . . . , s \}</math> právě jedno <math>k ∈ \{1, . . . , |K|\}</math>, pro kterou je <math>v[i, j, k] = 1</math>. Na pozici <math>S[i, j]</math> tedy dáme kachlík toho typu <math>Tk</math>, pro který je <math>v[i, j, k] = 1</math>. Lze snadno ověřit, že podmínky zakódované do formulí <math>γi, j, δi, j, εu, εb, εl, εr</math> zaručují, že tímto způsobem obdržíme přípustné vykachlíkování <math>S</math>.