Skip to content
master
Switch branches/tags
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

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/lpi21-‹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 Atomické formuly a štruktúry SAT solver
2 Výrokovologické spojky Výrokovologické spojky Sudoku
3 Výrokovologické vyplývanie Výrokovologické vyplývanie Formula
4 Vlastnosti a vzťahy formúl Vlastnosti a vzťahy formúl NNF a CNF
5 Dôkazy a výrokovologické tablá Výrokovologické tablá Tableau
6 Korektnosť a úplnosť výrokovologických tabiel Splniteľnosť a falzifikovateľnosť v tablách TableauBuilder
7 Korektné tablové pravidlá. Algoritmus DPLL Korektné tablové pravidlá. Tvrdenia o tablách bonus: Hamiltonovská kružnica
8 watched literals
9 Kvantifikátory Kvantifikátory SatSolver
10 Tablá pre kvantifikátory Tablá pre kvantifikátory. Viackvantifikátorové tvrdenia Agatha
11 Funkčné symboly. Tablá s rovnosťou Funkčné symboly. Tablá s rovnosťou FolFormula
12 Definície. Korektnosť prvorádových tabiel Definície a dôkazy s nimi Vlk, koza, kapusta
12 Rezolvencia Rezolvencia Rezolver
bonus: Rodinka

Pravidlá pre úlohy.