Strong Duality in Horn Minimization

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F17%3A10371729" target="_blank" >RIV/00216208:11320/17:10371729 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-662-55751-8_11" target="_blank" >http://dx.doi.org/10.1007/978-3-662-55751-8_11</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-662-55751-8_11" target="_blank" >10.1007/978-3-662-55751-8_11</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Strong Duality in Horn Minimization

Popis výsledku v původním jazyce

A pure Horn CNF is minimal if no shorter pure Horn CNF representing the same function exists, where the CNF length may mean several different things, e.g. the number of clauses, or the total number of literals (sum of clause lengths), or the number of distinct bodies (source sets). The corresponding minimization problems (a different problem for each measure of the CNF size) appear not only in the Boolean context, but also as problems on directed hypergraphs or problems on closure systems. While minimizing the number of clauses or the total number of literals is computationally very hard, minimizing the number of distinct bodies is polynomial time solvable. There are several algorithms in the literature solving this task. In this paper we provide a structural result for this body minimization problem. We develop a lower bound for the number of bodies in any CNF representing the same Boolean function as the input CNF, and then prove a strong duality result showing that such a lower bound is always tight. This in turn gives a simple sufficient condition for body minimality of a pure Horn CNF, yielding a conceptually simpler minimization algorithm compared to the existing ones, which matches the time complexity of the fastest currently known algorithm.

Název v anglickém jazyce

Strong Duality in Horn Minimization

Popis výsledku anglicky

A pure Horn CNF is minimal if no shorter pure Horn CNF representing the same function exists, where the CNF length may mean several different things, e.g. the number of clauses, or the total number of literals (sum of clause lengths), or the number of distinct bodies (source sets). The corresponding minimization problems (a different problem for each measure of the CNF size) appear not only in the Boolean context, but also as problems on directed hypergraphs or problems on closure systems. While minimizing the number of clauses or the total number of literals is computationally very hard, minimizing the number of distinct bodies is polynomial time solvable. There are several algorithms in the literature solving this task. In this paper we provide a structural result for this body minimization problem. We develop a lower bound for the number of bodies in any CNF representing the same Boolean function as the input CNF, and then prove a strong duality result showing that such a lower bound is always tight. This in turn gives a simple sufficient condition for body minimality of a pure Horn CNF, yielding a conceptually simpler minimization algorithm compared to the existing ones, which matches the time complexity of the fastest currently known algorithm.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA15-15511S" target="_blank" >GA15-15511S: Booleovské techniky v reprezentaci znalostí</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2017

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ů

Název statě ve sborníku

Fundamentals of Computation Theory, 21st International Symposium, FCT 2017

ISBN

978-3-662-55750-1

ISSN

0302-9743

e-ISSN

neuvedeno

Počet stran výsledku

13

Strana od-do

123-135

Název nakladatele

Springer-Verlag

Místo vydání

Berlin

Místo konání akce

Bordeaux, France

Datum konání akce

11. 9. 2017

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—