arXiv is now an independent nonprofit! Learn more
License: arXiv.org perpetual non-exclusive license
arXiv:2309.01750v2 [math.CO] 03 Oct 2023

On CNF formulas irredundant with respect to unit clause propagation

Petr Savický
Institute of Computer Science of the Czech Academy of Sciences
Czech Republic
   e-mail: savicky@cs.cas.cz
Abstract

Abstract

Two CNF formulas are called ucp-equivalent, if they behave in the same way with respect to the unit clause propagation (ucp). A formula is called ucp-irredundant, if removing any clause leads to a formula which is not ucp-equivalent to the original one. As a consequence of known results, the ratio of the size of a ucp-irredundant formula and the size of a smallest ucp-equivalent formula is at most n2n^{2}, where nn is the number of the variables. We demonstrate an example of a ucp-irredundant formula for a symmetric definite Horn function which is larger than a smallest ucp-equivalent formula by a factor Ω(n/lnn)\Omega(n/\ln n) and, hence, a general upper bound on the above ratio cannot be smaller than this.

1 Introduction

In some contexts, the strength of unit clause propagation (UCP) on the formula is important and formulas representing the same function have to be distinguished according to the behavior of UCP on them. An important example is the set of learned clauses in a SAT solver. Most of these clauses are implicates of the original formula so they do not change the represented function and they are added in order to make UCP stronger. In order to investigate formulas that appear in such a context, we need to compare the strength of UCP on different formulas. In this paper, we consider a corresponding equivalence and irredundancy. Two CNF formulas are called ucp-equivalent, if for every partial assignment α\alpha, UCP derives the same consistent set of literals from the two formulas together with α\alpha or we get a contradiction in both cases. A formula is called ucp-irredundant, if removing any clause makes UCP on the formula weaker and, hence, the obtained formula is not ucp-equivalent to the original one.

UCP in a CNF formula can be precisely described by its dual-rail encoding [3, 4, 5, 6, 11, 14, 15] which represents UCP by a specific Horn formula. In particular, two formulas are ucp-equivalent if and only if their dual-rail encodings are equivalent in the usual sense to represent the same Horn function. It is a well-known result [10] that the ratio of the size of a Horn formula irredundant with respect to representing a given function and the size of a smallest equivalent formula is at most the number of the variables. Using the dual-rail encoding we can transform this result to ucp-irredundant formulas, however, since dual-rail encoding changes the number of the clauses, we get a worse bound, namely 2n22n^{2}, where nn is the number of the variables. A slightly better bound n2n^{2} can be obtained by a proof used in [12] to prove the same bound for propagation complete formulas since the assumption of propagation completeness is used only to guarantee ucp-equivalence. Moreover, it appears that the factor n2n^{2} holds both for the number of clauses and for the length of the formula.

It is not clear whether a general upper bound on the ratio better than n2n^{2} can be obtained. The main result of the paper is an example of a ucp-irredundant formula φ\varphi^{\ell} of nn variables which is larger than the smallest ucp-equivalent formula φ\varphi^{*} by a factor Ω(n/lnn)\Omega(n/\ln n). It follows that a general upper bound on the ratio discussed above cannot be smaller than this.

The formulas used in the example represent a symmetric definite Horn function and the construction of the formula φ\varphi^{\ell} is easy. The hard part of the proof is to derive an upper bound on the size of φ\varphi^{*} and we show that the size of φ\varphi^{*} is closely related to the size of a specific covering system. Namely, for nn and k=n/2+O(1)k=n/2+O(1), we use a system of (k+1)(k+1)-subsets of an nn-set such that every kk-set is contained in at least one member of the system. The proof is then finished using a known upper bound on the size of such a system from [7] or a different upper bound from [18, 8].

Section 3 defines ucp-equivalence and ucp-irredundancy and Section 4 formulates the results. The property of the formulas needed for the results is reformulated in Section 5 as a property of a hypergraph. The construction of the required hypergraph is described in Section 7 using an auxiliary result from Section 6. The proofs of the results are summarized in Section 8. Conclusion and questions for further research are formulated in Section 9.

2 Preliminaries

2.1 CNF formulas

A literal is a variable or its negation, a clause is a disjunction of literals on different variables, and a CNF formula is a conjunction of clauses. Since we consider only CNF formulas, we call them formulas for simplicity.

A formula is considered as a set of clauses and a clause is considered as a set of literals. In particular, we use set operations on formulas and clauses. The size of a formula is the number of its clauses. A clause CC is an implicate of a formula φ\varphi, if φ\varphi implies CC. A clause CC is a prime implicate of a formula φ\varphi, if it is an implicate of φ\varphi and no proper subset of CC is an implicate of φ\varphi. If AA is a set of variables, let neg(A)={¬xxA}\mathrm{neg}(A)=\{\neg x\mid x\in A\}.

A formula is a Horn formula, if every clause contains at most one positive literal and a formula is a definite Horn formula, if every clause contains exactly one positive literal.

A partial assignment of the variables is a partial map from the variables to the set {0,1}\{0,1\} understood as a conjunction of identities of the form x=ax=a, where xx is a variable and a{0,1}a\in\{0,1\}. It is usual to represent a partial assignment by a conjunction of the literals equivalent to these identities. For example, the conjunction of identities x1=1x2=0x_{1}=1\wedge x_{2}=0 is equivalent to the conjunction of literals x1¬x2x_{1}\wedge\neg x_{2}.

Assume a formula φ\varphi, a clause CφC\in\varphi, and a literal lCl\in C. If α\alpha is a partial assignment falsifying all literals in C{l}C\setminus\{l\}, then every satisfying assignment of φ\varphi extending α\alpha satisfies ll and, hence, ll is a consequence of φα\varphi\wedge\alpha. Unit propagation in a formula φ\varphi from a partial assignment α\alpha is the process of extending α\alpha by assignments obtained as consequences of φα\varphi\wedge\alpha of this simple type. The process terminates if either no further literal can be derived in this way or all the literals in some of the clauses of φ\varphi are falsified. In the latter case, we say that a contradiction is derived and this means that the initial partial assignment cannot be extended to a satisfying assignment of φ\varphi. The opposite implication is not true. For example, unit propagation in the formula (x1x2)(x1¬x2)(¬x1x2)(¬x1¬x2)(x_{1}\vee x_{2})\wedge(x_{1}\vee\neg x_{2})\wedge(\neg x_{1}\vee x_{2})\wedge(\neg x_{1}\vee\neg x_{2}) from the empty assignment does not derive any literal and, hence, does not derive a contradiction, however, the formula is unsatisfiable.

2.2 Covering and Turán numbers

We use known bounds on covering numbers C(n,r,k)C(n,r,k) [9] and the closely related Turán numbers T(n,,t)T(n,\ell,t) [18, 8] defined using different conventions. Note that Turán’s theorem implies a precise value of T(n,,2)T(n,\ell,2), if we minimize the number of edges to be removed from a complete graph on nn vertices in order to eliminate all complete subgraphs on \ell vertices.

Definition 2.1.

For integers n>r>k>0n>r>k>0, let the covering number C(n,r,k)C(n,r,k) be the smallest size of a system of rr-subsets of an nn-set such that every kk-subset is contained in at least one set in the system.

Definition 2.2.

For integers n>>t>0n>\ell>t>0, let the Turán number T(n,,t)T(n,\ell,t) be the smallest size of a system of tt-subsets of an nn-set such that every \ell-subset contains at least one set in the system.

By taking complements of the sets, we obtain C(n,r,k)=T(n,nk,nr)C(n,r,k)=T(n,n-k,n-r). Let us recall several known results on covering numbers in the case r=k+1r=k+1 which we use. Clearly,

C(n,k+1,k)1k+1(nk).C(n,k+1,k)\geq\frac{1}{k+1}{n\choose k}\;. (1)

If kk is fixed and nn\to\infty, then by [16], we have

C(n,k+1,k)=(1+o(1))1k+1(nk).C(n,k+1,k)=(1+o(1))\frac{1}{k+1}{n\choose k}\;.

We are mainly interested in cases when k=n/2+O(1)k=n/2+O(1) for which only less precise bounds are known. Let μ(n,k)\mu(n,k) be such that

C(n,k+1,k)=1k+1(nk)μ(n,k)C(n,k+1,k)=\frac{1}{k+1}{n\choose k}\mu(n,k) (2)

and, equivalently,

T(n,t+1,t)=1t+1(nt)μ(n,nt1).T(n,t+1,t)=\frac{1}{t+1}{n\choose t}\mu(n,n-t-1)\;. (3)

By (1), we have 1μ(n,k)1\leq\mu(n,k). For an upper bound on μ(n,k)\mu(n,k), let us recall the following.

Theorem 2.3 (a special case of Theorem 13.4 from [7]).

For every n>k2n>k\geq 2, we have

C(n,k+1,k)1k+1(nk)(1+ln(k+1))C(n,k+1,k)\leq\frac{1}{k+1}{n\choose k}(1+\ln(k+1)) (4)

This implies

1μ(n,k)1+ln(k+1)1\leq\mu(n,k)\leq 1+\ln(k+1) (5)

for every n>k2n>k\geq 2. An incomparable upper bound on μ(n,k)\mu(n,k) follows from the bound [18] on Turán numbers improving [8] by a factor of 22. By this bound, we have

T(n,t+1,t)(1+o(1))lnt2t(nt)T(n,t+1,t)\leq\frac{(1+o(1))\ln t}{2t}{n\choose t} (6)

for nn\to\infty and tt\to\infty. Combining (6) with (3), substituting k=nt1k=n-t-1 and assuming nkn-k\to\infty, we obtain

μ(n,k)1+o(1)2ln(nk1).\mu(n,k)\leq\frac{1+o(1)}{2}\ln(n-k-1)\;. (7)

Bounds (5) and (7) are complementary in the sense that (5) is better, if kk is small, while (7) is better, if kk is close to nn. In Section 8 we need also the following.

Lemma 2.4.

For every n>k>1n>k>1, we have

μ(n1,k1)\displaystyle\mu(n-1,k-1) \displaystyle\leq μ(n,k)\displaystyle\mu(n,k) (8)
nk+1n+1μ(n,k)\displaystyle\frac{n-k+1}{n+1}\mu(n,k) \displaystyle\leq μ(n+1,k)\displaystyle\mu(n+1,k) (9)
Proof.

By [17, 9], we have

nk+1C(n1,k,k1)C(n,k+1,k)\frac{n}{k+1}C(n-1,k,k-1)\leq C(n,k+1,k)

implying (8). Assume a system of (k+1)(k+1)-subsets of a set XX of n+1n+1 points of size C(n+1,k+1,k)C(n+1,k+1,k) and covering all kk-subsets. For any xXx\in X, one can create a system of (k+1)(k+1)-subsets of X{x}X\setminus\{x\} covering all kk-subsets by replacing each ocurrence of xx in a (k+1)(k+1)-tuple in the system by any element of X{x}X\setminus\{x\} not contained in the (k+1)(k+1)-tuple. Hence, we have

C(n,k+1,k)C(n+1,k+1,k)C(n,k+1,k)\leq C(n+1,k+1,k)

implying (9). ∎

3 Ucp-equivalence and ucp-irredundancy

A formula φ\varphi is called propagation complete (PC), if for every partial assignment α\alpha of the variables, UCP from φα\varphi\wedge\alpha derives a contradiction, if φα\varphi\wedge\alpha is not consistent, and all implied literals otherwise. A PC formula is called irredundant PC formula, if removing any clause leads to a formula which is not a PC formula equivalent to the original one.

By the result [12], the ratio of the size of an arbitrary irredundant PC formula and a smallest equivalent PC formula is at most n2n^{2}, where nn is the number of the variables. The assumption that the two formulas are PC is used only to obtain that they behave in the same way with respect to UCP, since UCP on both of them is controlled by the represented function. This suggests to generalize the result using ucp-equivalence defined below. In particular, a PC formula is a formula ucp-equivalent to the set of all its (prime) implicates.

Definition 3.1.

Formulas φ1\varphi_{1} and φ2\varphi_{2} are ucp-equivalent if for every partial assignment α\alpha, unit clause propagation derives either the same partial assignment from φ1α\varphi_{1}\wedge\alpha and from φ2α\varphi_{2}\wedge\alpha or we get a contradiction in both cases.

In [5] a minimal PC formula is defined using the notion of an absorbed clause. A clause CC is absorbed by a formula φ\varphi, if for every lCl\in C, UCP from φneg(C{l})\varphi\wedge\mathrm{neg}(C\setminus\{l\}) derives ll or a contradiction. A formula is called minimal PC formula in [5] if none of its clauses is absorbed by the remaining ones. This does not guarantee that no smaller equivalent PC formula exists, however, the formula is irredundant with respect to the behavior of UCP. We use a straightforward generalization of this type of irredundancy obtained by removing the requirement that the formula is PC.

Definition 3.2.

A formula φ\varphi is ucp-irredundant if any of the following equivalent conditions is satisfied:

  • None of the clauses CφC\in\varphi is absorbed by φ{C}\varphi\setminus\{C\}.

  • For every CφC\in\varphi, the formulas φ\varphi and φ{C}\varphi\setminus\{C\} are not ucp-equivalent.

The following is a generalization of a similar upper bound for irredundant PC formulas from [12].

Proposition 3.3.

If φ\varphi is a ucp-irredundant formula on nn variables and φ\varphi^{*} is ucp-equivalent to φ\varphi, then

|φ|n2|φ||\varphi|\leq n^{2}|\varphi^{*}| (10)

and

φn2φ\|\varphi\|\leq n^{2}\|\varphi^{*}\| (11)
Proof.

Every clause of φ\varphi^{*} is absorbed by φ\varphi. Let φ\varphi^{\prime} be the set of clauses in φ\varphi needed for this for all clauses of φ\varphi^{*}. For each pair lCφl\in C\in\varphi^{*}, we need at most nn clauses of φ\varphi to derive ll or a contradiction from φneg(C{l})\varphi\wedge\mathrm{neg}(C\setminus\{l\}). This implies |φ|nφ|\varphi^{\prime}|\leq n\|\varphi^{*}\|. Since every clause of φ\varphi is absorbed by φ\varphi^{*}, every clause of φ\varphi^{*} is absorbed by φ\varphi^{\prime} and φφ\varphi^{\prime}\subseteq\varphi, the formula φ\varphi^{\prime} is ucp-equivalent to φ\varphi. Since φ\varphi is ucp-irredundant, we have |φ|nφ|\varphi|\leq n\|\varphi^{*}\| implying

|φ|nφn2|φ||\varphi|\leq n\|\varphi^{*}\|\leq n^{2}|\varphi^{*}|

and

φn|φ|n2φ\|\varphi\|\leq n|\varphi|\leq n^{2}\|\varphi^{*}\|

as required. ∎

4 The results

The main result is the following separation between the size of a ucp-irredundant formula and a smallest ucp-equivalent formula.

Theorem 4.1.

For every nn and k=n/2+O(1)k=n/2+O(1), there is a ucp-irredundant formula φ\varphi^{\ell} of nn variables and of size

|φ|=(k+1)(n1k)=Θ(n)(nk)|\varphi^{\ell}|=(k+1){n-1\choose k}=\Theta(n){n\choose k}

and such that a smallest ucp-equivalent formula φ\varphi^{*} has size

|φ|6(k+1)C(n,k+1,k)=O(lnn)(nk)|\varphi^{*}|\leq 6(k+1)C(n,k+1,k)=O(\ln n){n\choose k}

In particular, |φ|=Ω(n/lnn)|φ||\varphi^{\ell}|=\Omega(n/\ln n)|\varphi^{*}|.

For a proof, we investigate the size of ucp-irredundant formulas ucp-equivalent to the following definite Horn formula Ψn,k\Psi_{n,k}.

Definition 4.2.

For any integers nn, kk, such that 1kn11\leq k\leq n-1, let Ψn,k\Psi_{n,k} be the CNF formula consisting of all clauses on variables X={x1,,xn}X=\{x_{1},\ldots,x_{n}\} containing kk negative literals and one positive literal.

Clearly, |Ψn,k|=(nk)(nk)|\Psi_{n,k}|=(n-k){n\choose k}. A boolean function is called symmetric, if it is invariant under any permutation of its variables.

Lemma 4.3.

Formula Ψn,k\Psi_{n,k} represents the symmetric boolean function fn,kf_{n,k} of nn variables defined by

fn,k(x1,,xn)=1(i=1nxi<k)(i=1nxi=n)f_{n,k}(x_{1},\ldots,x_{n})=1\Leftrightarrow\left(\sum_{i=1}^{n}x_{i}<k\right)\vee\left(\sum_{i=1}^{n}x_{i}=n\right)
Proof.

By case inspection concerning the number of variables with value 11 and 00 in a given assignment. ∎

In particular, we prove the following upper and lower bound on the size of a smallest formula ucp-equivalent to Ψn,k\Psi_{n,k}.

Theorem 4.4.

The minimum size (number of clauses) of a formula ucp-equivalent to Ψn,k\Psi_{n,k} is at least

nC(n1,k,k1)=(nk)μ(n1,k1)(nk)n\,C(n-1,k,k-1)={n\choose k}\mu(n-1,k-1)\geq{n\choose k}

and if k=n/2+O(1)k=n/2+O(1) then it is at most

6(k+1)C(n,k+1,k)=6(nk)μ(n,k)=O(lnn)(nk).6(k+1)C(n,k+1,k)=6\,{n\choose k}\mu(n,k)=O(\ln n){n\choose k}\;.

The proof of Theorem 4.1 depends on Theorem 4.4 and the proof of both of them is summarized in Section 8 using constructions presented in this and the following sections. The lower and upper bound in Theorem 4.4 are proven to differ at most by a factor O(lnn)O(\ln n), however, it is plausible to assume that they are in fact closer, see the discussion of this in Section 8.

The lower bound in Theorem 4.4 is proven in Section 5. For the proof of the remaining statements, we construct for infinitely many pairs (n,k)(n,k) ucp-irredundant formulas φ\varphi^{\ell} (in Section 5) and φ\varphi^{*} (in Section 8) ucp-equivalent to Ψn,k\Psi_{n,k}, such that φ\varphi^{\ell} is as large as possible and φ\varphi^{*} is as small as possible. We obtain φ\varphi^{*} which meets the upper bound in Theorem 4.4 and the two formulas together satisfy Theorem 4.1. Each of the formulas φ\varphi^{\ell} and φ\varphi^{*} will be constructed as a hypergraph formula θ(H)\theta(H) where HH is a suitable hypergraph, see also [1, 2].

Definition 4.5.

For every (k+1)(k+1)-uniform hypergraph HH whose vertices are the variables XX, the hypergraph formula θ(H)\theta(H) consists of the clauses neg(e{x}){x}\mathrm{neg}(e\setminus\{x\})\cup\{x\} for all hyperedges eHe\in H and all variables xex\in e.

Clearly, for every HH, θ(H)Ψn,k\theta(H)\subseteq\Psi_{n,k} and |θ(H)|=(k+1)|H||\theta(H)|=(k+1)|H|. Considering hypergraph formulas for the upper bound in Theorem 4.4 is restrictive, however, this does not seem to be significant. The lower bound is valid for an arbitrary subset of Ψn,k\Psi_{n,k} and the gap between the lower bound and the upper bound obtained by hypergraph formulas is relatively small.

5 A combinatorial characterization

For simplicity, when considering formulas ucp-equivalent to Ψn,k\Psi_{n,k}, we consider only prime formulas. Since the formula Ψn,k\Psi_{n,k} is equal to the set of its prime implicates, these formulas are subsets of Ψn,k\Psi_{n,k}. We present two combinatorial characterizations of the subsets of Ψn,k\Psi_{n,k} which are ucp-equivalent to Ψn,k\Psi_{n,k}. The first of them is valid for an arbitrary subset of Ψn,k\Psi_{n,k} and is used for a lower bound on the size of prime formulas ucp-equivalent to Ψn,k\Psi_{n,k}. The other characterization is valid for subsets of Ψn,k\Psi_{n,k} in the form of a hypergraph formula θ(H)\theta(H) defined above and is used later for a corresponding upper bound.

Every clause of Ψn,k\Psi_{n,k} contains kk negative literals. It follows that UCP from Ψn,k\Psi_{n,k} and a partial assignment setting less than k1k-1 variables to 11 derives no additional literal. The same is true for every subset of Ψn,k\Psi_{n,k} and, hence, for a characterization of subsets of Ψn,k\Psi_{n,k} which are ucp-equivalent to Ψn,k\Psi_{n,k}, it is sufficient to consider partial assignments setting at least k1k-1 variables to 11.

Definition 5.1.

Assume φΨn,k\varphi\subseteq\Psi_{n,k} and a (k1)(k-1)-set AXA\subseteq X. Let Gd(φ,A)G^{d}(\varphi,A) be the directed graph on XAX\setminus A defined as

Gd(φ,A)={(xi,xj)neg(A){¬xi,xj}φ}.G^{d}(\varphi,A)=\{(x_{i},x_{j})\mid\mathrm{neg}(A)\cup\{\neg x_{i},x_{j}\}\in\varphi\}\;.

This graph represents unit propagation in φ\varphi for partial assignments setting all variables in AA to 11 in the following sense.

Lemma 5.2.

Let φ\varphi and AA be as in Definition 5.1. Assume a partial assignment α\alpha setting all variables in AA to 11 and setting a variable xiXAx_{i}\in X\setminus A to b{0,1}b\in\{0,1\}. Let β\beta be the partial assignment obtained by extending α\alpha by unit propagation in φ\varphi.

  • If b=0b=0, then β\beta extends α\alpha precisely by setting to 00 the variables xjx_{j} such that Gd(φ,A)G^{d}(\varphi,A) contains a path from xjx_{j} to xix_{i}.

  • If b=1b=1, then β\beta extends α\alpha at least by setting to 11 the variables xjx_{j} such that Gd(φ,A)G^{d}(\varphi,A) contains a path from xix_{i} to xjx_{j}.

Proof.

Consider setting all variables in AA to 11. With this partial assignment, the clauses containing a positive literal on a variable from AA become satisfied and, hence, can be removed. Since |A|=k1|A|=k-1, the remaining clauses form a definite Horn formula without unit clauses. In such a formula, setting some of the variables in XAX\setminus A to 00 can derive a value of a new variable by unit propagation only using a clause containing one negative literal. Since the derived value of the variable in this literal is 00, the same is true if the propagation is iterated. If CφC\in\varphi, then setting the variables in AA to 11 in CC produces a clause with one negative literal only if C=neg(A){¬xi,xj}C=\mathrm{neg}(A)\cup\{\neg x_{i},x_{j}\} for some i,ji,j and the resulting clause is {¬xi,xj}\{\neg x_{i},x_{j}\}. Hence, the clauses relevant for propagating assignments of variables in XAX\setminus A to 00 after setting all variables in AA to 11 form the 2-CNF formula

φA={Cneg(A)neg(A)Cφ}.\varphi_{A}=\{C\setminus\mathrm{neg}(A)\mid\mathrm{neg}(A)\subseteq C\in\varphi\}\;. (12)

The clause {¬xi,xj}\{\neg x_{i},x_{j}\} is the same as ¬xixj\neg x_{i}\vee x_{j} and is equivalent to implication xixjx_{i}\to x_{j}. Unit propagation using this implication derives xi=0x_{i}=0, if xj=0x_{j}=0 and the graph Gd(φ,A)G^{d}(\varphi,A) corresponds precisely to implications in φA\varphi_{A}. Setting all variables in XAX\setminus A to 00 is a satisfying assignment of φA\varphi_{A}, so propagating zeros cannot lead to a contradiction. This proves the statement concerning b=0b=0.

The statement concerning b=1b=1 is clear, since φA\varphi_{A} is a subset of the formula obtained from φ\varphi by setting variables in AA to 11 and the clauses of φA\varphi_{A} allow propagation of values 11 along all directed paths in Gd(φ,A)G^{d}(\varphi,A). ∎

Lemma 5.3.

A formula φΨn,k\varphi\subseteq\Psi_{n,k} is ucp-equivalent to Ψn,k\Psi_{n,k} if and only if for every (k1)(k-1)-set AXA\subseteq X the graph Gd(φ,A)G^{d}(\varphi,A) is a strongly connected graph on XAX\setminus A.

Proof.

Let AA be any (k1)(k-1)-subset of XX and let Ψn,k,A\Psi_{n,k,A} be obtained from Ψn,k\Psi_{n,k} by setting the variables in AA to 11. Formula Ψn,k,A\Psi_{n,k,A} contains the clauses ¬xixj\neg x_{i}\vee x_{j} for every xi,xjXAx_{i},x_{j}\in X\setminus A. It follows that unit propagation in Ψn,k,A\Psi_{n,k,A} from a partial assignment setting a variable xjXAx_{j}\in X\setminus A to 00 derives the value 00 for all the remaining variables xiXAx_{i}\in X\setminus A. The resulting assignment is a satisfying assignment of Ψn,k,A\Psi_{n,k,A}, so contradiction is not derived.

Assume, φΨn,k\varphi\subseteq\Psi_{n,k} is ucp-equivalent to Ψn,k\Psi_{n,k}. Since unit propagation in Ψn,k,A\Psi_{n,k,A} derives value 00 for all variables in XAX\setminus A if one of them is set to 00, the same should be true for the formula obtained from φ\varphi by setting the variables in AA to 11. By Lemma 5.2 with b=0b=0, this implies that Gd(φ,A)G^{d}(\varphi,A) contains a path in both directions between any two variables in XAX\setminus A, so it is strongly connected.

Assume that Gd(φ,A)G^{d}(\varphi,A) is strongly connected. Let CΨn,kφC\in\Psi_{n,k}\setminus\varphi and let us prove that any unit propagation step using the clause CC can be replaced by unit propagation in φ\varphi deriving the same literal from the same assumptions. Let lCl\in C and consider a partial assignment α\alpha of the variables falsifying all the literals in C{l}C\setminus\{l\}. We have to show that unit propagation in φ\varphi derives ll from α\alpha.

If ll is positive, let gC{l}g\in C\setminus\{l\} be arbitrary. If ll is negative, let gg be the positive literal contained in CC. For a suitable (k1)(k-1)-set of variables AA, we have C=neg(A){g,l}C=\mathrm{neg}(A)\cup\{g,l\}, gg and ll have the opposite sign, and α\alpha falsifies all the literals in neg(A)\mathrm{neg}(A) and gg. Assume that the variable in gg is xix_{i} and the variable in ll is xjx_{j}. Hence, we have either g=xig=x_{i} and l=¬xjl=\neg x_{j} or g=¬xig=\neg x_{i} and l=xjl=x_{j}. By assumption, Gd(φ,A)G^{d}(\varphi,A) contains paths between xix_{i} and xjx_{j} in both directions. If g=xig=x_{i}, then falsifiying gg means setting xix_{i} to 00 and Lemma 5.2 with b=0b=0 implies that unit propagation derives xj=0x_{j}=0 and, hence, the literal ll. If g=¬xig=\neg x_{i}, then falsifiying gg means setting xix_{i} to 11 and Lemma 5.2 with b=1b=1 implies that unit propagation derives xj=1x_{j}=1 and, hence, the literal ll.

We obtained that unit propagation in φ\varphi from partial assignment α\alpha derives ll. Since this is true for every clause CΨn,kφC\in\Psi_{n,k}\setminus\varphi and for every lCl\in C, φ\varphi is ucp-equivalent to Ψn,k\Psi_{n,k}. ∎

Proposition 5.4.

The size (number of clauses) of a formula ucp-equivalent to Ψn,k\Psi_{n,k} is at least nC(n1,k,k1)n\,C(n-1,k,k-1).

Proof.

Let φ\varphi^{*} be a smallest formula ucp-equivalent to Ψn,k\Psi_{n,k}. Without loss of generality, we can assume that φ\varphi^{*} consists only of prime implicates and, hence, is a subset of Ψn,k\Psi_{n,k}. For every variable xXx\in X, let

𝒮x={Bneg(B)xφ}.\mathcal{S}_{x}=\{B\mid\mathrm{neg}(B)\vee x\in\varphi^{*}\}\;.

For every B𝒮xB\in\mathcal{S}_{x}, we have BX{x}B\subseteq X\setminus\{x\} and |B|=k|B|=k. Let xXx\in X and let AA be an arbitrary (k1)(k-1)-subset of X{x}X\setminus\{x\}. By Lemma 5.3, vertex xx has non-zero in-degree in Gd(φ,A)G^{d}(\varphi^{*},A) and, hence, there is a set B𝒮xB\in\mathcal{S}_{x} such that ABA\subseteq B. It follows that 𝒮x\mathcal{S}_{x} is a system of kk-subsets of an (n1)(n-1)-set covering all (k1)(k-1)-subsets. Hence, |𝒮x|C(n1,k,k1)|\mathcal{S}_{x}|\geq C(n-1,k,k-1) and, since |φ|=xX|𝒮x||\varphi^{*}|=\sum_{x\in X}|\mathcal{S}_{x}|, the statement follows. ∎

For analysis of the formulas θ(H)\theta(H) we use the following notion.

Definition 5.5.

We say that a (k+1)(k+1)-uniform hypergraph HH on the set of vertices XX has connected restrictions, if for every (k1)(k-1)-set AXA\subseteq X, the graph

G(H,A)={eAAeH}G(H,A)=\{e\setminus A\mid A\subseteq e\in H\} (13)

is a connected graph on the set XAX\setminus A.

Proposition 5.6.

If HH is (k+1)(k+1)-uniform hypergraph on XX, then θ(H)\theta(H) is ucp-equivalent to Ψn,k\Psi_{n,k} if and only if HH has connected restrictions.

Proof.

Since θ(H)\theta(H) is a subset of Ψn,k\Psi_{n,k}, we can use the characterization of formulas ucp-equivalent to Ψn,k\Psi_{n,k} from Lemma 5.3.

Let AA be an arbitrary (k1)(k-1)-subset of XX. If Gd(θ(H),A)G^{d}(\theta(H),A) contains the directed edge (xi,xj)(x_{i},x_{j}), then it also contains the directed edge (xj,xi)(x_{j},x_{i}). Moreover, these two edges are contained in Gd(θ(H),A)G^{d}(\theta(H),A) if and only if G(H,A)G(H,A) contains the undirected edge {xi,xj}\{x_{i},x_{j}\}. Hence, Gd(θ(H),A)G^{d}(\theta(H),A) is strongly connected if and only if G(H,A)G(H,A) is connected. Since this is satisfied for arbitrary (k1)(k-1)-subset AXA\subseteq X, θ(H)\theta(H) satisfies the condition from Lemma 5.3 if and only if HH has connected restrictions. ∎

Note that Ψn,k=θ(H0)\Psi_{n,k}=\theta(H_{0}), where H0H_{0} is the complete (k+1)(k+1)-uniform hypergraph. The ucp-irredundant formula φ\varphi^{\ell} can be obtained as follows.

Definition 5.7.

Let H1H_{1} consist of all (k+1)(k+1)-subsets of XX containing the variable x1x_{1} and let φ=θ(H1)\varphi^{\ell}=\theta(H_{1}).

In particular, H1H_{1} has connected restrictions, since for every (k1)(k-1)-set AA not containing x1x_{1}, the graph G(H1,A)G(H_{1},A) is a star on XAX\setminus A whose central vertex is x1x_{1}. If x1Ax_{1}\in A, then G(H1,A)G(H_{1},A) is a complete graph on XAX\setminus A.

Proposition 5.8.

Formula φ\varphi^{\ell} is ucp-irredundant and ucp-equivalent to Ψn,k\Psi_{n,k}.

Proof.

As mentioned above, H1H_{1} has connected restrictions. It follows that φ\varphi^{\ell} is ucp-equivalent to Ψn,k\Psi_{n,k} by Proposition 5.6. Let us prove that it is ucp-irredundant. For this purpose, let CφC\in\varphi^{\ell} be arbitrary and let us prove that φ{C}\varphi^{\ell}\setminus\{C\} is not ucp-equivalent to Ψn,k\Psi_{n,k}. Let VV be the set of variables used in CC except of x1x_{1}, so we have |V|=k|V|=k. Let α\alpha be the partial assignment of the variables in VV such that all literals on variables from VV in CC are falsified. The clause CC together with α\alpha derives a value of x1x_{1} which makes the literal on x1x_{1} in CC satisfied. Since CC is an implicate of Ψn,k\Psi_{n,k}, every formula ucp-equivalent to Ψn,k\Psi_{n,k} should derive the same value of x1x_{1} as CC. The proof will be finished by proving that φ{C}\varphi^{\ell}\setminus\{C\} does not satisfy this.

Depending on whether CC contains the literal x1x_{1} or ¬x1\neg x_{1}, the partial assignment α\alpha assigns all variables in VV the value 11 or all variables in VV are assigned the value 11 except of one which is assigned 00. In both cases, the following is true. Every clause DD in φ{C}\varphi^{\ell}\setminus\{C\} on the same set of variables as CC is satisfied by α\alpha, since two of the variables in CC have different sign in CC and DD. At least one of them is not x1x_{1} and the literal with this variable is satisfied in DD. Every clause in φ{C}\varphi^{\ell}\setminus\{C\} on a set of variables different from the set of variables of CC contains at least two variables not assigned by α\alpha, namely x1x_{1} and some variable not in V{x1}V\cup\{x_{1}\} and, hence, cannot be used for unit propagation. It follows that unit propagation in φ{C}\varphi^{\ell}\setminus\{C\} from the assignment α\alpha does not derive a value of any new variable, in particular, a value of x1x_{1}. ∎

Construction of a hypergraph HH such that the size of θ(H)\theta(H) is a good upper bound on the size of φ\varphi^{*} is more complicated and we use results proven in the next two sections for this purpose.

6 Random permutations of a graph or hypergraph

The purpose of this section is to prove that a union of independent permutations of several graphs without isolated vertices is connected with high probability. This is an auxiliary result used in the next section to prove that union of several independent random permutations of a (k+1)(k+1)-uniform hypergraph which covers all kk-subsets is a hypergraph with connected restrictions with high probability.

Definition 6.1.

Let HH be a hypergraph on a set of vertices VV. Consider a permutation π:VV\pi:V\to V. We denote by π(H)\pi(H) the hypergraph on the set of vertices VV such that for every set eVe\subseteq V, π(e)\pi(e) is a hyperedge of π(H)\pi(H) is and only if ee is a hyperedge of HH.

Intuitively, hypergraph π(H)\pi(H) is obtained by moving each vertex uu of HH to π(u)\pi(u) and moving the edges correspondingly. By a random permutation of HH, we mean π(H)\pi(H), where π\pi is chosen at random from the uniform distribution on permutations of VV.

The following lemma is an anticoncentration inequality for the sum of independent variables XiX_{i} such that the distribution of XiX_{i} is uniform on {0,ai}\{0,a_{i}\} where ai2a_{i}\geq 2 are integers. For technical reasons, it is formulated using counts instead of probabilities.

Lemma 6.2 ([19]).

Assume integers ai2a_{i}\geq 2 for i=1,,ri=1,\ldots,r and let m=i=1raim=\sum_{i=1}^{r}a_{i}. Then for every 2dm/22\leq d\leq m/2, the number of sets I{1,,r}I\subseteq\{1,\ldots,r\}, such that

iIai=d\sum_{i\in I}a_{i}=d (14)

is at most

(m/2d/2).{\lfloor m/2\rfloor\choose\lfloor d/2\rfloor}\;.
Proof.

The sets II satisfying (14) are pairwise incomparable and have size at most d/2\lfloor d/2\rfloor. Let cjc_{j} for j=1,,d/2j=1,\ldots,\lfloor d/2\rfloor be the number of these sets of size jj. By LYM inequality [13], we have

j=1d/2cj(rj)1.\sum_{j=1}^{\lfloor d/2\rfloor}\frac{c_{j}}{{r\choose j}}\leq 1\;.

Since rm/2r\leq\lfloor m/2\rfloor, we have also

j=1d/2cj(m/2j)1\sum_{j=1}^{\lfloor d/2\rfloor}\frac{c_{j}}{{\lfloor m/2\rfloor\choose j}}\leq 1

and, since d/2m/2/2\lfloor d/2\rfloor\leq\lfloor m/2\rfloor/2, this implies that the number of sets II satisfying (14) is at most

j=1d/2cj(m/2d/2)\sum_{j=1}^{\lfloor d/2\rfloor}c_{j}\leq{\lfloor m/2\rfloor\choose\lfloor d/2\rfloor}

as required. ∎

Let G=(V,E)G=(V,E) be an undirected graph. For a permutation π:VV\pi:V\to V, we define π(G)\pi(G) in the same way as for a hypergraph. Namely, for every pair of distinct vertices u,vVu,v\in V, {π(u),π(v)}\{\pi(u),\pi(v)\} is an edge of π(G)\pi(G) if and only if {u,v}\{u,v\} is an edge of GG.

Lemma 6.3.

Assume a set YY of size mm and let GG be a graph on YY with no isolated vertices. Let AYA\subseteq Y, and let 2d=|A|m/22\leq d=|A|\leq m/2. The probability that a random permutation of GG has no edge connecting AA and YAY\setminus A is at most

(m/2d/2)(md)1{\lfloor m/2\rfloor\choose\lfloor d/2\rfloor}{m\choose d}^{-1}
Proof.

Consider a random permutation π\pi of the vertices of GG. Graph π(G)\pi(G) has no edge between AA and YAY\setminus A if and only if the preimage π1(A)\pi^{-1}(A) is a union of connected components of GG. The preimages π1(A)\pi^{-1}(A) are uniformly distributed over subsets of YY of size dd. The number of subsets of YY of size dd that are a union of connected components in GG is equal to the number of solutions of the equation (14) where rr is the number of connected components of GG and aia_{i} are their sizes. Since GG has no isolated vertices, we have ai2a_{i}\geq 2 for i=1,,ri=1,\ldots,r and, hence, the lemma follows from Lemma 6.2. ∎

Proposition 6.4.

Let G1,,GsG_{1},\ldots,G_{s}, s3s\geq 3, be graphs on the same set of mm vertices each of which has no isolated vertices. If ss is fixed and mm tends to infinity, then the probability that the union of independent random permutations of G1,,GsG_{1},\ldots,G_{s} is not a connected graph is at most O(m2s)O(m^{2-s}).

Proof.

Let YY be the common set of vertices of the graphs. The probability of the event that the union of independent permutations of G1,,GsG_{1},\ldots,G_{s} is not a connected graph is at most the sum of the probabilities over subsets AYA\subseteq Y of size between 22 and m/2m/2 of the event that the union contains no edge between AA and YAY\setminus A. Using d=|A|d=|A| as a summation index and using Lemma 6.3, this is at most

d=2m/2pd\sum_{d=2}^{\lfloor m/2\rfloor}p_{d}

where

pd=(m/2d/2)s(md)1s.p_{d}={\lfloor m/2\rfloor\choose\lfloor d/2\rfloor}^{s}{m\choose d}^{1-s}\;. (15)

For a few smallest values of dd, the following simple estimate is sufficient. If dd and ss are fixed and mm\to\infty, we have

pd=O(md(1s/2)).p_{d}=O\left(m^{d(1-s/2)}\right)\;. (16)

For larger values of dd, we estimate pdp_{d} using more precise bounds on binomial coefficients. Denote

b(t,d)=(td)d(ttd)td=etH(d/t)b(t,d)=\left(\frac{t}{d}\right)^{d}\left(\frac{t}{t-d}\right)^{t-d}=\mathrm{e}^{t\mathrm{H}(d/t)}

where H(x)=xlnx(1x)ln(1x)\mathrm{H}(x)=-x\ln x-(1-x)\ln(1-x) is the entropy function. Since H(x)\mathrm{H}(x) is increasing for 0x1/20\leq x\leq 1/2, b(t,d)b(t,d) is increasing in dd if tt is fixed and 1dt/21\leq d\leq t/2. Since H(x)\mathrm{H}(x) is strictly concave, H(x)/x\mathrm{H}(x)/x is decreasing for 0<x10<x\leq 1 and, hence, b(t,d)b(t,d) is increasing in tt if dd is fixed. By a well-known upper bound on binomial coefficients and using dm/2d\leq\lfloor m/2\rfloor, we get

(m/2d/2)b(m/2,d/2)b(m/2,d/2)=b(m,d)1/2.{\lfloor m/2\rfloor\choose\lfloor d/2\rfloor}\leq b(\lfloor m/2\rfloor,\lfloor d/2\rfloor)\leq b(m/2,d/2)=b(m,d)^{1/2}\;.

By a well-known lower bound on binomial coefficients, we have

1m+1b(m,d)(md).\frac{1}{m+1}b(m,d)\leq{m\choose d}\;.

Using these bounds and (15), we obtain

pd(m+1)s1b(m,d)1s/2.p_{d}\leq(m+1)^{s-1}b(m,d)^{1-s/2}\;. (17)

Choose a fixed integer d04(s1)/(s2)d_{0}\geq 4(s-1)/(s-2). By (16) we have

d=2d01pd=O(m2s).\sum_{d=2}^{d_{0}-1}p_{d}=O(m^{2-s})\;. (18)

If d0dm/2d_{0}\leq d\leq m/2, then b(m,d)b(m,d0)(m/d0)d0b(m,d)\geq b(m,d_{0})\geq(m/d_{0})^{d_{0}} and by (17)

pd(m+1)s1(m/d0)d0(1s/2)=O(m1s).p_{d}\leq(m+1)^{s-1}(m/d_{0})^{d_{0}(1-s/2)}=O(m^{1-s})\;.

Together with (18), we obtain

d=2m/2pd=O(m2s)\sum_{d=2}^{\lfloor m/2\rfloor}p_{d}=O(m^{2-s}) (19)

and the proof is finished. ∎

7 Size of a hypergraph with connected restrictions

In this section, we prove an upper bound on the minimum size of a hypergraph with connected restrictions using covering numbers.

Proposition 7.1.

For every large enough nn and k=n/2+O(1)k=n/2+O(1), there is a (k+1)(k+1)-uniform hypergraph on nn vertices of size at most 6C(n,k+1,k)6\,C(n,k+1,k) with connected restrictions.

Proof.

Let |X|=n|X|=n and let HH be a (k+1)(k+1)-uniform hypergraph of size C(n,k+1,k)C(n,k+1,k) covering all kk-subsets of XX. Let s=5s=5 and consider independent random permutations π1,,πs\pi_{1},\ldots,\pi_{s} of XX chosen from the uniform distribution and let H=π1(H)πs(H)H^{*}=\pi_{1}(H)\cup\ldots\cup\pi_{s}(H).

If AA is a (k1)(k-1)-subset of XX and π\pi is a permutation of XX, then the graph G(π(H),A)G(\pi(H),A) has no isolated vertices, however, for different permutations π\pi, the graphs G(π(H),A)G(\pi(H),A) are not, in general, permutations of the same graph on XAX\setminus A. In order to overcome this, we partition the probability space of all ss-tuples of permutations of XX by a set of mutually exclusive conditions such that the conditional distribution of the ss-tuple of graphs G(πi(H),A)G(\pi_{i}(H),A), i=1,,si=1,\ldots,s under any of these conditions satisfies the assumption of Proposition 6.4. Namely, for an arbitrary ss-tuple (A1,,As)(A_{1}^{\prime},\ldots,A_{s}^{\prime}) of (k1)(k-1)-subsets of XX consider the condition πi(Ai)=A\pi_{i}(A_{i}^{\prime})=A for every i=1,,si=1,\ldots,s. Clearly, these conditions have the same probability for all ss-tuples of (k1)(k-1)-subsets AiA_{i}^{\prime} and represent a partition of the probability space.

Fix an arbitrary ss-tuple (A1,,As)(A_{1}^{\prime},\ldots,A_{s}^{\prime}) and consider the corresponding conditional distribution. For a fixed ii and all permutations πi\pi_{i} satisfying πi(Ai)=A\pi_{i}(A_{i}^{\prime})=A, the graphs G(πi(H),A)G(\pi_{i}(H),A) are isomorphic. Choose any of them as GiG_{i}. The distribution of G(πi(H),A)G(\pi_{i}(H),A) is the same as random permutations of GiG_{i}. Moreover, these permutations are independent for i=1,,si=1,\ldots,s. Hence, we can use Proposition 6.4 to obtain that G(H,A)G(H^{*},A) is not connected with probability at most O((nk+1)2s)O((n-k+1)^{2-s}) under any of the considered conditions and, hence, also unconditionally.

A (k1)(k-1)-set AA is called “bad”, if the graph G(H,A)G(H^{*},A) is not connected and let tt be the random variable equal to the number of such sets. By the argument above, we have

𝐄t=O((nk+1)2s)(nk1).\mathbf{E}\;t=O\left((n-k+1)^{2-s}\right){n\choose k-1}\;. (20)

For each of the tt “bad” sets AA, we add several (k+1)(k+1)-sets to HH^{*} to make G(H,A)G(H^{*},A) connected. The number of (k+1)(k+1)-sets needed for this is at most the number of the connected components G(H,A)G(H^{*},A) minus 11 which is at most (nk)/2(n-k)/2. Hence, the resulting (k+1)(k+1)-uniform hypergraph HH^{**} has size at most s|H|+t(nk)/2s|H|+t(n-k)/2. By (20), there is a choice of permutations πi\pi_{i} for i=1,,si=1,\ldots,s, such that

tO((nk+1)2s)(nk1)O((nk+1)2s)(nk)t\leq O\left((n-k+1)^{2-s}\right){n\choose k-1}\leq O\left((n-k+1)^{2-s}\right){n\choose k}

Since nk=Θ(k)n-k=\Theta(k), we can conclude

|H|s|H|+O(k3s)(nk).|H^{**}|\leq s|H|+O\left(k^{3-s}\right){n\choose k}\;.

Using (1) and s=5s=5, we get

|H|(s+1)|H|6C(n,k+1,k)|H^{**}|\leq(s+1)|H|\leq 6\,C(n,k+1,k)

if nn and, hence, also kk are sufficiently large. This finishes the proof, since HH^{**} has connected restrictions. ∎

8 Proof of the results

In this section, we summarize the results of the previous sections. First, we finish the proof of Theorem 4.4 which presents a lower and an upper bound on the size of a smallest formula ucp-equivalent to Ψn,k\Psi_{n,k} needed for the proof of the main result.

Proof of Theorem 4.4.

The lower bound is Proposition 5.4. For the upper bound, consider a hypergraph HH of size at most 6C(n,k+1,k)6\,C(n,k+1,k) with connected restrictions guaranteed by Proposition 7.1. By Proposition 5.6, θ(H)\theta(H) is ucp-equivalent to Ψn,k\Psi_{n,k} and its size is (k+1)|H|(k+1)|H|. It follows that the size of a smallest formula ucp-equivalent to Ψn,k\Psi_{n,k} is at most 6(k+1)C(n,k+1,k)6\,(k+1)C(n,k+1,k). Using (2) and the bound (5) or (7), we obtain the required asymptotic estimate. ∎

The main result is Theorem 4.1 providing an almost linear separation between the size of a specific ucp-irredundant formula ucp-equivalent to Ψn,k\Psi_{n,k} and a smallest such formula.

Proof of Theorem 4.1.

Let φ\varphi^{\ell} be the formula defined in Section 5. This formula is an irredundant PC formula equivalent to Ψn,k\Psi_{n,k} by Proposition 5.8 and its size is

|φ|=(k+1)(n1k)=(k+1)(1kn)(nk)=Ω(n)(nk).|\varphi^{\ell}|=(k+1){n-1\choose k}=(k+1)\left(1-\frac{k}{n}\right){n\choose k}=\Omega(n){n\choose k}\;.

Let φ\varphi^{*} be a smallest formula ucp-equivalent to Ψn,k\Psi_{n,k}. The statement follows by comparing the lower bound on |φ||\varphi^{\ell}| and the upper bound on |φ||\varphi^{*}| implied by Theorem 4.4. ∎

Let us include an observation concerning the difference between the lower and the upper bound in Theorem 4.4. The following proposition implies that there is an infinite set of pairs (n,k)(n,k) satisfying k=n/2+O(1)k=n/2+O(1) for which this lower and upper bound differ at most by a multiplicative constant. It remains open whether this is true for all pairs (n,k)(n,k) satisfying k=n/2+O(1)k=n/2+O(1).

Proposition 8.1.

Let aa\in\mathbb{Z}. We have 1μ(n,k)/μ(n1,k1)31\leq\mu(n,k)/\mu(n-1,k-1)\leq 3 for infinitely many k2k\geq 2 and n=2k+an=2k+a.

Proof.

By (8), we have 1μ(n,k)/μ(n1,k1)1\leq\mu(n,k)/\mu(n-1,k-1). Assume for a contradiction that for some k02k_{0}\geq 2 and every kk0k\geq k_{0} and n=2k+an=2k+a, we have μ(n,k)/μ(n1,k1)>3\mu(n,k)/\mu(n-1,k-1)>3. Let P={(n,k)kk0,n=2k+a}P=\{(n,k)\mid k\geq k_{0},n=2k+a\}. By (9), the pairs (n,k)P(n,k)\in P satisfy

μ(n+1,k)μ(n,k)k+a+12k+a+1=12+o(1)\frac{\mu(n+1,k)}{\mu(n,k)}\geq\frac{k+a+1}{2k+a+1}=\frac{1}{2}+o(1)

and since (n+2,k+1)P(n+2,k+1)\in P, we have

μ(n+2,k+1)μ(n+1,k)>3\frac{\mu(n+2,k+1)}{\mu(n+1,k)}>3

implying

μ(n+2,k+1)μ(n,k)32+o(1).\frac{\mu(n+2,k+1)}{\mu(n,k)}\geq\frac{3}{2}+o(1)\;.

It follows that μ(n,k)\mu(n,k) grows exponentially with kk for pairs (n,k)P(n,k)\in P which contradicts the bound μ(n,k)=O(lnn)\mu(n,k)=O(\ln n). ∎

9 Conclusion and further research

The paper shows that a general upper bound on the ratio of the size of a ucp-irredundant formula and the size of a smallest ucp-equivalent formula is at most n2n^{2} (Proposition 3.3) and at least Ω(n/lnn)\Omega(n/\ln n) (Theorem 4.1). The gap between these bounds is quite large. An interesting open problem for further research is to reduce this gap.

The lower and the upper bound on the size of a smallest formula ucp-equivalent to Ψn,k\Psi_{n,k} in Theorem 4.4 differ by a factor Θ(μ(n,k)/μ(n1,k1))\Theta(\mu(n,k)/\mu(n-1,k-1)). Is this factor bounded by a constant for every k2k\geq 2 and n=2k+an=2k+a if aa\in\mathbb{Z} is fixed?

Acknowledgement. The author would like to thank Diana Piguet for a fruitful discussion on using hypergraphs, in particular, for suggesting Definition 4.5, and Matas Šileikis for suggesting Lemma 6.2 which improves a slightly weaker bound on the same quantity by the author. The author acknowledges institutional support RVO:67985807.

References

  • [1] K. Bérczi, E. Boros, and K. Makino. Hypergraph Horn functions. arXiv:2301.05461, 2023.
  • [2] K. Bérczi, E. Boros, and K. Makino. Matroid Horn functions. arXiv:2301.06642, 2023.
  • [3] Ch. Bessiere, G. Katsirelos, N. Narodytska, and T. Walsh. Circuit complexity and decompositions of global constraints. In Proceedings of the Twenty-First International Joint Conference on Artificial Intelligence (IJCAI-09), pages 412–418, 2009.
  • [4] M. L. Bonet, S. Buss, A. Ignatiev, J. Marques-Silva, and A. Morgado. MaxSAT resolution with the dual rail encoding. In Thirty-Second AAAI Conference on Artificial Intelligence, 2018.
  • [5] L. Bordeaux and J. Marques-Silva. Knowledge compilation with empowerment. In SOFSEM 2012, volume 7147 of Lecture Notes in Computer Science, pages 612–624. Springer, 2012.
  • [6] R. E. Bryant, D. Beatty, K. Brace, K. Cho, and T. Sheffler. COSMOS: A compiled simulator for MOS circuits. In Proceedings of the 24th ACM/IEEE Design Automation Conference, DAC ’87, page 9–16, New York, NY, USA, 1987. Association for Computing Machinery.
  • [7] P. Erdős and J. Spencer. Probabilistic methods in combinatorics. Akademiai Kiado-Budapest, 1974.
  • [8] P. Frankl and V. Rödl. Lower bounds for Turán’s problem. Graphs and Combinatorics, 1:213––216, 1985.
  • [9] D. M. Gordon, O. Pataschnik, and G. Kuperberg. New constructions for covering designs. Journal of Combinatorial Designs, 3(4):269–284, 1995.
  • [10] P. L. Hammer and A. Kogan. Optimal compression of propositional horn knowledge bases: Complexity and approximation. Artificial Intelligence, 64(1):131–145, 1993.
  • [11] A. Ignatiev, A. Morgado, and J. Marques-Silva. On tackling the limits of resolution in SAT solving. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing – SAT 2017, pages 164–183. Springer International Publishing, 2017.
  • [12] P. Kučera and P. Savický. Bounds on the size of PC and URC formulas. Journal of Artificial Intelligence Research, 69:1395–1420, 2020.
  • [13] D. Lubell. A short proof of Sperner’s lemma. Journal of Combinatorial Theory, 1(2):299, 1966.
  • [14] V. M. Manquinho, P. F. Flores, J. P. M. Silva, and A. L. Oliveira. Prime implicant computation using satisfiability algorithms. In Proceedings Ninth IEEE International Conference on Tools with Artificial Intelligence, pages 232–239, Nov 1997.
  • [15] A. Morgado, A. Ignatiev, M. L. Bonet, J. Marques-Silva, and S. Buss. DRMaxSAT with MaxHS: First contact. In International Conference on Theory and Applications of Satisfiability Testing, pages 239–249. Springer, 2019.
  • [16] V. Rödl. On a packing and covering problem. European Journal of Combinatorics, 6(1):69–78, 1985.
  • [17] J. Schönheim. On coverings. Pacific Journal of Mathematics, 14(4):1405–1411, 1964.
  • [18] A. F. Sidorenko. Upper bounds for Turán numbers. Journal of Combinatorial theory, Series A, 77(1):134–147, 1997.
  • [19] Matas Šileikis. Personal communication, 2023.