About: Properties of SLUR Formulae

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Properties of SLUR Formulae Goto Sponge NotDistinct Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
rdfs:seeAlso	http://link.springer.com/chapter/10.1007%2F978-3-642-27660-6_15
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. (en)
Title	Properties of SLUR Formulae Properties of SLUR Formulae (en)
skos:prefLabel	Properties of SLUR Formulae Properties of SLUR Formulae (en)
skos:notation	RIV/00216208:11320/12:10126236!RIV13-GA0-11320___
http://linked.open...avai/predkladatel	Matematicko-fyzikální fakulta
http://linked.open...avai/riv/aktivita	I P S
http://linked.open...avai/riv/aktivity	I, P(GAP202/10/1188), S
http://linked.open...iv/cisloPeriodika	7147
http://linked.open...vai/riv/dodaniDat	2013
http://linked.open...aciTvurceVysledku	Kučera, Petr Čepek, Ondřej Vlček, Václav
http://linked.open.../riv/druhVysledku	J - Článek v odborném periodiku
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...titaPredkladatele	Univerzita Karlova v Praze / Matematicko-fyzikální fakulta
http://linked.open...dnocenehoVysledku	162907
http://linked.open...ai/riv/idVysledku	RIV/00216208:11320/12:10126236
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	unit resolution; CNF satisfiability; Boolean functions (en)
http://linked.open.../riv/klicoveSlovo	Boolean functions CNF satisfiability unit resolution
http://linked.open...odStatuVydavatele	DE - Spolková republika Německo
http://linked.open...ontrolniKodProRIV	[9FD95D68974C]
http://linked.open...i/riv/nazevZdroje	Lecture Notes in Computer Science
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	3 (xsd:int)
http://linked.open...cetTvurcuVysledku	3 (xsd:int)
http://linked.open...vavai/riv/projekt	KnowSched: Knowledge Techniques in Scheduling
http://linked.open...UplatneniVysledku	2012
http://linked.open...v/svazekPeriodika	2012
http://linked.open...iv/tvurceVysledku	Kučera, Petr Čepek, Ondřej Vlček, Václav
http://linked.open...ain/vavai/riv/wos	000307258500015
issn	0302-9743
number of pages	13 (xsd:int)
http://bibframe.org/vocab/doi	10.1007/978-3-642-27660-6_15
http://localhost/t...ganizacniJednotka	11320
is http://linked.open...avai/riv/vysledek of	Properties of SLUR Formulae

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 58 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software