11.-13. listopadu 2022 bylo podzimní soustředění FIKS v Praze. Následují osnovy a dodatečné materiály k mým přednáškám.

Kreslení vektorové grafiky

Ukázali jsme si jak kreslit vektorovou grafiku pomocí IPE a TikZu.

Řešení těžkých problémů

Kód používaný pro demonstraci na přednášce stáhnete zde: fiks_sat.zip. MiniSat lze stáhnout online dle vašeho OS.

  • Které problémy umíme řešít rychle, a co ‘rychle’ znamená?
    • Rychlé uvažujeme polynomiální
    • Co je to P a NP
      • turingův stroj
      • pouze pro rozhodovací problémy (odpověď je Ano/Ne)
      • řešitelné v polynomiálním čase = P
      • nedeterministicky řešitelné v polynomiálním čase = NP
  • Logika
    • Proměnné, Literály, Klauzule, Logické spojky, Formule
    • Úprava logické formule
    • Úloha SAT – rozhodovací, jak je těžká?
    • Převod do CNF
  • Řešení SAT
    • vyvození trivialit
    • jak vyresit 2-SAT
    • rozhodovací strom – full search
    • index, sledování dvou proměnných z klauzule – obrovské ušetření času algoritmu
    • CDCL – chceme se naučit něco z minulosti
      • Graf závislostí
      • unique implication point