|
|
Upper bounds for (k,s)-SAT
Jurenka, David ; Szeider, Stefan (vedoucí práce) ; Dantchev, Stefan (oponent)
Při studiu problému (k, s)-SAT narážíme na funkci f : N → N vyme- zující hranici mezi triviálními a NP-těžkými variantami tohoto problému. Nicméně přesné hodnoty f (k) pro k > 4 nejsou známy. Tato práce se zabývá funkcí f, hledáním jejích horních odhadů pro ma- lé hodnoty k a generováním minimálních formulí (k, s)-CNF dokládajících tyto odhady. Horní odhady jsou získány implementací heuristiky nedáv- no popsané v časopisecké literatuře. Výpočet je následně paralelizován pro využití potenciálu počítačových clusterů pro HPC. Dále je dokázáno několik teoretických výsledků. Vyvrátíme jeden ne- dávný dolní odhad pro f, zavedeme dolní odhad velikosti vynucujících for- mulí pro (k, s)-SAT a zlepšíme stávající faktor neaproximovatelnosti pro- blému MAX-(3, 4)-SAT.
|
|
|
Nerozhodnutelnost struktury racionálních čísel
Jurenka, David ; Švejdar, Vítězslav (vedoucí práce) ; Krajíček, Jan (oponent)
Otázka rozhodnutelnosti, tj. otázka, zda existuje algoritmus, který by byl schopen rozhodnout o platnosti každé prvořádové predikátové formule, se dostala na výsluní pozornosti matematiků ve dvacátých letech minulého století. Spolu s ní byla zkoumána i rozhodnutelnost druhořádových formulí a obecně jakéhokoli matematického tvrzení. Souhrnně byly tyto otázky označovány jako Hilbertův Entscheidungsproblem a ještě roku 1930 Hilbert věřil v jejich kladné řešení. Roku 1936 však Alonzo Church ukázal, že samotná predikátová logika prvního řádu je nerozhodnutelná, a téhož roku pak Alan Turing představil dnes již klasický nerozhodnutelný problém, problém zastavení. Oba při tom ve svých pracech využili myšlenek, které formuloval Kurt Godel ve svém důkazu neúplnosti aritmetiky. V otázce rozhodnutelnosti základních aritmetických struktur přinesl první významný výsledek Mojzesz Presburger, který roku 1929 dokázal rozhodnutelnost přirozených čísel s operací sčítání a konstantami O a 1. Nicméně hned následujícího roku vyplynulo z Godelových výsledků, že tatáž struktura včetně operace násobení již rozhodnutelná být nemůže. Tím byla zároveň vyřešena i otázka rozhodnutelnosti čísel celých, neboť pojem přirozeného čísla je v této struktuře definovatelný (viz kapitolu 4.2), a tak je možno v celých číslech reformulovat každou...
|
|
|
Upper bounds for (k,s)-SAT
Jurenka, David ; Szeider, Stefan (vedoucí práce) ; Dantchev, Stefan (oponent)
Při studiu problému (k, s)-SAT narážíme na funkci f : N → N vyme- zující hranici mezi triviálními a NP-těžkými variantami tohoto problému. Nicméně přesné hodnoty f (k) pro k > 4 nejsou známy. Tato práce se zabývá funkcí f, hledáním jejích horních odhadů pro ma- lé hodnoty k a generováním minimálních formulí (k, s)-CNF dokládajících tyto odhady. Horní odhady jsou získány implementací heuristiky nedáv- no popsané v časopisecké literatuře. Výpočet je následně paralelizován pro využití potenciálu počítačových clusterů pro HPC. Dále je dokázáno několik teoretických výsledků. Vyvrátíme jeden ne- dávný dolní odhad pro f, zavedeme dolní odhad velikosti vynucujících for- mulí pro (k, s)-SAT a zlepšíme stávající faktor neaproximovatelnosti pro- blému MAX-(3, 4)-SAT.
|
|
|
Nerozhodnutelnost struktury racionálních čísel
Jurenka, David ; Krajíček, Jan (oponent) ; Švejdar, Vítězslav (vedoucí práce)
Otázka rozhodnutelnosti, tj. otázka, zda existuje algoritmus, který by byl schopen rozhodnout o platnosti každé prvořádové predikátové formule, se dostala na výsluní pozornosti matematiků ve dvacátých letech minulého století. Spolu s ní byla zkoumána i rozhodnutelnost druhořádových formulí a obecně jakéhokoli matematického tvrzení. Souhrnně byly tyto otázky označovány jako Hilbertův Entscheidungsproblem a ještě roku 1930 Hilbert věřil v jejich kladné řešení. Roku 1936 však Alonzo Church ukázal, že samotná predikátová logika prvního řádu je nerozhodnutelná, a téhož roku pak Alan Turing představil dnes již klasický nerozhodnutelný problém, problém zastavení. Oba při tom ve svých pracech využili myšlenek, které formuloval Kurt Godel ve svém důkazu neúplnosti aritmetiky. V otázce rozhodnutelnosti základních aritmetických struktur přinesl první významný výsledek Mojzesz Presburger, který roku 1929 dokázal rozhodnutelnost přirozených čísel s operací sčítání a konstantami O a 1. Nicméně hned následujícího roku vyplynulo z Godelových výsledků, že tatáž struktura včetně operace násobení již rozhodnutelná být nemůže. Tím byla zároveň vyřešena i otázka rozhodnutelnosti čísel celých, neboť pojem přirozeného čísla je v této struktuře definovatelný (viz kapitolu 4.2), a tak je možno v celých číslech reformulovat každou...
|
|
|
Nerozhodnutelnost struktury racionálních čísel
Jurenka, David ; Švejdar, Vítězslav (vedoucí práce) ; Krajíček, Jan (oponent)
Otázka rozhodnutelnosti, tj. otázka, zda existuje algoritmus, který by byl schopen rozhodnout o platnosti každé prvořádové predikátové formule, se dostala na výsluní pozornosti matematiků ve dvacátých letech minulého století. Spolu s ní byla zkoumána i rozhodnutelnost druhořádových formulí a obecně jakéhokoli matematického tvrzení. Souhrnně byly tyto otázky označovány jako Hilbertův Entscheidungsproblem a ještě roku 1930 Hilbert věřil v jejich kladné řešení. Roku 1936 však Alonzo Church ukázal, že samotná predikátová logika prvního řádu je nerozhodnutelná, a téhož roku pak Alan Turing představil dnes již klasický nerozhodnutelný problém, problém zastavení. Oba při tom ve svých pracech využili myšlenek, které formuloval Kurt Godel ve svém důkazu neúplnosti aritmetiky. V otázce rozhodnutelnosti základních aritmetických struktur přinesl první významný výsledek Mojzesz Presburger, který roku 1929 dokázal rozhodnutelnost přirozených čísel s operací sčítání a konstantami O a 1. Nicméně hned následujícího roku vyplynulo z Godelových výsledků, že tatáž struktura včetně operace násobení již rozhodnutelná být nemůže. Tím byla zároveň vyřešena i otázka rozhodnutelnosti čísel celých, neboť pojem přirozeného čísla je v této struktuře definovatelný (viz kapitolu 4.2), a tak je možno v celých číslech reformulovat každou...
|
host ::
RSS.