Thesis (Selection of subject)Thesis (Selection of subject)(version: 285)
Assignment details
   Login via CAS
Formal proofs of the correctness of SAT algorithms
Thesis title in Czech: Formální důkazy korektnosti SAT algoritmů
Thesis title in English: Formal proofs of the correctness of SAT algorithms
Key words: formální důkazy, SAT algoritmy
English key words: formal proofs, SAT algorithms
Academic year of topic announcement: 2018/2019
Type of assignment: diploma thesis
Thesis language: angličtina
Department: Department of Algebra (32-KA)
Supervisor: prof. RNDr. Jan Krajíček, DrSc.
Author:
Guidelines
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.

References
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á.
Preliminary scope of work
Dokazatelnost korektnosti SAT algoritmů a jejich časová složitost.
Preliminary scope of work in English
Provability of the correctness of SAT algorithms and their time complexity.
 
Charles University | Information system of Charles University | http://www.cuni.cz/UKEN-329.html