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:
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