Příklady VPL ZS 2024/25

17.10.2024 ; v.1.4.5

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).
  13. Humor: temporální logika umožňuje například formulovat "Byl to bývalý budoucí premiér z budoucí bývalé vládní strany" (IX'2024).
    • Pozn. 1: Pragmaticky, juniorní úroveň: při převodu z přirozeného jazyka do formulí někdy musíme zachytit implicitní podmínky, které nejsou vyjádřeny explicitně. Ale pokud by platily, vyjádřily bychom skutečnost jinak. Např. pokud modální spojka pro budoucnost zahrnuje i přítomnost, obvykle chceme platnost formule v přítomnosti vyloučit, protože jinak bychom nepoužili ve vyjádření slovo "budoucí".
    • Pozn. 2: Pragmaticky, seniorní úroveň: pokud si nejste jistí, jak to uživatel myslel, zeptejte se. Např. na okrajové případy.

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í?
    • d) manažersky: d1) proč chceme velkou (univerzální) množinu spojek? Např. přidat $xor$. d2) proč chceme malou (univerzální) množinu spojek?
  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í?
    • Rezolventa jako důsledek: Pro dve vstupní formule $f1$ a $f2$ uděláme jeden rezoluční krok a dostaneme $f3$. Ukažte, že může existovat model $f3$, který není modelem $T=\{f1, f2\}$.

      Důsledek: rezolventa popisuje jinou teorii a má jiné modely než teorie vstupních formulí $T$. Ale je ekvisplnitelná, což nám při hledání sporu (tj. nesplnitelné klauzule) stačí.

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. V posloupnosti $n$ nul a jedniček, neexistují tři $0$ nebo tři $1$ se stejnými vzdálenostmi.
    • Varianty: víc než 2 barvy (pro 1.), víc než 2 znaky (pro 2.).
    • 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$.
    • 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$. A další.
    • 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ší.
    • Hint, např. pro sudoku: volba reprezentace, podmínky ("syntaktické") umožňující správnou rekonstrukci čísel/mřížky, podmínky ("sémantické") popisující správné řešení problému.
    • Jak se projeví na podmínkách, pokud jsou oblasti sudoku nepravidelné, případně pokud máme další podmínky, např. pro uhlopříčky.
    • Máme obecné podmínky pro "správně vyřešené sudoku" pro prázdnou mřížku. V zadání konkrétního sudoku je na daném políčku konkrétní číslo. Jak tuto informaci zadáme do podmínek a jak se projeví v .cnf souboru?
    • 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".)
    • 12.b Speciálně: problém je velký, ale máme k dispozici několik procesorů. Jak můžeme (vhodně) rozdělit hledání řešení (tzv. prohledávání stavového prostoru) mezi jednotlivé procesory, tak aby se problémy nepřekrývaly a z dílčích výsledků jsme byli schopni poskládat celkový výsledek?
    • 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 (doporučeno), 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?
    • 14.b Odstraňování symetrií při barvení grafu.
    • 15. Irregular strings. (Ramseyova teorie pro řetězce.) Pracujeme nad abecedou $\Sigma=\{1,...,k\}$ a pro každé $i$ máme danou hodnotu $l_i \ge 3$. Najděte co nejdelší slovo (délky $n$), které neobsahuje znak $i$ na indexech aritmetické posloupnosti délky $l_i$. Vyzkoušejte také pro $k \ge 3$. (Příklad 2. je speciální případ pro $k=2$ a $l_i=3$.)
    • 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, které se můžou hodit:
    • 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 a binární reprezentaci), možnosti propagace hodnot (paměť vs. čas). Rekonstrukce řešení (pro uživatele).
    • Reprezentace. Obvykle se pro reprezentaci $n$ možností používá unární (1-hot) reprezentace pomocí $n$ proměnných. (Protože obvykle vyjdou jednodušší formule pro podmínky.) Ze splňujícího ohodnocení chceme být schopni zrekonstruovat řešení původního problému, proto formule musí charakterizovat přesně správná řešení (instancí) problému.
    • Převod formule do CNF (pro solvery a rezoluci). 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).
      Podobně, při formulaci problému můžeme přidat proměnné pro existenci/neexistenci podobjektu na daném místě (např. v grafu nebo v posloupnosti).
      Formulace problému v CNF odpovídá zadání problému pomocí (konjunkce) podmínek; formulace v DNF odpovídá popisu možných řešení.
    • Efektivita (Efektivita bude v ADS2.) Neformálně: Chceme, aby počet proměnných popisujících úlohu byl pouze polynomiálně větší než popis vstupu úlohy. Například při hledání kliky velikosti $k$ v grafu nebo nezávislé množiny velikosti $k$ nemůžeme zavést proměnnou pro každou kliku, resp. nezávislou množinu až do velikosti $k$, protože by proměnných bylo příliš mnoho. Viz dále.
    • "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 (i zakázání minulých řešení) - lze i úpravou .CNF souboru. (Předspracování (pro zmenšení zadání): jednotková propagace, odstranění čistých literálů, zjednodušení vzájemných negací literálů ($p\leftrightarrow \neg q$), subsumpce.) Superpozice (při rezoluci).
    • Interně v solverech: většinou prohledávací algoritmus DPLL - úplné procházení (s propagací a s heuristikami :-) možných přiřazení proměnných (tj. stavového prostoru) pomocí backtrackingu (s vylepšeními (CDCL - Conflict Driven Clause Learning; Two Watched Literals - pro lepší informace o jednotkové propagaci, ...) 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 - problém Kliky v grafu: naivně/přímočaře vytvořená formule (kde jedna proměnná odpovídá jedné klice) v CNF je splnitelná, pokud v daném grafu $G$ existuje klika (nebo nezávislá množina) velikosti $k$. Možných klik je mnoho a následně 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 informace víc propagují a 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(X).
    • 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)$.
    • DIMACS formát:
    • Výhody:
    • Lze použít víc solverů na stejný vstup, nezávisle.
    • Lze použít několik parametrizací solverů.
    • Lze dělit (vhodným způsobem) vstupní úlohu, následně paralelizovat. Úprava vstupu je jednoduchá. Vstup jde předzpracovat.
    • Formát je přenosný, standardní, ustálený, univerzální, veřejný, textový, ... přímočarý, skontrolovatelný, jednoduchý, i pro velké úlohy.
    • Univerzální formát: mnoho úloh jde převést na SAT.
    • Víme, že máme solvery pro tuto úlohu. Solver je univerzální. Nemusíme psát specializované solvery pro jednotlivé úlohy. Zlepšení v solverech (nová verze, heuristiky) se projeví při řešení všech úloh.
    • Uživatelskou úlohu převádíme do tohoto formátu. Implementace převodu je jednodušší než implementace solveru. Implementace převodu je samostatná, např. v jiném jazyce.
    • Vidíme velikost zadání.
    • Překlad do CNF je v naší režii: různé způsoby reprezentace a překladu, tradeoff velikosti a propagace. Implementace v našem oblíbeném jazyce, nemusíme se přizpůsobovat jazyku knihovny/solveru.
    • Nevýhody:
    • Vyčtení uživatelských výsledků z modelu je nepřívětivé.
    • Příbuzné úlohy (jako nalezení všech výsledků, spočítání počtu výsledků, optimalizační verze) nemusí být solverem podporované. (Závisí na solveru.)
    • Nízkoúrovňové, jsou i nadstavbové nástroje (i nad CNF). -> Nevyužijí se optimalizované metody *překladu* (tady nemyslíme běh solverů).
    • Porovnání s/podle: (řešení, vstup, kontext)
    • jinými formáty a zápisy formule: SMT, fof, v logice;
    • jinými přístupy a solvery: lineární programování, integerové programování, Mixed IP, CSP, SMT;
    • jinými API;
    • offline vs. online vs. webová služba;

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

Cvičení různé

  1. Struktury.
    • a) Jsou $\mathbb{Q}\langle \sqrt 2\rangle$ a $\mathbb{Q}\langle \sqrt 3\rangle$ izomorfní?
    • b) Jsou $\mathbb{Q}\langle \sqrt 2,\sqrt 3\rangle$ a $\mathbb{Q}\langle \sqrt 6\rangle$ izomorfní?
    • c) Jak byste reprezentovali prvky, abyste mohli počítat aritmetické operace?

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

-konec VPL

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