On Hierarchies over the SLUR Class
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F12%3A10126646" target="_blank" >RIV/00216208:11320/12:10126646 - isvavai.cz</a>
Result on the web
<a href="http://www.cs.uic.edu/pub/Isaim2012/WebPreferences/ISAIM2012_Boolean_Balyo_etal.pdf" target="_blank" >http://www.cs.uic.edu/pub/Isaim2012/WebPreferences/ISAIM2012_Boolean_Balyo_etal.pdf</a>
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
On Hierarchies over the SLUR Class
Original language description
SLUR is a class of the CNF formulae on which the single lookahead unit resolution algorithm for satis?ability (SAT) testing never fails. It is known that the SLUR class contains classes of Horn, hidden Horn, (hidden) extended Horn and balanced formulae as a subclass. In recent paper it was proven that the SLUR class contains all canonical formulae. In this paper we will extend this result by showing it suf?ces that all prime implicates can be derived in one resolution step from input formula. We will also generalize previous hierarchy called SLUR(i) which is built on top of the SLUR class.
Czech name
—
Czech description
—
Classification
Type
O - Miscellaneous
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GAP202%2F10%2F1188" target="_blank" >GAP202/10/1188: KnowSched: Knowledge Techniques in Scheduling</a><br>
Continuities
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
Others
Publication year
2012
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů