This paper integrates weak decomposable negation normal form (wDNNF) circuits, introduced by Akshay et al. in 2018, into the knowledge compilation map. This circuit type generalises decomposable negation normal form (DNNF) circuits in such a way that they allow a restricted form of sharing variables among the inputs of a conjunction node. We show that wDNNF circuits have the same properties as DNNF circuits regarding the queries and transformations presented in the knowledge compilation map, whilst being strictly more succinct than DNNF circuits (that is, they can represent Boolean functions compactly). We also present and evaluate a knowledge compiler, called Bella, for converting CNF formulae into wDNNF circuits. Our experiments demonstrate that wDNNF circuits are suitable for configuration instances.

Horn functions form an important subclass of Boolean functions and appear in many different areas of computer science and mathematics as a general tool to describe implications and dependencies. Finding minimum sized representations for such functions with respect to most commonly used measures is a computationally hard problem admitting a $2^{\log^{1-o(1)}n}$ inapproximability bound. In this paper we consider the natural class of key Horn functions representing keys of relational databases. For this class, the minimization problems for most measures remain NP-hard. In this paper we provide logarithmic factor approximation algorithms for key Horn functions with respect to all such measures.

Given a relational database, a key is a set of attributes such that a value assignment to this set uniquely determines the values of all other attributes. The database uniquely defines a pure Horn function h, representing the functional dependencies. If the knowledge of the attribute values in set A determines the value for attribute v, then A→v is an implicate of h. If K is a key of the database, then K→v is an implicate of h for all attributes v. Keys of small sizes play a crucial role in various problems. We present structural and complexity results on the set of minimal keys of pure Horn functions. We characterize Sperner hypergraphs for which there is a unique pure Horn function with the given hypergraph as the set of minimal keys. Furthermore, we show that recognizing such hypergraphs is co-NP-complete already when every hyperedge has size two. On the positive side, we identify several classes of graphs for which the recognition problem can be decided in polynomial time. We also present an algorithm that generates the minimal keys of a pure Horn function with polynomial delay, improving on earlier results. By establishing a connection between keys and target sets, our approach can be used to generate all minimal target sets with polynomial delay when the thresholds are bounded by a constant. As a byproduct, our proof shows that the Minimum Key problem is at least as hard as the Minimum Target Set Selection problem with bounded thresholds.

We describe a compilation language of backdoor decomposable monotone circuits (BDMCs) which generalizes several concepts appearing in the literature, e.g. DNNFs and backdoor trees. A C-BDMC sentence is a monotone circuit which satisfies decomposability property (such as in DNNF) in which the inputs (or leaves) are associated with CNF encodings from a given base class C. We consider the class of propagation complete (PC) encodings as a base class and we show that PC-BDMCs are polynomially equivalent to PC encodings. Additionally, we use this to determine the properties of PC-BDMCs and PC encodings with respect to the knowledge compilation map including the list of efficient operations on the languages.

Given a CNF formula Φ with clauses C1,…,Cm and variables V={x1,…,xn}, a truth assignment a:V→{0,1} of Φ leads to a clause sequence σΦ(a)=(C1(a),…,Cm(a))∈{0,1}m where Ci(a)=1 if clause Ci evaluates to 1 under assignment a, otherwise Ci(a)=0. The set of all possible clause sequences carries a lot of information on the formula, e.g. SAT, MAX-SAT and MIN-SAT can be encoded in terms of finding a clause sequence with extremal properties. We consider a problem posed at Dagstuhl Seminar 19211 “Enumeration in Data Management” (2019) about the generation of all possible clause sequences of a given CNF with bounded dimension. We prove that the problem can be solved in incremental polynomial time. We further give an algorithm with polynomial delay for the class of tractable CNF formulas. We also consider the generation of maximal and minimal clause sequences, and show that generating maximal clause sequences is NP-hard, while minimal clause sequences can be generated with polynomial delay.

In this paper, we investigate CNF encodings, for which unit propagation is strong enough to derive a contradiction if the encoding is not consistent with a partial assignment of the variables (unit refutation complete or URC encoding) or additionally to derive all implied literals if the encoding is consistent with the partial assignment (propagation complete or PC encoding). We prove an exponential separation between the sizes of PC and URC encodings without auxiliary variables and strengthen the known results on their relationship to the PC and URC encodings that can use auxiliary variables. Besides of this, we prove that the sizes of any two irredundant PC formulas representing the same function differ at most by a factor polynomial in the number of the variables and present an example of a function demonstrating that a similar statement is not true for URC formulas. One of the separations above implies that a q-Horn formula may require an exponential number of additional clauses to become a URC formula. On the other hand, for every q-Horn formula, we present a polynomial size URC encoding of the same function using auxiliary variables. This encoding is not q-Horn in general.

A Boolean formula in conjunctive normal form (CNF) is called matched if the system of sets of variables which appear in individual clauses has a system of distinct representatives. We present here two results for matched CNFs: The first result is a shorter and simpler proof of the fact that Boolean minimization remains complete for the second level of polynomial hierarchy even if the input is restricted to matched CNFs. The second result is structural --- we show that if a Boolean function f admits a representation by a matched CNF then every clause minimum CNF representation of f is matched.

A matched formula is a CNF formula whose incidence graph admits a matching which matches a distinct variable to every clause. Such a formula is always satisfiable. Matched formulas are used, for example, in the area of parameterized complexity. We prove that the problem of counting the number of the models (satisfying assignments) of a matched formula is #P-complete. On the other hand, we define a class of formulas generalizing the matched formulas and prove that for a formula in this class one can choose in polynomial time a variable suitable for splitting the tree for the search of the models of the formula. As a consequence, the models of a formula from this class, in particular of any matched formula, can be generated sequentially with a delay polynomial in the size of the input. On the other hand, we prove that this task cannot be performed efficiently for linearly satisfiable formulas, which is a generalization of matched formulas containing the class considered above.

A matched formula is a CNF formula whose incidence graph admits a matching which matches a distinct variable to every clause. Such a formula is always satisfiable. Matched formulas are used, for example, in the area of parametrized complexity. We prove that the problem of counting the number of the models (satisfying assignments) of a matched formula is #P-complete. On the other hand, we define a class of formulas generalizing the matched formulas and prove that for a formula in this class one can choose in polynomial time a variable suitable for splitting the tree for the search of the models of the formula. As a consequence, the models of a formula from this class, in particular of any matched formula, can be generated sequentially with a delay polynomial in the size of the input. On the other hand, we prove that this task cannot be performed efficiently for linearly satisfiable formulas, which is a generalization of matched formulas containing the class considered above.

A Boolean formula in conjunctive normal form (CNF) is called matched if the system of sets of variables which appear in individual clauses has a system of distinct representatives. Each matched CNF is trivially satisfiable (each clause can be satisfied by its representative variable). Another property which is easy to see, is that the class of matched CNFs is not closed under partial assignment of truth values to variables. This latter property leads to a fact (proved here) that given two matched CNFs it is co-NP complete to decide whether they are logically equivalent. The construction in this proof leads to another result: a much shorter and simpler proof of the fact that the Boolean minimization problem for matched CNFs is a complete problem for the second level of the polynomial hierarchy. The main result of this paper deals with the structure of clause minimum CNFs. We prove here that if a Boolean function f admits a representation by a matched CNF then every clause minimum CNF representation of f is matched.