Příklady VPL ZS 2021/22

v.1.4.3
Požadavky: 2/3 bodů z možných, tj. zadaných příkladů. Příklad za 5 bodů, pokud není řečeno jinak. Standardní doba pro řešení: 1 týden, tj. do dalšího cvičení.
Zadání: přes Moodle
Odevzdávání: přes Moodle
Výsledky: přes Moodle

Cvičení 1.

  1. Sestrojte pravdivostní tabulky pro následující formule:
    • a) $((p \to q ) \to p) \to p$ **
    • b) $\neg (p \vee q) \leftrightarrow \neg p \wedge \neg q$
    • c) $(p \to q \to r) \to (p \to q) \to (p \to r)$
    • d) $((p \leftrightarrow q)\leftrightarrow r) \leftrightarrow (p \leftrightarrow ( q\leftrightarrow r))$ , asociativita ekvivalence
    • e) $((p \to q)\to r) \leftrightarrow (p \to ( q\to r))$ , asociativita implikace
  2. Navrhněte jazyk, relace a teorie pro
    • a) obyčejné orientované grafy bez násobných hran
    • b) grafy bez smyček
    • c) neorientované grafy
  3. Vyjádřete formulí 1. řádu (v jazyce teorie grafů)
    • a) v grafu existuje cesta délky 4
    • b) v grafu existuje kružnice délky 4
    • c) $u$ a $v$ mají aspoň jednoho společného souseda
    • d) existují tři nezávislé hrany
    • e) existuje cesta mezi $u$ a $v$ délky $n$, kde $n>0$ je předem dané
    • e1) existuje cesta mezi $u$ a $v$ délky nejvýše $n$, kde $n>0$ je předem dané
    • f) v grafu existuje vrchol stupně 1
    • g) graf je regulární stupně 3
    • h) existuje vrcholové pokrytí velikosti $n$, kde $n>0$ je předem dané
    • i) ... klika, nezávislá množina ... , dané velikosti $n$
    • z1) graf je hvězdička: jeden centrální vrchol je spojen se všemi ostatními a ostatní nejsou propojeny, v teorii grafů: $\exists x ((\forall y (x\not= y \to xHy)) \wedge \forall y \forall z (x \not= y \wedge x \not= z \to \neg yHz))$ ; první část charakterizuje centrální vrchol $x$ v neorientovaném grafu bez smyček, druhá zakazuje hrany mimo centrální vrchol.
    • z2) totéž, v teorii množin: $... $
  4. Sestrojte formule 2. řádu (v jazyce teorie grafů) vyjadřující
    • a) existuje bipartitní rozklad, (Bipartitní graf $G$ lze charakterizovat pomocí "$G$ nemá cyklus liché délky", ale to se tady nehodí.)
    • b) existuje perfektní párování
    • c) existuje cesta mezi $u$ a $v$
    • d) existuje obarvení grafu třemi barvami
    • e) existuje obarvení grafu $n$ barvami, kde $n>0$ je předem dané
    • f) graf má tvar vrstveného grafu s $n$ vrstvami, kde $n>0$ je předem dané (tj. všechny hrany vedou z vrstvy $i$ do vrstvy $i+1$)
    • g) ...
    • z1) (v teorii množin) Existuje rozklad vrcholů na dvě neprázdné třídy X a Y s vlastností $\phi(X,Y)$:
      $\exists X \exists Y (X \cap Y = \emptyset \wedge X \cup Y = V_{G} \wedge X\not= \emptyset \wedge Y \not= \emptyset \wedge \phi(X,Y) )$
      s komentářem: $\exists X \exists Y (X \cap Y = \emptyset \wedge ...$ ... ; existují dvě třídy X a Y, které mají prázdný průnik a (A)...
      ... $X \cup Y = V_{G} \wedge$ ... ; jejich sjednocení je celá množina vrcholů a ... (B)
      ... $X\not= \emptyset \wedge Y \not= \emptyset \wedge \phi(X,Y) )$ ... ; obě jsou neprázdné a platí $\phi(.,.)$ (C)
    • z2) Totéž, v teorii grafů (zjednodušte/zkraťte): $X$ a $Y$ jsou unární predikáty:
      $\exists X \exists Y (\forall x (\neg (X(x) \wedge Y(x)) \wedge (X(x) \vee Y(x))) \wedge \exists x X(x) \wedge \exists y Y(y) \wedge \phi(X,Y) )$
  5. Je dán (neorientovaný) graf $G$ a dva jeho vrcholy $u$ a $v$. Sestrojte výrokovou formuli (algoritmicky, v závislosti na $G$), která je splnitelná, právě když
    • a) $G$ je bipartitní
    • b) $G$ má perfektní párování
    • c) v $G$ existuje cesta mezi $u$ a $v$
    • d) graf je obarvitelný 3 barvami
    • e) graf má cestu délky 4
    • (f) v $G$ existuje f.1) klika velikosti $n$, f.2) nezávislá množina velikosti $n$, f.3) vrcholové pokrytí velikosti $n$, f.4) obarvení grafu $n$ barvami, kde $n>0$ je předem dané
    • z) graf $G$ je hvězdička (viz výš), s $n$ vrcholy: Pro vrchol $v_i$ zavedeme (výrokovou) proměnnou $x_i$ charakterizující "$v_i$ je centrální vrchol" a proměnné $h_{ij}$ pro "existenci hrany $e_{ij}$ mezi $v_i$ a $v_j$". Formule: $(\bigvee_{i=1}^n x_i) \wedge \bigwedge_{i=1}^n \bigwedge_{j=1,j\not= i}^n (\neg x_i \vee \neg x_j) \wedge \bigwedge_{i,j=1}^n (x_i \to h_{ij}) \wedge \bigwedge_{i,j=1, i\not= j}^n (\neg x_i \wedge \neg x_j \to \neg h_{ij}) \wedge \bigwedge_{e_{ij} \in G} h_{ij} \wedge \bigwedge_{e_{ij} \not\in G} \neg h_{ij}$
      neformálně vyjadřuje: "aspoň 1 vrchol je centrální" a "nejsou dva centrální vrcholy" a "centrální $x_i$ je spojen se všemi (včetně smyčky)" a "lib. dva necentrální vrcholy nejsou spojeny" a "hrany jsou v $G$" a "hrany nejsou v $G$". Poslední dvě části formule závisí na konkrétních hranách v zadaném grafu $G$.
    • Poznámky:
    • a) Formule není v CNF, převeďte do CNF.
    • b) V poslední části jsou jednotkové klauzule. Jejich propagací můžeme (my nebo SAT solver, např. v preprocesingu) formuli zjednodušit. Může se stát, že se formule zjednoduší až na True nebo False.
    • c) Ohodnocení $v(h_{ii})=1$ (ve třetí části) jako smyčku si můžeme při převodu na SAT dovolit. Je to "interní" reprezentace, podobná zarážce v programování. (Při převodu na řešení (v následující podúloze) hodnoty $v(h_{ii})$ ignorujeme. Taky je můžeme (v rámci odstraňování symetrií) vynutit přidáním do formule (do části 5). A nejlepší je vynechat proměnné (a příslušné části formule) úplně). (Meta: KISS: Keep It Simple, Stupid; "Sága jako o SGML.")
    • d) Pravdivému ohodnocení formule odpovídá konkrétní splnění podmínky v grafu (tzv. svědek), které můžeme zrekonstruovat.
    • e) Odstraňte symetrie ve formuli, např. u $h_{ij}$. (Při řešení pomocí SAT solverů je odstranění symetrií a následné zmenšení formule (vzhledem k počtu spojek nebo proměnných) obvykle lepší řešení než "zlepšení propagace"zavedením $h_{ij} \leftrightarrow h_{ji}$ )
    • Globální poznámky:
    • i) Předbíháme, bude ještě na ADS2. Většinou chceme formuli v CNF a polynomiálně velkou k $G$.
    • ii) Pro podobné grafové úlohy v minulých úlohách chceme 3 odlišné věci: 1) navrhnout jazyk a teorii; 2) vyjádřit formulí; 3) převést na výrokovou formuli.
  6. Formalizujte s relací dělitelnosti $m|n$ ($m$ dělí $n$) v teorii množin:
    • a) $z$ je společný dělitel $x$ a $y$
    • b) $z$ je největší společný dělitel $x$ a $y$
    • c) $z$ je největší společný dělitel všech čísel z množiny $X$
  7. Formalizujte v jazyce s relacemi $P(x)$ vyjadřující "$x$ je prvočíslo" a $R(x,y)$
    • a) pro nějaké prvočíslo $x$ máme prvek $y$, že platí $R(x,y)$
    • b) pro každé prvočíslo $x$ máme prvek $y$, že platí $R(x,y)$
    Pozn.: V PL nemáme sorty (druhy/typy prvků), proto pokud chceme charakterizovat nebo vybírat pouze z nějakých prvků, potřebujeme je určit a vhodně spojit se zbytkem formule.
  8. Formalizujte v jazyce s $\le$ a rovností
    • a) $x$ je minimální prvek, (tj. neexistuje menší)
    • b) $x$ je nejmenší prvek (tj. je menší než ostatní prvky),
    • c) $x$ má bezprostředního předchůdce,
    • d) každé dva prvky mají nejmenšího společného následníka.
  9. Formalizujte v jazyce s rovností pro dané $n$
    • a) existuje nejvýš $n$ prvků
    • b) existuje aspoň $n$ prvků
    • c) existuje právě $n$ prvků
    • d) Lze vyjádřit "existuje nekonečně mnoho prvků"? (proč ne, případně jak ano)
  10. Hra dvou hráčů. Mějme konečnou hru dvou (střídajících se) hráčů. Hra končí po $n$ kolech výhrou jednoho ze dvou hráčů označených $X$ a $Y$, přičemž $X$ začíná. Hra je zadána formulí $\varphi(x_1, y_1, ... , x_n, y_n)$ vyjadřující, že ve hře s tahy $x_1, y_1, ... , x_n, y_n\,$ vyhrává $X$. Pomocí kvantifikátorů sestrojte formuli vyjadřující
    • a) "$X$ nemůže prohrát",
    • b) "$Y$ nemůže prohrát",
    • c) "$X$ má vyhrávající strategii",
    • d) "$Y$ má vyhrávající strategii".
  11. Strukturální rekurze. Dokažte, že formule, která neobsahuje negaci (ale jen $\vee$, $\wedge$ , $ \to$, $\leftrightarrow$ a proměnné), je splnitelná. Hint: Pokud je ohodnocení všech proměnných pravda, pak celá formule je pravdivá.

  12. a) Navrhněte jazyk pro posloupnosti, tj. řetězce.
    b) Definujte teorie pro relace předpona $P_2$ (\(P(x,y)\) pro "\(x\) má předponu \(y\)") , přípona $S_2$, (spojitý) podřetězec $U_2$, (nespojitá) podposloupnost $W_2$ a obrácení řetězce $R_2$.
    Pozn.: Algebraická struktura monoid: asociativní binární operace (binární funkční symbol), s neutrálním prvkem (konstantní, nulární funkční symbol).

Cvičení 2

  1. Zapište a/nebo zakreslete vytvořující strom formule $\neg(p \to \neg q) \to (q \vee \neg r) $.
    • p) Jaké jiné zápisy struktury výrazů (termů) znáte, např. z programování? Použijte je.
  2. Zapište v CNF a DNF formuli $f(p,q,r)$ nad $\{p, q, r\}$:
    • a) parita , tj. lichý počet pravdivých prvovýroků,
    • b) majorita, tj. aspoň polovina pravdivých prvovýroků,
    • (a.1) pro paritu (i majoritu) vycházejí velké formule. Víte zdůvodnit proč?
    • (a.2) Máte spojku xor (vylučovací nebo, $\otimes$). Dokážete zapsat paritu malou formulí?
    • (a.3) Najdete jinou formuli, která bude mít dlouhý zápis?
    • c) Najděte formuli (lze v DNF), která po převodu do CNF bude mít exponenciálně dlouhý zápis.
  3. Univerzální množiny spojek.
    • a) Určete, které z následujících množin spojek jsou univerzální: 1: $\{\vee,\wedge,\neg\}$, 2: $\{\vee,\wedge\}$, 3: $\{\vee, \neg\}$, 4: $\{\to,\neg\}$, 5: $\{\to,\neg,\vee,\wedge\}$, 6: $\{\downarrow \}$, 7: $\{\uparrow \}$, 8: $\{\vee, \wedge, \to\}$, 9: $\{\vee, \to, \leftrightarrow \}$.
      Pozn.: šipka dolu: Peirceova spojka, NOR (TeX: downarrow); šipka nahoru: Shefferova spojka, NAND (TeX: uparrow)
    • b) Pokud je nějaká množina spojek $S$ univerzální, je každá její nadmnožina $S'$, $S \subseteq S'$, univerzální?
    • (c) Jakým způsobem lze dokázat, že nějaká množina spojek není univerzální?
  4. Převeďte dané formule do CNF a DNF i) tabulkou (tj určením modelů) a ii) ekvivalentními úpravami
    • a) $(p \lor \neg q) \to (q \vee \neg r)$ **
    • b) $(\neg p \to (\neg q \to r)) \to p $
    • c) $((p \to \neg q) \to r) \to q $
    • d) $(\neg p \wedge q) \to (\neg q \leftrightarrow r)$
  5. Pomocí implikačního grafu rozhodněte o splnitelnosti formule.
    • a) $(x_1 \lor \neg x_2) \wedge (x_2 \lor x_3) \wedge (\neg x_3 \lor \neg x_1) \wedge (\neg x_3 \lor \neg x_4) \wedge (x_4 \lor x_5) \wedge (\neg x_5 \lor \neg x_1)$
    • b) $(x_1 \lor \neg x_2) \wedge (x_2 \lor x_3) \wedge (\neg x_3 \lor x_1) \wedge (\neg x_3 \lor \neg x_4) \wedge (x_4 \lor x_5) \wedge (\neg x_5 \lor x_1)$
    • c) $(x_1 \lor x_2) \wedge (\neg x_2 \lor x_3) \wedge (\neg x_3 \lor x_1) \wedge (\neg x_3 \lor \neg x_4) \wedge (x_4 \lor x_5) \wedge (\neg x_5 \lor x_2)$
  6. Pomocí jednotkové propagace zjednodušte a rozhodněte o splnitelnosti formule: **
    • a) $x_1 \wedge (\neg x_1 \lor x_2) \wedge (\neg x_1 \lor \neg x_3) \wedge (\neg x_2 \lor x_3 \lor x_4) \wedge (\neg x_4 \lor x_5 \lor \neg x_6)$
    • b) $x_1 \wedge (\neg x_1 \lor x_2) \wedge (\neg x_1 \lor \neg x_3) \wedge (\neg x_1 \lor x_3 \lor x_4) \wedge (x_3 \lor \neg x_4)$
  7. Pro testování splnitelnosti máte formule zjednodušit a případně popsat použitou úvahu/pravidlo obecně: ("ekvisplnitelnost", "subsumpce" kl. i hodnot)
    • a) $(x_1 \lor \neg x_3) \wedge (x_1 \lor x_2 \lor \neg x_3)$
    • b) $(x_1 \lor \neg x_2) \wedge (x_2 \lor x_3) \wedge (\neg x_3 \lor x_1)$
  8. Uvažme teorii $T=\{\neg q \to (\neg p \vee q), \neg p \to q, r \to q \}$. Které výroky jsou pravdivé / lživé / nezávislé / splnitelné / ekvivalentní v $T$?
    • $p,q,r,s$
    • $p \to \neg q, \neg q \to p, \neg q \to \neg p, \neg q \to q$
  9. Uvažme teorii $T=\{p_i \to p_{i+1} | i \in \mathbb{N}\}$ nad var($T$).
    • a) Které výroky ve tvaru $p_i \to p_{j} $ jsou důsledkem $T$?
    • b) Určete všechny modely teorie $T$.
  10. Uvažme teorii $T=\{p_i \to p_{i+1} \vee q_{i+1}, q_i \to p_{i+1} \vee q_{i+1}| i \in \mathbb{N}\}$ nad var($T$).
    • a) Které výroky ve tvaru $p_i \to p_{j} $ jsou důsledkem $T$?
    • b) Které výroky ve tvaru $p_i \to (p_{j} \vee q_{j})$ jsou důsledkem $T$? (opraveno)
    • c) Určete všechny modely teorie $T$.
  11. Které všechny pravidla potřebujete, abyste mohli převést lib. formuli do CNF, resp. DNF? (Předn.) **

  12. Uvažme teorii $T=\{p_i \wedge p_{i+1} \to p_{i+2} | i \in \mathbb{N}\}$ nad var($T$).
    • a) Které výroky ve tvaru $p_i \to p_{j} $ jsou důsledkem $T$?
    • b) Určete všechny modely teorie $T$.
  13. Pro formuli nad $n$ proměnnými a $k$ spojkami odhadněte
    • a) počet výskytů proměnných, označme $m$
    • b) počet podformulí
    • c) časovou složitost tabulkové metody, v závislosti na $n$, $m$ a $k$ (pro určení tautologie a/nebo splnitelnosti)
    • d) paměťovou složitost;
    • Pozn.: případně optimalizujte (výběr proměnných, výběr hodnot), když hledáte nějaké pravdivé, resp. nepravdivé, ohodnocení pro splnitelnost, resp. vyvrácení tautologie.
  14. Pro formuli $\neg(p \to \neg q) \to (q \vee \neg r) $ určete modely (nad $\{p,q,r\}$) a použitím pravidel převeďte do CNF a DNF. **
  15. (QBF, Kvantifikované Boolovské Formule) QBF dovolují pro výrokové proměnné kvantifikátory ve formuli, tj. $(\forall p)\phi$ (A) a $(\exists p) \phi$ (B) jsou formule pro libovolnou QBF $\phi$, s významem A, resp. B, je pravdivá, pokud $\phi$ je pravdivá pro obě hodnoty $p$, resp. pro aspoň jednu hodnotu $p$. (Splnitelnost definujeme analogicky.)
    • a) Navrhnout algoritmus a/nebo upravit tabulkovou metodu pro a.1) pravdivost a.2) splnitelnost
    • b) odhadnout složitost algoritmu, časovou i paměťovou
    • c) navrhnout převod na nekvantifikované formule VL, když c.1) máme $\top$ a $\bot$ (True a False); c.2) nemáme výrokové konstanty; c.3) a dokázat správnost převodu,
    • d) analyzovat složitost převodu; je polynomiální?

Dodatek: SAT solvery

  1. SAT solver
    • Solver sat4j z sat4j.org, potřebuje Javu. (Místo solveru glucose.)
    • volání: "java -jar sat4j-sat.jar testy/boarddomino4.cnf"
    • soubor solveru sat4j-sat2007.jar nebo v sat4j-sat4j-sat-v20130419.zip
    • Soubory .cnf jsou v DIMACS formátu pro CNF. Taky se používá DIMACS formát pro grafy.
  2. Příklady:
    • podle PG: Sestrojte výrokovou formuli, která je splnitelná, když úloha splňuje podmínky (pro dané $n$).
    • 1. Při obarvení čísel $1,...,n$ dvěma barvami, neexistuje monochromatické řešení rovnice $a+b=c$ pro $1\le a\lt b \lt c\le n$.
    • 2. (DU2/2020) V posloupnosti $n$ nul a jedniček, neexistují tři $0$ nebo tři $1$ se stejnými vzdálenostmi.
    • 3. Dvě množiny $\{1,...,n\}$ jdou uspořádat do posloupnosti délky $2n$ tak, že vzdálenost mezi čísly $k$ je právě $k$.
    • 4. Existuje obarvení grafu G, pevným počtem barev $n$.
    • Varianty: víc než 2 barvy (pro 1.), víc než 2 znaky (pro 2.).
    • 5. Graf je bez trojúhelníků.
    • 6. z ADS2: Hamiltonovská kružnice.
    • 6.b varianta: Hamiltonovská cesta; 6.c Hamiltonovská cesta z $u$ do $v$.
    • 7. Graf G je bipartitní.
    • 7.b Pro minulý problém, vyšla vám formule v CNF ve tvaru 2-SAT? Pokud ne, najděte jinou reprezentaci.
    • 8. Sudoku má řešení. 8.b Kakuro, číselná křížovka, má řešení. 8.c A další.
    • 9.a Vyřešit Lloydovu 15 ze zadané pozice na $k$ tahů. Lloydova 15 obsahuje 15 kostiček s čísly v čtverečkové mřížce $4 \times 4$ a jedno pole zůstává prázdné. Tah je přesun očíslované kostičky na sousední volné pole. Koncová vyřešená pozice obsahuje čísla od 1 od levého horního rohu po řádcích, pak po sloupcích, a volné pole je vlevo dole. (Reprezentace posloupnosti stavů.)
    • 9.b (Jednodušší:) 8 kostiček a jedno prázdné pole v mřížce $3\times 3$.
    • 10.a Pro úlohu 4. Barvení převodem na SAT navrhněte způsob odstraňování (některých) symetrií. Tj. pro řešení SAT, která odpovídají v principu stejnému rozdělení vrcholů podle barev, chcete jedno z řešení vybrat a další zneplatnit.
      (Odstranění symetrií zmenší prohledávaný prostor, což je vhodné speciálně pro UNSAT problémy.)
    • 10.b Odstraňování symetrií pro jiné úlohy, 1-6.
    • 11.a Pro úlohu 4 navrhněte způsob rozdělení velkého problému barvení na menší problémy, které půjdou zpracovávat paralelně, případně sekvenčně, a ze kterých jste schopni sestavit barvení celého původního grafu.
      i) Popište na úrovni domény, tj. barvení grafu.
      ii) Jak lze rozdělení realizovat při generování anebo pomocí transformace .cnf souboru.
    • 11.b Rozdělení na menší problémy pro jiné úlohy, 1-6.
    • 12. Jak lze rozdělování SAT problémů realizovat obecně na úrovni .cnf souborů, tj. pomocí transformace .cnf souborů? (Tj. "černá skříňka".) Jaké techniky lze použít pro rozdělování, pokud víme způsob generování SAT problémů? (Tj. "bílá skříňka".)
    • 13. SAT solver vydal řešení, které uživateli nevyhovuje. Jak můžeme (transformací .cnf souboru) získat další, jiné řešení?
    • Pozn. Obecně dva přístupy: úprava instance vs. úprava generátoru. V prvním případě upravujeme data, v druhém program.
    • 14. Pro dvě přirozená čísla $x$ a $y$ požadujeme $x\le y$ pro odstranění symetrie. Jak se liší implementace tohoto odstraňování symetrií při unární (1-hot) a binární reprezentaci čísel?
    • 99. (Předn.) Lze desku $4\times 4$ bez 2 protilehlých rohů pokrýt úplně kostičkami domina? (vzorový soubor boardomino4.cnf)
  3. Poznámky
    • Převody do SAT: různé kódování. Tradeoff: vliv na počet proměnných, délku klauzulí, počet klauzulí (včetně režijních klauzulí, například: právě 1 z $n$, zakázaná barva 4 (=11) při obarvení 3 barvami), možnosti propagace hodnot (paměť vs. čas). Rekonstrukce řešení (pro uživatele).
    • Převod formule do CNF (pro solvery). Přímočaře exponenciální převod (rozdistribuováním), ale jde převést lineárně při přidání proměnných pro podformule (Tseitinova transformace).
    • "Programování" v SAT. Deklarativní popis problému, v CNF. SAT jako univerzální solver (pro konečné domény), nepotřebujeme psát (... a ladit a optimalizovat) programy pro jednotlivé problémy. Optimalizace technologie (a heuristiky) pomůže pro mnoho problémů (ale pro jednotlivé problémy může být vhodnější různé nastavení). Solvery jako nástroje, off-the-shelf (chceme spolehlivé, ověřené, dokumentované, udržované, ...). Převod problému na SAT se používá v praxi (jako jeden z přístupů), je vhodné mít GUI/prostředí.
    • Podobné problémy nebo varianty problému SAT: MAXSAT, 1-in-3-SAT, vážený SAT (jiné vstupní formáty), CSP+převod na SAT.
    • Nesymetrie ověřitelnosti: řešení pro SAT/splnitelné (jednoduše ověřitelné pomocí ohodnocení jako svědka) vs. strom výpočtu pro UNSAT. (SAT pro nalezení (proti)příkladu - záleží na otázce/formulaci problému.)
    • Odstraňování symetrií, rozdělení výpočtu např. pro paralelní zpracování, dodatečné vstupní podmínky. (Superpozice při rezoluci.)
    • Interně v solverech: často prohledávací algoritmus DPLL - úplné procházení možných přiřazení proměnných (tj. stavového prostoru) pomocí backtrackingu (s vylepšeními (CDCL - Conflict Driven Clause Learning, ...) a heuristikami (pro výběr proměnných i hodnot)). Jiná možnost je neúplné prohledávání pro splnitelné formule, které neověří nesplnitelnost (UNSAT). Aplikace neúplného prohledávání je, když splnitelná formule popisuje chybu, zakázaný stav nebo zakázanou posloupnost stavů (délku posloupnosti prodlužujeme, dokud to technologie zvládá).
    • Složitost: Pro problém SAT není známý polynomiální algoritmus, pouze exponenciální (více bude na ADS2). Při vytváření instance (popisu v) SAT pro nějakou instanci jiného problému, chceme polynomiálně velkou formuli. (Proti)příklad: naivně/přímočaře vytvořená formule (kde jedna klauzule odpovídá jedné klice) v CNF je splnitelná, pokud v daném grafu $G$ existuje klika (nebo nezávislá množina) velikosti $k$. Taková formule je velká, chceme jiný lepší popis.
    • Ekvisplnitelnost při transformacích formule: zachování splnitelnosti i nesplnitelnosti, zachování svědka/důkazu (ve VL splňující ohodnocení). Ve VL, v ekvisplnitelné formuli můžeme pro nové proměnné zvolit jejich hodnoty. (Ekvisplnitelnost bude i v pred.logice; podobný koncept je v ADS2 při NP-úplnosti, i když se tak nenazývá.)
    • Pro SAT: Fázový přechod s těžkými instancemi leží mezi podspecifikovanými (obvykle řešitelnými) a přespecifikovanými (obvykle neřešitelnými, UNSAT) instancemi. Obvykle: podspecifikované problémy mají mnoho řešení a téměř libovolná volba prvních proměnných se dá s malým prohledáváním doplnit na řešení; přespecifikované problémy dojdou ke sporu často v malé hloubce. V obou případech prohledáváme pouze část stromu možností. Pro UNSAT problémy, optimalizace výstupu: unsatisfiable core - množina (proměnných a) klauzulí, které nejdou splnit.
    • Pragmaticky, na ověřování vypsaného ohodnocení (nebo důkazu) se používá samostatný program, protože je jednodušší (tudíž lépe zkontrolovatelný), nemá heuristické (až nekorektní) optimalizace a nepotřebuje tolik paměti.
    • Rozšíření SAT na SMT, Satisfiability Modulo Theories, například pomocí algoritmu DPLL(T).
    • Rozšíření SAT na QSAT pro QBF, splnitelnost pro Quantified Boolean Formulas (= jazyk TQBF, True QBF). Příklad instance: $\forall x \exists y \exists z (x \wedge y) \vee (\neg x \wedge z)$

Cvičení 3

  1. Explicitní výsledky, reifikace
    • a) Máte formuli ve dvou výrokových proměnných, např. $\phi(x,y) = x \to \neg x \lor y$. Dokážete napsat formuli $\phi'$ v proměnných $x, y,v$, která je pravdivá, právě když $v$ je hodnota $\phi(x,y)$?
    • b) Zobecněte metodu pro lib. $\phi(x_1,...,x_n)$.
    • Pozn. Hodnota formule $\phi(x,y)$ (při nějakém ohodnocení) je definována v metajazyce VL, ne "uvnitř" formulí VL. Tento trik zavedením $v$ umožní pracovat s hodnotami formulí "uvnitř" formulí.
  2. Kolik neekvivalentních výroků lze sestavit z $n$ prvovýroků?
  3. Nechť $T$ je teorie $\{(p \land q) \to r \}$ nad ${\mathbb P} =\{ p,q,r\} $
    • a) Kolik má T modelů?
    • b) Stejná otázka, ale nad ${\mathbb P} =\{ p,q,r,s\} $
  4. Nechť T je teorie

DU a kandidáti na DU, náhradní příklady

-konec VPL

Slovníček
(Řecká písmena: ...)