Témata prací (Výběr práce)Témata prací (Výběr práce)(verze: 290)
Detail práce
   Přihlásit přes CAS
Formal proofs of the correctness of SAT algorithms
Název práce v češtině: Formální důkazy korektnosti SAT algoritmů
Název v anglickém jazyce: Formal proofs of the correctness of SAT algorithms
Klíčová slova: formální důkazy, SAT algoritmy
Klíčová slova anglicky: formal proofs, SAT algorithms
Akademický rok vypsání: 2018/2019
Typ práce: diplomová práce
Jazyk práce: angličtina
Ústav: Katedra algebry (32-KA)
Vedoucí / školitel: prof. RNDr. Jan Krajíček, DrSc.
Řešitel:
Zásady pro vypracování
By the correctness of a SAT algorithm is meant the statement
that it finds a satisfying assignment for all satisfiable formulas.
The statement can be formalized by a first-order formula Ref(M)
valid in all finite structures. The provability of Ref(M) using
some restricted means (e.g. using only induction for FO properties
of finite structures) automatically implies an exponential lower
bound on the time complexity of M. The aim of the Thesis will
be to formalize and to prove using restricted means Ref(M)
for some interesting M.

Seznam odborné literatury
J.Krajicek, A note on SAT algorithms and proof complexity,
Information Processing Letters, 112 (2012), pp. 490-493.
viz http://www.karlin.mff.cuni.cz/~krajicek/sat.pdf
a literatura tam zmíněná.
Předběžná náplň práce
Dokazatelnost korektnosti SAT algoritmů a jejich časová složitost.
Předběžná náplň práce v anglickém jazyce
Provability of the correctness of SAT algorithms and their time complexity.
 
Univerzita Karlova | Informační systém UK