Phase Transition in Matched Formulas and a Heuristic for Biclique Satisfiability
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F19%3A10402519" target="_blank" >RIV/00216208:11320/19:10402519 - isvavai.cz</a>
Výsledek na webu
<a href="https://doi.org/10.1007/978-3-030-10801-4_10" target="_blank" >https://doi.org/10.1007/978-3-030-10801-4_10</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-030-10801-4_10" target="_blank" >10.1007/978-3-030-10801-4_10</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Phase Transition in Matched Formulas and a Heuristic for Biclique Satisfiability
Popis výsledku v původním jazyce
A matched formula is a CNF formula whose incidence graph admits a matching which matches a distinct variable to every clause. We study phase transition in a context of matched formulas and their generalization of biclique satisfiable formulas. We have performed experiments to find a phase transition of property "being matched" with respect to the ratio m/n where m is the number of clauses and n is the number of variables of the input formula ϕ. We compare the results of experiments to a theoretical lower bound which was shown by Franco and Van Gelder [11]. Any matched formula is satisfiable, and it remains satisfiable even if we change polarities of any literal occurrences. Szeider [17] generalized matched formulas into two classes having the same property-varsatisfiable and biclique satisfiable formulas. A formula is biclique satisfiable if its incidence graph admits covering by pairwise disjoint bounded bicliques. Recognizing if a formula is biclique satisfiable is NP-complete. In this paper we describe a heuristic algorithm for recognizing whether a formula is biclique satisfiable and we evaluate it by experiments on random formulas. We also describe an encoding of the problem of checking whether a formula is biclique satisfiable into SAT and we use it to evaluate the performance of our heuristic.
Název v anglickém jazyce
Phase Transition in Matched Formulas and a Heuristic for Biclique Satisfiability
Popis výsledku anglicky
A matched formula is a CNF formula whose incidence graph admits a matching which matches a distinct variable to every clause. We study phase transition in a context of matched formulas and their generalization of biclique satisfiable formulas. We have performed experiments to find a phase transition of property "being matched" with respect to the ratio m/n where m is the number of clauses and n is the number of variables of the input formula ϕ. We compare the results of experiments to a theoretical lower bound which was shown by Franco and Van Gelder [11]. Any matched formula is satisfiable, and it remains satisfiable even if we change polarities of any literal occurrences. Szeider [17] generalized matched formulas into two classes having the same property-varsatisfiable and biclique satisfiable formulas. A formula is biclique satisfiable if its incidence graph admits covering by pairwise disjoint bounded bicliques. Recognizing if a formula is biclique satisfiable is NP-complete. In this paper we describe a heuristic algorithm for recognizing whether a formula is biclique satisfiable and we evaluate it by experiments on random formulas. We also describe an encoding of the problem of checking whether a formula is biclique satisfiable into SAT and we use it to evaluate the performance of our heuristic.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
—
OECD FORD obor
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Návaznosti výsledku
Projekt
—
Návaznosti
S - Specificky vyzkum na vysokych skolach<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Ostatní
Rok uplatnění
2019
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
SOFSEM 2019: Theory and Practice of Computer Science
ISBN
978-3-030-10800-7
ISSN
0302-9743
e-ISSN
—
Počet stran výsledku
14
Strana od-do
108-121
Název nakladatele
Springer Switzerland
Místo vydání
Cham, Switzerland
Místo konání akce
Nový Smokovec, Slovakia
Datum konání akce
27. 1. 2019
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—