Boolean functions with a simple certificate for CNF complexity
Autor: | Petr Kučera, Petr Savický, Ondřej Čepek |
---|---|
Rok vydání: | 2012 |
Předmět: |
Discrete mathematics
Applied Mathematics Existential quantification Function (mathematics) Disjoint sets Upper and lower bounds Set (abstract data type) Combinatorics Simple (abstract algebra) Discrete Mathematics and Combinatorics Boolean functions CNF representations Boolean function Representation (mathematics) Mathematics |
Zdroj: | Discrete Applied Mathematics. 160:365-382 |
ISSN: | 0166-218X |
DOI: | 10.1016/j.dam.2011.05.013 |
Popis: | In this paper we study relationships between CNF representations of a given Boolean function f and essential sets of implicates of f . It is known that every CNF representation and every essential set must intersect. Therefore the maximum number of pairwise disjoint essential sets of f provides a lower bound on the size of any CNF representation of f . We are interested in functions, for which this lower bound is tight, and call such functions coverable. We prove that for every coverable function there exists a polynomially verifiable certificate (witness) for its minimum CNF size. On the other hand, we show that not all functions are coverable, and construct examples of non-coverable functions. Moreover, we prove that computing the lower bound, i.e. the maximum number of pairwise disjoint essential sets, is N P -hard under various restrictions on the function and on its input representation. Highlights? We study certain lower bounds for a CNF size (number of clauses) of a Boolean function. ? The lower bound is given by the maximum number of disjoint essential sets of implicates. ? Boolean functions for which this lower bound is tight are called coverable. ? Non-coverable functions exist and the gap may be arbitrarily large. ? Complexity of computing the lower bound under different conditions is investigated. |
Databáze: | OpenAIRE |
Externí odkaz: |