This HTML5 document contains 47 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
n13http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216208%3A11320%2F12%3A10126236%21RIV13-GA0-11320___/
dctermshttp://purl.org/dc/terms/
n5http://localhost/temp/predkladatel/
n10http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n6http://linked.opendata.cz/resource/domain/vavai/projekt/
n16http://linked.opendata.cz/resource/domain/vavai/subjekt/
n15http://linked.opendata.cz/ontology/domain/vavai/
shttp://schema.org/
skoshttp://www.w3.org/2004/02/skos/core#
rdfshttp://www.w3.org/2000/01/rdf-schema#
n3http://linked.opendata.cz/ontology/domain/vavai/riv/
n17http://bibframe.org/vocab/
n2http://linked.opendata.cz/resource/domain/vavai/vysledek/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n14http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n19http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n11http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n4http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n21http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n20http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n7http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216208%3A11320%2F12%3A10126236%21RIV13-GA0-11320___
rdf:type
skos:Concept n15:Vysledek
rdfs:seeAlso
http://link.springer.com/chapter/10.1007%2F978-3-642-27660-6_15
dcterms:description
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 SLUR class 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 algorithm for the class SLUR(i), and that every CNF on n variables belongs to SLUR(i) for some i {= n. 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 SLUR class 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 algorithm for the class SLUR(i), and that every CNF on n variables belongs to SLUR(i) for some i {= n.
dcterms:title
Properties of SLUR Formulae Properties of SLUR Formulae
skos:prefLabel
Properties of SLUR Formulae Properties of SLUR Formulae
skos:notation
RIV/00216208:11320/12:10126236!RIV13-GA0-11320___
n15:predkladatel
n16:orjk%3A11320
n3:aktivita
n4:S n4:P n4:I
n3:aktivity
I, P(GAP202/10/1188), S
n3:cisloPeriodika
7147
n3:dodaniDat
n7:2013
n3:domaciTvurceVysledku
n10:1561510 n10:9459413 n10:4048067
n3:druhVysledku
n20:J
n3:duvernostUdaju
n19:S
n3:entitaPredkladatele
n13:predkladatel
n3:idSjednocenehoVysledku
162907
n3:idVysledku
RIV/00216208:11320/12:10126236
n3:jazykVysledku
n11:eng
n3:klicovaSlova
unit resolution; CNF satisfiability; Boolean functions
n3:klicoveSlovo
n14:unit%20resolution n14:CNF%20satisfiability n14:Boolean%20functions
n3:kodStatuVydavatele
DE - Spolková republika Německo
n3:kontrolniKodProRIV
[9FD95D68974C]
n3:nazevZdroje
Lecture Notes in Computer Science
n3:obor
n21:IN
n3:pocetDomacichTvurcuVysledku
3
n3:pocetTvurcuVysledku
3
n3:projekt
n6:GAP202%2F10%2F1188
n3:rokUplatneniVysledku
n7:2012
n3:svazekPeriodika
2012
n3:tvurceVysledku
Čepek, Ondřej Vlček, Václav Kučera, Petr
n3:wos
000307258500015
s:issn
0302-9743
s:numberOfPages
13
n17:doi
10.1007/978-3-642-27660-6_15
n5:organizacniJednotka
11320