Aktuální verze slidů k přednášce o obsahuje řadu chyb a nepřesností. Na této stránce budou nalezené chyby postupně vypisovány. Do slidů budou opravy zapracovány později.

Přednáška 2
Slide 23: Není jasné, proč je lepší druhá nejvyšší úroveň při návratu. Návrat na úroveň level znamená všechna rozhodnutí na úrovních větších než level zrušit a pokračovat se stávajícím ohodnocením na úrovni level (ohodnocením se myslí buď True, nebo False). Návrat na druhou nejvyšší úroveň z úrovní proměnných v konfliktní klauzuli je výhodné vzhledem k heuristice, posledně ohodnocená proměnná z těch, co vedly ke konfliktu, je odohodnocena, tím pádem má heuristika šanci zvolit jinou proměnnou. To je výhodné, protože nyní je navíc naučená konfliktní klauzule, která může ovlivnit rozhodnutí heuristiky. Je však třeba dávat pozor, aby byla zaručena úplnost konflikty řízeného backtrackingu. Lze zajistit tak, že si pamatujeme všechny konfliktní klauzule, nebo tak, že konfliktní klauzule je vždy vynucující (v tomto případě je dovoleno zapomínání naučených klauzulí).
Slide 24: Rezoluční pravidlo má v druhém řádku obsahovat (a₁ ∨ a₂ ∨ ... ∨ a_n ∨ b₁ ∨ b₂ ∨ ... ∨ b_m). Chybně je uvedena negace b_m.

Přednáška 7
Slide 6: Programy v C++ na určení pořadového čísla proměnné a znaménka literálu založené na bitových operacích jsou chybné. Nejprve je třeba říci, že literály jsou kódovány pomocí neznaménkových čísel, kde nejnižší bit je použit pro znaménko literálů (tedy určuje jeho pozitivitu/negativitu) a vyšší bity kódují pořadové číslo proměnné příslušící literálu. Například literál x₃ je kódován neznaménkovým číslem 7 (v binárním zápisu 111), literál not(x₇) je kódován neznaménkovým číslem 14 (v binárním zápisu 1110).

Program extrahující pořadové číslo proměnné z kód literálu tedy má správně být:

unsigned variable_index(unsigned literal_code)
{
  return literal_code >> 1;
}

A program zjištující pozitivitu literálů má správně být:

bool variable_index(unsigned literal_code)
{
  return literal_code & 1;
}

Pozn.: Nechť dimacs_code je kód literálu v DIMACS kódování; tedy například literál x₃ je kódován celým číslem 3, literál not(x₇) je kódován celým číslem -7. Potom literal_code = 2*|dimacs_code|+(dimacs_code > 0 ? 1 : 0), kde || značí absolutní hodnotu. Uvedený způsob kódování literálů používá SAT řešící systém MiniSAT (reversním inženýrstvím zjistil Tomáš Balyo). Hovoříme-li tedy o kódování literálů, je třeba upřesnit o jaké kódování se jedná (DIMACS nebo bitové).

Přednáška 11
Slide 30: Není uvedena podmínka na saturující systém Γ, aby skutečně při aplikaci pravidel dokud nedojde k saturaci vygeneroval úplný důkaz. Je potřeba, aby Γ byl tvořen pravidly, která používá úplná deduktivní rozhodovací procedura DEDUCE_T pro rozhodování konjuknce literálů. Jinak by systém Γ sice mohl být saturující, ale nemusel by nic dokazovat. Takto je zaručeno, že aplikujeme-li Γ na lit(&phi) můžeme vygenerovat důkaz, který by vygenerovala DEDUCE_T.