Název: Rozšíření matched formulí
Překlad názvu: Extensions to the class of matched formulae
Autoři: Chromý, Miloš ; Kučera, Petr (vedoucí práce) ; Babka, Martin (oponent)
Typ dokumentu: Diplomové práce
Rok: 2015
Jazyk: cze
Abstrakt: [cze] [eng]
S KNF formulí můžeme asociovat incidenční graf. Tento graf je bipartitní a jedna partita zastupuje proměnné a druhá klauzule. Díky tomu můžeme definovat nové třídy KNF formulí, jimiž jsou matched formule a biklikově splnitelné formule. Obě tyto třídy mají tu vlastnost, že formule, které do nich patří jsou splnitelné i po změně polarity libovolného literálu. Takovým formulím říkáme var-splnitelné. V této práci uvažujeme práci Stefana Szeidera, která popisuje parametrizo- vaný algoritmus s pevným parametrem řešící problém matched formulí s malou deficiencí, což je rozdíl počtu klauzulí a počtu proměnných. Ukázali jsme, proč tento přístup nejde přímo zobecnit pro biklikově splnitelné formule. Vzhledem k tomu, že testování toho, je-li formule biklikově splnitelná, je NP- úplné, popsali jsme heuristiku, která hledá biklikové pokrytí v čase O(n2 e), kde n je počet proměnných ve formuli a e je délka formule. Provedli jsme experimenty na náhodných formulích. Z výsledků těchto experimentů lze usuzovat, že existuje fázový přechod ve výsledcích heuristiky. Dále jsme provedli experimenty, které ověřují existenci fázového přechodu matched formulí. Tyto výsledky jsme porov- nali s výsledky experimentů provedených s heuristikou. Výsledky experimentu provedeném na matched formulí jsme též porovnali s teoretickou hranicí... We can associate an incidence graph with any CNF formula. It's a bipartite graph, in which he first part corresponds to variables and the second one to clauses. We can define matched formulas and biclique satisfiable formulas, based on this incidence graph. Both of these classes share an interesting property: Given a formula F which is matched or biclique satisfiable, F remains satisfiable even after we switch polarity of any occurrence of any literal. Class of formulas with this property is called var-satisfiable. In this thesis, we consider a parameterized algorithm introduced by Stefan Szeider for deciding satisfiability of formulas with small deficiency. Here deficiency of a formula is defined as a difference between the number of clauses and the number of variables in the formula. We explain why this algorithm cannot be simply generalized for the case of biclique satisfiable formulas. Since the problem of determining whether a formula is biclique satisfiable is NP-complete, we introduce a heuristic, which tries to find some biclique cover in time O(n2 e), where n denotes the number of variables and e denotes the length of the input formula. We performed experiments testing this heuristic on random formulas. The results of these experiments suggest, that there is a phase transition in the behaviour of the heuristic....
Klíčová slova: Matched formule; maximální deficience formule; splnitelnost; Matched formulae; maximum deficiency of a formula; satisfiability

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/81178

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


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 > Diplomové práce