|
|
NP vyhledávací problémy
Jirotka, Tomáš ; Krajíček, Jan (vedoucí práce) ; Pudlák, Pavel (oponent)
Název práce: NP vyhledávací problémy Autor: Tomáš Jirotka Katedra: Katedra algebry Vedoucí diplomové práce: Prof. RNDr. Jan Krajíček, DrSc. Abstrakt: Práce shrnuje dosavadní výsledky v oblasti NP vyhledávacích problémů. Podrobně diskutujeme otázku složitosti faktorizace celých čísel a před- kládáme výsledky, které zařazují tento problém do již známých složitostních tříd a v jistém smyslu se jej snaží separovat z PLS. Dále definujeme několik nových vyhledávacích problémů. Klíčová slova: Výpočetní složitost, TFNP, faktorizace čísel.
|
|
|
Těžké tautologie
Pich, Ján ; Krajíček, Jan (vedoucí práce) ; Pudlák, Pavel (oponent)
Skoumáme nedokazatelnost tvrzení NP$\not\subseteq$P/poly v různých fragmentech aritmetiky. Ta se obvykle dosahuje ukázáním těžkosti výrokových formulí kódujících superpolynomiální spodní odhady pro booleovské obvody. Nejprve prezentujeme několik známých technik a tvrzení. Přirozené důkazy, efektívní interpolaci, KPT větu, iterovatelnost, gadget generátory atd. Pak dokážem několik původních výsledků. Ukážeme nedokazatelnost superpolynomiálních spodních odhadů na booleovské obvody v systémech s efektívní interpolaci (modulo složitostní předpoklad) a v systémech podobajících se stromovým Frege systémům manipulujícím s formulemi, které obsahují jen málo proměnných dokazovaného tvrzení. Tyto výsledky jsou založeny na dokazování těžkosti Nisan-Wigdersonových generátorů v príslušných důkazových systémech.
|
|
|
Vyhledávací problémy a hledání kolizí pro hašovací funkce
Čarnoký, Samuel ; Krajíček, Jan (vedoucí práce) ; Pudlák, Pavel (oponent)
Název práce: Vyhledávací problémy a hledání kolizí pro hašovací funkce Autor: Samuel Čarnoký Katedra : Katedra algebry Vedoucí diplomové práce: prof. RNDr. Jan Krajíček, DrSc. e-mail vedoucího: krajicek@karlin.mff.cuni.cz Abstrakt: Centrálnymi bodmi tejto práce sú NP vyhľadávacie problémy a existencia redukcie medzi nimi v relativizovanom zmysle. Absolútna separácia by separovala P od NP. Venujeme sa špeciálne problému hľadania kolízii v hešovacích funkciách, ktorých existencia je garantovaná známym holubníkovým princípom (PHP). Podávame stručný úvod do problematiky, definujeme rôzne NP vyhľadávacie problémy a pripomíname redukcie a separácie. Referujeme o redukcii slabej verzie PHP na hľadanie homogénneho podgrafu a prinášame vlastnú redukciu varianty PHP na problematiku súvisiacu s hľadaním ciest v grafe. Pojednávame o redukovaní hladania kolízií vo viacerých funkciach na hľadanie kolízie v jednej. Klíčová slova: NP vyhľadávanie, redukcie, pigeonhole principle, orákula
|
|
|
Výroková logika a algebra
Polach, František ; Krajíček, Jan (vedoucí práce) ; Pudlák, Pavel (oponent)
Algebraic proof systems of which the most important are the polynomial calculus and the Nullstellensatz proof system are proof systems that use algebraic means for proving propositional tautologies - they are based on polynomial identities over (commutative) rings. Razborov [9] have proved a non-trivial lower bound on degree for polynomia calculus proofs of the tautologies (a set of polynomials) that express the pigeonhole principle over any field. This work gathers present important results for algebraic proof systems and generalizes the Razborov's construction used in his proof of the lower bound to another set of polynomials. We explicitly describe the basis of the vector space of polynomials that are derivable by a small degree polynomial calculus proof from the tautologies that express a variant of the pigeonhole principle (that generalizes the principle for multifunctions).
|
|
| |
|
|
Interpolation in modal logics
Bílková, Marta ; Pudlák, Pavel (vedoucí práce) ; Švejdar, Vítězslav (oponent) ; Iemhoff, Rosalie (oponent)
Since Craig's landmark result on interpolation for classical predicate logic, proved as the main technical lemma in [14], interpolation is considered one of the centra! concepts in pure logic. Various interpolation properties find their applications in computer science and have many deep purely logical consequences. We focus on two propositional versions of Craig interpolation property: Craig Interpolation Property: for every provable implication (A -+ B) there is an interpolant I containing only only common variables of A and B such that both implications (A -+ I) and (I-+ B) are provable. Craig interpolation, although it seems rather technical, is a deep logical property. It is dosely related to expressive power of a logic - as such it entails Beth's definability property, or forces functional completeness. It is also related to Robinson's joint consistency of two theories that agree on the common language. Craig interpolation has an important algebraic counterpart - it entails amalgamation or superamalgamation property of appropriate algebraic structures. In case of modal provability logics, Craig interpolation entails fixed point theorem. There are other interpolation properties, defined w.r.t. a consequence relation rather then w.r.t. a provable implication. In presence of deduction theorem the two...
|
|
|
Silné důkazové systémy
Mikle-Barát, Ondrej ; Krajíček, Jan (vedoucí práce) ; Pudlák, Pavel (oponent)
R-OBDD je nový Cook-Reckhowův důkazový systém pro výrokovou logiku založen na kombinaci OBDD důkazového systému a rezolučního důkazového systému. R-OBDD má sílu OBDD důkazového systému - tautologie s exponenciálně velkými důkazy v rezoluci jako PHPn nebo Tseitinovy kontradikce mají v R-OBDD systému polynomiální důkazy (R-OBDD p-simuluje jak OBDD důkazový systém, tak rezoluci). Na druhé straně, odvozovací pravidla R-OBDD systému byly navrhnuty, aby se podobaly odvozovacím pravidlům rezoluce. Tím pádem je možné vytvořit modifikaci DPLL algoritmu, která bude pracovat v R-OBDD systému a zároveň použít některé heuristiky známé z algoritmů založených na DPLL. Vzniká možnost vytvořit efektivnejší algoritmus na řešení problému splnitelnosti formule (SAT). Ukážeme návrh algoritmu, který je adaptací DPLL algoritmu pro R-OBDD důkazový systém. Přikldáme důkaz z jeho korektnosti a ukážeme, že jeho běh nad nesplnitelnou formulí je možné transformovat do stromového důkazu v R-OBDD systému.
|
|
| |
|
| |
|
| |
host ::
RSS.