A decomposition method for CNF minimality proofs
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F13%3A10144058" target="_blank" >RIV/00216208:11320/13:10144058 - isvavai.cz</a>
Výsledek na webu
<a href="http://dx.doi.org/10.1016/j.tcs.2013.09.016" target="_blank" >http://dx.doi.org/10.1016/j.tcs.2013.09.016</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1016/j.tcs.2013.09.016" target="_blank" >10.1016/j.tcs.2013.09.016</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
A decomposition method for CNF minimality proofs
Popis výsledku v původním jazyce
A CNF is minimal if no shorter CNF representing the same function exists, where by CNF length we mean either the number of clauses or the total number of literals (sum of clause lengths). In this paper we develop a decomposition approach that can be in certain situations applied to a CNF formula when proving its minimality. We give two examples in which this decomposition approach is used. Both examples deal with pure Horn minimization, a problem defined as follows: given a pure Horn CNF, construct a logically equivalent pure Horn CNF which is the shortest possible (either w.r.t. the number of clauses or w.r.t. the total number of literals). Both presented examples give alternative proofs of known complexity results for pure Horn minimization.
Název v anglickém jazyce
A decomposition method for CNF minimality proofs
Popis výsledku anglicky
A CNF is minimal if no shorter CNF representing the same function exists, where by CNF length we mean either the number of clauses or the total number of literals (sum of clause lengths). In this paper we develop a decomposition approach that can be in certain situations applied to a CNF formula when proving its minimality. We give two examples in which this decomposition approach is used. Both examples deal with pure Horn minimization, a problem defined as follows: given a pure Horn CNF, construct a logically equivalent pure Horn CNF which is the shortest possible (either w.r.t. the number of clauses or w.r.t. the total number of literals). Both presented examples give alternative proofs of known complexity results for pure Horn minimization.
Klasifikace
Druh
J<sub>x</sub> - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)
CEP obor
IN - Informatika
OECD FORD obor
—
Návaznosti výsledku
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)
Ostatní
Rok uplatnění
2013
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 periodika
Theoretical Computer Science
ISSN
0304-3975
e-ISSN
—
Svazek periodika
510
Číslo periodika v rámci svazku
říjen
Stát vydavatele periodika
NL - Nizozemsko
Počet stran výsledku
16
Strana od-do
111-126
Kód UT WoS článku
000328296800007
EID výsledku v databázi Scopus
—