Příklady VPL ZS 2019/20

v.1.4
Náhradní příklady na konci.
Výsledky: v SISu (v záznamníku učitele) u cvičení si najděte svůj pseudokód, pod tímto pseudokódem budou vaše výsledky z DU na mojí stránce.

DU1/CV1(3.10.2019): PG2018/1.2a. Pro daný graf G, sestrojte výrokovou formuli, která je splnitelná, právě když je graf bipartitní.

DU2/CV2(10.10.2019, ): SAT Solvery.2.2 Popište konstrukci formule v CNF.

DU3/CV2(do 6.11.2019 St, 10 bodů): Úloha jako DU2. a/ Nainstalujte si (některý) SAT-solver. b/ Naprogramujte vytváření .cnf souboru v závislosti na $n$, tj. délce řetězce. c/ Najděte největší $n_{max}$, pro které požadovaný řetězec existuje (pomocí části b/ a SAT solveru z a/). d/ Pošlete mi e-mailem v ZIPu nalezené $n_{max}$, počty proměnných a klauzulí ve vygenerovaných .cnf souborech pro $k, 4\le k \le n_{max+1}$ a zdrojáky použité pro generování .cnf souborů. (update:) A vygenerovane .cnf soubory pro $n_{max}$ a $n_{max+1}$.

DU4/CV3 (17.10.) Tablo: PG2018/4.4c

DU5/CV5 (31.10., do 7.11.) Rezoluce: PG2019/5.6 a totéž níže.
A taky DU3 je do 6.11. (středa)

DU6/CV6 (7.11.) PG2018/6.9 Dokažte nebo vyvraťte (sémanticky z definic): ...

- Pokud posíláte fotku nebo sken řešení e-mailem, napište i na papír své jméno. -

Cvičení 1.

  1. Sestrojte pravdivostní tabulky pro následující formule:
    • a) $((p \to q ) \to p) \to p$ *CV1*
    • 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)$
  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$
  4. Sestrojte formule 2. řádu (v jazyce teorie grafů) vyjadřující
    • a) existuje bipartitní rozklad
    • 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) ...
  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í *DU1*
    • 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é
    • Poznámky:
    • i) Předbíháme, bude ještě na ADS. 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, (~neexistuje menší)
    • b) $x$ je nejmenší prvek,
    • 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. 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í, s neutrálním prvkem.

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. *CV1*
    • 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í? *CV1*
    • (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,DU3) 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). Obecně exponenciální převod, ale jde lineárně při přidání proměnných.
    • "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 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 skontrolovatelný), nemá heuristické (až nekorektní) optimalizace a nepotřebuje tolik paměti.
    • Rozšíření SAT na SMT, Satisfiability Modulo Theories, například pomocí DPLL(T).

Cvičení 3

  1. Explicitní výsledky
    • 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)$.
  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: ...)