Properties of SLUR Formulae

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F12%3A10126236" target="_blank" >RIV/00216208:11320/12:10126236 - isvavai.cz</a>

Výsledek na webu

<a href="http://link.springer.com/chapter/10.1007%2F978-3-642-27660-6_15" target="_blank" >http://link.springer.com/chapter/10.1007%2F978-3-642-27660-6_15</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-642-27660-6_15" target="_blank" >10.1007/978-3-642-27660-6_15</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Properties of SLUR Formulae

Popis výsledku v původním jazyce

Single look-ahead unit resolution (SLUR) algorithm is a non-deterministic polynomial time algorithm which for a given input formula in a conjunctive normal form (CNF) either outputs its satisfying assignment or gives up. A CNF formula belongs to the SLURclass if no sequence of nondeterministic choices causes the SLUR algorithm to give up on it. The SLUR class is reasonably large. It is known to properly contain the well studied classes of Horn CNFs, renamable Horn CNFs, extended Horn CNFs, and CC-balanced CNFs. In this paper we show that the SLUR class is considerably larger than the above mentioned classes of CNFs by proving that every Boolean function has at least one CNF representation which belongs to the SLUR class. On the other hand, we show, that given a CNF it is coNP-complete to decide whether it belongs to the SLUR class or not. Finally, we define a non-collapsing hierarchy of CNF classes SLUR(i) in such a way that for every fixed i there is a polynomial time satisfiability

Název v anglickém jazyce

Properties of SLUR Formulae

Popis výsledku anglicky

Single look-ahead unit resolution (SLUR) algorithm is a non-deterministic polynomial time algorithm which for a given input formula in a conjunctive normal form (CNF) either outputs its satisfying assignment or gives up. A CNF formula belongs to the SLURclass if no sequence of nondeterministic choices causes the SLUR algorithm to give up on it. The SLUR class is reasonably large. It is known to properly contain the well studied classes of Horn CNFs, renamable Horn CNFs, extended Horn CNFs, and CC-balanced CNFs. In this paper we show that the SLUR class is considerably larger than the above mentioned classes of CNFs by proving that every Boolean function has at least one CNF representation which belongs to the SLUR class. On the other hand, we show, that given a CNF it is coNP-complete to decide whether it belongs to the SLUR class or not. Finally, we define a non-collapsing hierarchy of CNF classes SLUR(i) in such a way that for every fixed i there is a polynomial time satisfiability

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GAP202%2F10%2F1188" target="_blank" >GAP202/10/1188: KnowSched: Znalostní techniky v rozvrhování</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2012

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ů

Název periodika

Lecture Notes in Computer Science

ISSN

0302-9743

e-ISSN

—

Svazek periodika

2012

Číslo periodika v rámci svazku

7147

Stát vydavatele periodika

DE - Spolková republika Německo

Počet stran výsledku

13

Strana od-do

177-189

Kód UT WoS článku

000307258500015

EID výsledku v databázi Scopus

—