|
|
Vlastnosti intervalových booleovských funkcí
Hušek, Radek ; Čepek, Ondřej (vedoucí práce)
Tato práce řeší problém rozpoznávání k-intervalových boolovských funkcí. Na vstup bo- olovské funkce můžeme nahlížet jako na binární zápis přirozeného čísla. Funkce je k- intervalová, pokud - při takto interpretovaném vstupu - nabývá hodnoty jedna právě pro vstupy z daných nejvýše k intervalů. Tento problém je pro obecné boolovské funkce zadané DNF coNP-těžký. Proto se zabýváme případem, kdy DNF náleží do dané řešitelné třídy (třída je řešitelná, pokud pro DNF z ní umíme řešit falsifikovatelnost v polynomiál- ním čase a je uzavřená na částečná dosazení), a ukazujeme, že v tomto případě je úloha pro pevné k řešitelná v polynomiálním čase. 1
|
|
|
Graph communication protocols
Folwarczný, Lukáš ; Pudlák, Pavel (vedoucí práce) ; Sgall, Jiří (oponent)
Grafové komunikační protokoly jsou zobecněním klasických komunikačních protokolů na případ, kdy je grafem protokolu orientovaný acyklický graf. Motivováni možnými aplikacemi v důkazové složitosti studujeme varianty grafových komunikačních protokolů a vztahy mezi nimi. Hlavním výsledkem je porovnání síly dvou typů protokolů, protokolů s rovností a protokolů s konjunkcí konstantního počtu nerovností. Dokazujeme, že protokoly prvního typu jsou alespoň tak silné jako protokoly druhého typu v následujícím smyslu: Necht' f je booleovská funkce. Pokud existuje protokol s konjunkcí konstantního počtu nerovností polynomiální velikosti řešící f, pak existuje protokol s rovností polynomiální velikosti řešící f. Rovněž zavádíme dva nové typy grafových komunikačních protokolů, protokoly s disjunktností a protokoly s nedisjunktností, a dokazujeme, že protokoly prvního typu jsou alespoň tak silné jako doposud uvažované protokoly a že protokoly druhého typu jsou příliš silné na to, aby mohly být aplikovány.
|
|
|
Boolean methods in knowledge compilation
Kaleyski, Nikolay Stoyanov ; Čepek, Ondřej (vedoucí práce) ; Gregor, Petr (oponent)
V rámci práce je vyřešen otevřený problém o relativní úspornosti jazyků PI a MODS. Ukazuje se, že PI není alespoň tak úsporný jako MODS tím, že se konstruuje třída Booleovských funkcí s počtem primárních implikantů který je superpolynomiální vzhledem k počtu nulových bodů zkonstruovaných funkcí. Odvozuje se dolní mez (čím se dokazuje, že PI není alespoň tak úsporný jako MODS), horní mez (která ukazuje, že zkonstruovaný protipříklad nemůže poskytnout exponenciální separaci PI a MODS) a vzorec pro přesný počet primárních implikantů zkonstruovaných funkcí. Powered by TCPDF (www.tcpdf.org)
|
|
|
Vlastnosti intervalových booleovských funkcí
Hušek, Radek ; Čepek, Ondřej (vedoucí práce) ; Kučera, Petr (oponent)
Tato práce řeší problém rozpoznávání k-intervalových boolovských funkcí. Na vstup bo- olovské funkce můžeme nahlížet jako na binární zápis přirozeného čísla. Funkce je k- intervalová, pokud - při takto interpretovaném vstupu - nabývá hodnoty jedna právě pro vstupy z daných nejvýše k intervalů. Tento problém je pro obecné boolovské funkce zadané DNF coNP-těžký. Proto se zabýváme případem, kdy DNF náleží do dané řešitelné třídy (třída je řešitelná, pokud pro DNF z ní umíme řešit falsifikovatelnost v polynomiál- ním čase a je uzavřená na částečná dosazení), a ukazujeme, že v tomto případě je úloha pro pevné k řešitelná v polynomiálním čase. 1
|
|
|
Special Classes of Boolean Functions with Respect to the Complexity of their Minimization.
Gurský, Štefan ; Čepek, Ondřej (vedoucí práce) ; Marquis, Pierre (oponent) ; Janota, Mikoláš (oponent)
V práci zkoumáme boolovské funkce ze tří různých hledisek. Zaprvé zkoumáme zložitost minimalizace formulí z několika tříd s polynomiálně řešitelným SATem a uvádíme postačující podmínky pro třídy CNF aby se jejich minimalizace přesunula níž alespoň o jeden stupeň v polynomiální hierarchii. Zadruhé zk- oumáme třídu formulí zvaných matched (párované) pro které je SAT triviální, ale minimalizace zůstává Σp 2 úplná. Dokazujeme, že pro každou párovanou CNF existuje alespoň jedna primární a iredundantní CNF s ní ekvivalentní, která je také párovaná. Použitím tohoto tvrzení ukazujeme hlavní výsledek této části a to, že pro každou párovanou CNF všechny s ní ekvivalentní CNF mající minimální možný počet klauzulí jsou taky párované. Zatřetí se věnujeme vlastnosti propagation completeness (úplnosti pro propagaci) - CNF je úplná pro propagaci, pokud pro každé částečné dosazení jsou všechny vynucené literály odvoditelné jednotkovou propagací. Každá CNF sa dá rozšířit na úplnou pro propagaci přidáváním empowering (zesilujících) imp- likátů. Hlavním výsledkem této části je důkaz coNP úplnosti rozpoznávání formulí úplných pro propagaci. Dále ukazujeme, že existují formule, ke kterým je nutno přidat exponenciálně mnoho zesilujících implikátů, aby se staly úplnými pro propagaci.
|
|
|
Knihovna pro binární rozhodovací diagramy
Janků, Petr ; Hrubý, Martin (oponent) ; Holík, Lukáš (vedoucí práce)
Efektivní manipulace Booleovských funkcí je důležitou součástí mnoha počítačových návrhů. Jako datová struktura pro reprezentaci a manipulaci s Booleovskými funkcemi se běžně používají binární rozhodovací diagramy. Tyto diagramy se běžně používají v mnoha odvětvích, jako je například ověřování modelů, verifikace systému, návrh obvodů apod. V této práci jsou popsány tyto diagramy a jsou zde uvedeny i jejich modifikace. Dále jsou v této práci uvedeny a popsány techniky pro efektivní manipulaci a reprezentaci binárních rozhodovacích diagramů. Mimoto tato práce popisuje návrh a implementaci knihovny, která bude s těmito diagramy pracovat. Dále je diskutována potenciální aplikace vyvinuté knihovny v knihovně VATA pro manipulaci se stromovými automaty. Na závěr je tato knihovna porovnána s dobře známou a silně optimalizovanou knihovnou CUDD, která je volně dostupná a s knihovnou CacBDD. Výsledky experimentů ukázaly, že navrhovaná knihovna je poměrně blízká CUDD a CacBDD (dosahuje srovnatelného a většinou i lehce lepšího výkonu).
|
host ::
RSS.