On the maximal minimal cube lengths in distinct DNF tautologies

TL;DR

This paper explores the maximum minimal clause length in certain DNF formulas with specific structural constraints, using SAT solvers to answer open questions and analyze symmetric cases.

Contribution

It introduces a computational approach to determine maximal minimal clause lengths in constrained DNF formulas, extending previous theoretical work.

Findings

Identified maximal minimal clause lengths for various DNF configurations

Solved open questions from prior research using SAT solvers

Analyzed the impact of symmetry constraints on DNF formulas

Abstract

Inspired by a recent article by Anthony Zaleski and Doron Zeilberger, we investigate the question of determining the largest k for which there exists boolean formulas in disjunctive normal form (DNF) with n variables, none of whose conjunctions are `parallel', and such that all of them have at least k literals. Using a SAT solver, we answer some of the questions they left open. We also determine the corresponding numbers for DNFs obeying certain symmetries.

Full text

∗ Supported by the Austrian FWF grants F5004 and P31571-N32.

∗∗ Supported by the Austrian FWF grant S11408-N23.

1. Problem Statement

We consider boolean formulas with $n$ variables $x_{1},\dots,x_{n}$. A literal is a variable or a negated variable, e.g., $x_{3}$ or $\bar{x}_{7}$. A cube is a conjunction of literals, e.g., $x_{3}\land\bar{x}_{7}$. The length of a cube is the number of distinct literals appearing in it. A formula in disjunctive normal form (DNF) is a disjunction of cubes, e.g., $(x_{3}\land\bar{x}_{7})\lor(x_{5}\land\bar{x}_{6}\land x_{7})$. Such a DNF is called a tautology if it evaluates to true for all assignments of the variables. For example $x_{3}\lor x_{5}\lor(\bar{x}_{3}\land\bar{x}_{5})$ is a tautology. It consists of two cubes of length 1 and one cube of length 2.

Inspired by work of Erdös [3], Zaleski and Zeilberger [8] have recently considered DNFs in which all cubes have distinct supports. The support of a cube is the set of variables occurring in it. For example the support of the cube $x_{3}$ is the singleton set $\{3\}$, the support of the cube $\bar{x}_{5}$ is the singleton set $\{5\}$, while the support of the cube $\bar{x}_{3}\land x_{5}$ is the set $\{3,5\}$. This implies that the DNF $x_{3}\lor{\bar{x}_{5}}\lor(\bar{x}_{3}\land x_{5})$ has distinct supports. On the other hand the Hamlet question $x_{1}\lor\bar{x}_{1}$ does not have distinct supports. They call these formulas distinct DNFs. Inspired by a study of covering systems, Zaleski and Zeilberger want to know, for any given $n$, what is the largest $k$ such that there is a distinct DNF tautology with $n$ variables only consisting of cubes of length at least $k$.

Using a greedy algorithm, they searched for distinct DNF tautologies with a prescribed number of variables and a prescribed minimal cube length. The largest minimal cube length for which they found formulas are as follows:

[TABLE]

These are only lower bounds for the optimal values of $k$. However, by a density argument it can be shown that the optimal $k$ must satisfy the inequality $\sum_{i=k}^{n}\binom{n}{i}2^{-i}\geq 1$, which gives rise to upper bounds. The numbers given in the table above turn out to match the upper bounds except for $n=10$ and $n=14$ (indicated by question marks), where they are off by one.

As a variant of the problem, Zaleski and Zeilberger also wanted to know, for any given $n$, what is the largest $k$ such that there is a distinct DNF tautology with $n$ variables only consisting of cubes of length exactly $k$. In this case, the density argument implies that such a $k$ must satisfy $\binom{n}{k}2^{-k}\geq 1$, which again gives an upper bound. With their greedy approach, they determined the following lower bounds. Again, mismatches with the upper bound are indicated by a question mark.

[TABLE]

It is clear that there is no solution for $n=3$ and $k=1$, so in this case the upper bound is too pessimistic and $k=0$ is the right value.

For $n=5$ and $n=9$ the computations reported in the present paper imply that the values $2$ and $5$ are also correct. We were not able to confirm the entry for $n=10$ in the first table with about one year of computation time. We did not attempt to confirm the entries for $n=14$ in the first or $n=13$ in the second table.

We add two refinements to the problem. First, we introduce an additional parameter $u$ which bounds the lengths of the cubes from above. For any particular choice $n,u$, we want to know the largest $k$ such that there is a distinct DNF tautology with $n$ variables only consisting of cubes of length at least $k$ and at most $u$. The special case $u=n$ corresponds to the first variant of Zaleski and Zeilberger and the special case $u=k$ corresponds to the second variant. We think that the intermediate cases are also of interest.

Our second refinement concerns symmetries. Letting permutations act on the indices of the variables, we say that a DNF is invariant under a certain subgroup $G$ of $S_{n}$ if every $g\in G$ maps the DNF to itself. For example, the DNF $(x_{1}\land\bar{x}_{2}\land x_{3})\lor(x_{2}\land\bar{x}_{3}\land x_{4})\lor(x_{3}\land\bar{x}_{4}\land x_{1})\lor(x_{4}\land\bar{x}_{1}\land x_{3})$ is invariant under the cyclic group $C_{4}$. For the groups $C_{n}$, $D_{n}$, $A_{n}$, and $S_{n}$, and for various choices of $n$ and $u$, we have determined the largest $k$ such that there is a distinct DNF tautology with $n$ variables consisting of cubes of lengths at least $k$ and at most $u$ which are invariant under the given group.

2. SAT Encoding

Our results were obtained with the help of a SAT solver [5, 6], using a rather straightforward encoding of the problem. For each cube, we introduced one boolean variable that indicates whether or not this cube is going to be a part of the DNF we are looking for. Note that this creates $\sum_{i=k}^{u}\binom{n}{i}2^{i}$ variables, a quantity that grows quickly when $n$ or $u-k$ increase. For example, in the case $n=u=10$ and $k=7$, where we were unable to complete the computation, we were dealing with 33024 variables.

In order to enforce that the DNF is a tautology, we specify for every assignment a clause saying that at least one of the cubes that becomes true under this assignment must be selected. In order to enforce that the DNF be distinct, we have to specify clauses which encode the requirement that for every possible support, at most one of the cubes having this support can be selected. There are many ways to encode a constraint of the form “at most one”, and their pros and cons are discussed extensively in the literature [2, 4]. For our purpose, the so-called binary encoding seemed to work well.

Finally, in order to enforce invariance under a certain group, we chose a set of generators and added for each cube $c$ and each generator $g$ a clause that says “if $c$ is selected, then also $g(c)$”.

The encoding as described so far is sufficient for proving existence or non-existence of a distinct DNF tautology for any prescribed $n,u,k$, and any prescribed group. In order to speed up the computations in practice, we may add some further constraints. One idea is to add clauses which forbid to select two cubes where one is strictly contained in the other. This is clearly a valid restriction, because when there is a solution that has two cubes that are contained in one another, we can discard the smaller one from it and obtain another solution. However, it turns out that this particular idea floods the formula with too many additional clauses and slows down the computation rather than speeding it up.

It is more efficient to break the symmetry of the problem, a standard technique in the context of SAT solving [7]. Clearly, when there is a distinct DNF for certain $n,u,k$ and a certain group, then permuting all the variables $x_{1},\dots,x_{n}$ in some way will yield another solution. Also replacing a certain variable $x_{i}$ by its negation $\bar{x}_{i}$ (and canceling double negation introduced by that) turns a solution into a new solution. Since we dropped the idea to forbid cubes that are contained in other cubes, we can restrict the search to a solution containing a cube of length $k$, and because we are free to permute and negate variables, we may assume this cube to be $x_{1}\land x_{2}\land\cdots\land x_{k}$.

Adding the variable for this cube to the formula allows for an appreciable amount of simplification (called unit propagation [5] in SAT jargon). We are left with the freedom to permute the variables $x_{1},\dots,x_{k}$ and the variables $x_{k+1},\dots,x_{n}$. By the first, it is fair to enforce an assumption that the variables are indexed in such a way that when a cube with support $x_{1},\dots,x_{k-1},x_{k+1}$ is selected, there is some $i$ such that $x_{1},\dots,x_{i}$ appear negated in it and the remaining variables do not. This assumption may still leave some degrees of freedom, which can be used to make a similar restriction as to which cubes with support $x_{1},\dots,x_{k-1},x_{k+2}$ may be selected. The freedom to permute the variables $x_{k+1},\dots,x_{n}$ is exploited by restricting the search to DNFs such for every $i=k+1,\dots,n-1$, the cube $x_{1}\land\cdots\land x_{k-1}\land x_{i+1}$ is only selected when $x_{1}\land\cdots\land x_{k-1}\land x_{i}$ is also selected.

3. Results

We have written a Python script that produces the SAT instances described in the previous section, and we have used Biere’s award-winning SAT solver Treengeling [1] to solve them. The results are summarized in the following tables, in which $n$ appears increased towards the right and $u$ grows downwards. Entries with $u>n$ are left blank because they are equivalent to $u=n$.

By the density argument, the maximal $k$ for a particular choice of $n$ and $u$ must satisfy the inequality $\sum_{i=k}^{u}\binom{n}{i}2^{-i}\geq 1$. In the following table, an entry is boxed when it does not match this bound. For the entries marked with a question mark, we have not been able to prove that the $k$ we found is really optimal, but the long and successless search is at least some indication that the bound is not reached in these cases. For $(n,u)\in\{(5,3),(9,6),(10,8)\}$, the SAT solver is able to show that distinct DNF tautologies with $k=3$, $k=6$, $k=7$, respectively, do not exist, although their existence would not be in conflict with the density bound.

[TABLE]

The next two tables contain our results about distinct DNF tautologies invariant under certain groups. We have investigated the cyclic group $C_{n}$, the dihedral group $D_{n}$, the alternating group $A_{n}$, and the full symmetric group $S_{n}$. The table on the left lists the numbers for $C_{n}$ and $D_{n}$, which turn out to be identical. Boxed entries highlight the differences to the previous table. The question marks refer to the search for $C_{n}$, which for three entries did not terminate in a reasonable amount of time. Interestingly, it follows from the previous table that the entry for $(n,u)=(10,8)$ is correct, but while the SAT solver was able to prove this in the (seemingly harder) case without invariant constraints, it did not succeed with the constraints for $C_{n}$. The computations for all entries terminated in presence of the constraints for $D_{n}$.

[TABLE]

[TABLE]

The table on the right lists the numbers for $A_{n}$ and $S_{n}$, which also turn out to be the same. For these groups, the invariant constraints make the problem easier, so that we were able to cover slightly larger values of $n$ and $u$. All given numbers have been proved to be optimal. Note that a regular pattern emerges: we seem to have the formula $k=\min(u-1,\lfloor n/2\rfloor)$.