Název: Důkazová složitost CSP
Překlad názvu: Proof Complexity of CSP
Autoři: Gaysin, Azza ; Krajíček, Jan (vedoucí práce) ; Kolokolova, Antonina (oponent) ; Kompatscher, Michael (oponent)
Typ dokumentu: Disertační práce
Rok: 2024
Jazyk: eng
Abstrakt: [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. 1 V 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
Klíčová slova: omezená aritmetika|problém splňování podmínek|důkazová složitost|univerzální algebra; bounded arithmetic|constraint satisfaction problem|proof complexity|universal algebra

Instituce: Fakulty UK (VŠKP) (web)
Informace o dostupnosti dokumentu: Dostupné v digitálním repozitáři UK.
Původní záznam: http://hdl.handle.net/20.500.11956/188623

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-542135


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Univerzita Karlova > Fakulty UK (VŠKP)
Vysokoškolské kvalifikační práce > Disertační práce