A decomposition method for CNF minimality proofs

Result code in 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>
Result on the web
<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>

Result language
angličtina
Original language name
A decomposition method for CNF minimality proofs
Original language description
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.
Czech name
—
Czech description
—

Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
IN - Informatics
OECD FORD branch
—

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)

Publication year
2013
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)