Original title:
Důkazová složitost CSP
Translated title:
Proof Complexity of CSP
Authors:
Gaysin, Azza ; Krajíček, Jan (advisor) ; Kolokolova, Antonina (referee) ; Kompatscher, Michael (referee) Document type: Doctoral theses
Year:
2024
Language:
eng Abstract:
[eng][cze] In this thesis we formalize Zhuk's decision algorithm solving in p-time tractable con- straint satisfaction problems (CSPs) in a weak theory of bounded arithmetic W1 1 . As a consequence, we show that tautologies that express the negative instances of such CSPs have polynomial proofs in the quantified propositional calculus G. 1V této práce formalizujeme Zhukův polynomiální algoritmus rozhodující řešitelnost problémů splňování podmínek (CSPs), které nejsou NP-úplné, ve slabé teorii omezené aritmetiky W1 1 . Jako důsledek odvodíme, že tautologie odpovídající negativním instancím oněch CSP mají polynomiální důkazy v kvantifikovaném výrokovém počtu G. 1
Keywords:
bounded arithmetic|constraint satisfaction problem|proof complexity|universal algebra; omezená aritmetika|problém splňování podmínek|důkazová složitost|univerzální algebra
Institution: Charles University Faculties (theses)
(web)
Document availability information: Available in the Charles University Digital Repository. Original record: http://hdl.handle.net/20.500.11956/188623