README.md

Logika pre informatikov

Stránka predmetu.

Inštrukcie na odovzdávanie riešení praktických úloh.

Priebežné hodnotenie

Prehľad o vašom priebežnom bodovom hodnotení nájdete v súbore report.md vo vetve report vo vašich repozitároch. Priame URL je (nezabudnite nahradiť ‹LOGIN› za svoje prihlasovacie meno):

https://github.com/FMFI-UK-1-AIN-412/lpi22-‹LOGIN›/blob/report/report.md

Ak si toto pozeráte vo svojom repozitári, funguje nasledujúci odkaz: report.md.

Súťaž o najrýchlejší SAT solver

Zapojte sa do súťaže o najrýchlejší SAT solver. Autori najrýchlejších solverov môžu získať až 5 bonusových bodov.

Úlohy a prezentácie z prednášok

Týždeň	Prezentácie z prednášok	Teoretické úlohy	Praktické úlohy
1	Úvod. Atomické formuly a štruktúry	tu01 (AIN)	SAT solver
2	Výrokovologické spojky	tu02 (AIN)	Sudoku
3	Výrokovologické vyplývanie	tu03 (AIN)	Formula
4	Vlastnosti a vzťahy formúl	tu04 (AIN)	NNF a CNF
5	Dôkazy a výrokovologické tablá	tu05 (AIN)	Tableau
6	Korektnosť a úplnosť výrokovologických tabiel	tu06 (AIN)	TableauBuilder
7	1. Korektné tablové pravidlá. Algoritmus DPLL 2. CDCL, VSIDS a aplikácie SAT solverov	tu07 (AIN)	Hamiltonovská kružnica
8	Kvantifikátory	tu08 (AIN)	watched literals
9	Tablá pre kvantifikátory. Viackvantifikátorové tvrdenia	tu09 (AIN)	SAT solver
			bonus: Agatha
10	Funkčné symboly. Tablá s rovnosťou	tu10 (AIN)	FolFormula
11	Korektnosť prvorádových tabiel. Explicitné definície	tu11 (AIN)	Vlk, koza, kapusta
12	Rezolvencia	tu12 (AIN)	Rezolver

Zbierka teoretických úloh (AIN).

Poznámky z prednášok – všetky prezentácie ako knižka.

Pravidlá pre úlohy.