A lower bound on CNF encodings of the at-most-one constraint

TL;DR

This paper establishes a near-tight lower bound on the size of propagation complete CNF encodings for the at-most-one constraint, crucial for efficient problem translation in SAT solving.

Contribution

It provides the first lower bound on clause size for propagation complete encodings of the at-most-one constraint, nearly matching existing best encodings.

Findings

Lower bound nearly matches the size of known encodings

Slightly improved lower bounds for 2-CNF encodings

Bounds also apply to the exactly-one constraint

Abstract

Constraint "at most one" is a basic cardinality constraint which requires that at most one of its $n$ boolean inputs is set to $1$. This constraint is widely used when translating a problem into a conjunctive normal form (CNF) and we investigate its CNF encodings suitable for this purpose. An encoding differs from a CNF representation of a function in that it can use auxiliary variables. We are especially interested in propagation complete encodings which have the property that unit propagation is strong enough to enforce consistency on input variables. We show a lower bound on the number of clauses in any propagation complete encoding of the "at most one" constraint. The lower bound almost matches the size of the best known encodings. We also study an important case of 2-CNF encodings where we show a slightly better lower bound. The lower bound holds also for a related "exactly one" constraint.

Equations

$$f(\alpha )=1⟺(\exists \beta \in {\{0,1\}}^{\ell })\phi (\alpha ,\beta )=1\text{.}$$

$$f(\mathbf{x})\wedge \underset{i=1}{\overset{p}{\bigwedge }}{g}_i\models h$$

$$\phi \wedge \underset{i=1}{\overset{p}{\bigwedge }}{g}_i{⊢}_{1}h\text{or}\phi \wedge \underset{i=1}{\overset{p}{\bigwedge }}{g}_i{⊢}_1\perp \text{.}$$

$${\mathcal{U}}_{\phi }(g_1,\dots ,g_k)=\left\{h\mid \phi \wedge \underset{i=1}{\overset{k}{\bigwedge }}{g}_i{⊢}_{1}h\right\}.$$

$$Q_{\phi ,i}=\{C\in \phi |\neg x_i\in C\}\text{.}$$

$$|\phi |\ge |{\phi }^{\prime }|+3\ge \min (2n,3n-6)\text{.}$$

$${\phi }_3^s(x_1,x_2,x_3)=(\neg x_1\vee \neg x_2)\wedge (\neg x_1\vee \neg x_3)\wedge (\neg x_2\vee \neg x_3)$$

$${\phi }_n^s(x_1,\dots ,x_n)=(\neg x_1\vee \neg x_2)\wedge (\neg x_1\vee y)\wedge (\neg x_2\vee y)\wedge {\phi }_{n-1}^s(y,x_3,\dots ,x_n)$$

$${\phi }_3^t(x_1,x_2,x_3)={\phi }_3^s(x_1,x_2,x_3)$$

$${\phi }_n^t(x_1,\dots ,x_n)=(\neg x_1\vee \neg x_2)\wedge (\neg x_1\vee y)\wedge (\neg x_2\vee y)\wedge {\phi }_{n-1}^t(x_3,\dots ,x_n,y)$$

$${\phi }_3^p(x_1,x_2,x_3)={\phi }_3^s(x_1,x_2,x_3)$$

$$(\neg x_1\vee \neg x_2)\wedge (\neg x_1\vee y)\wedge (\neg x_2\vee y)\wedge {\phi }_{n-1}^p(y,x_3,\dots ,x_n)$$

$$\underset{i=1}{\overset{n}{\bigwedge }}(\neg x_i\vee y_{r(i)})\wedge \underset{i=1}{\overset{n}{\bigwedge }}(\neg x_i\vee z_{c(i)})\wedge {\phi }_{m_1}^p(\mathbf{y})\wedge {\phi }_{m_2}^p(\mathbf{z})$$

$$|{\phi }_n^p|\le 3n-6.$$

$$|{\phi }_n^p|\le 2n+2|{\phi }_m^p|\text{.}$$

$$|{\phi }_n^p|\le 2n+O(\sqrt{n})\text{.}$$

$$|{\phi }_n^p|\le 2n+4\sqrt{n}+O(\sqrt[4]{n})$$

$${\phi }^{\prime }=(x_1\vee \dots \vee x_{n-2}\vee x_n\vee y)\wedge (x_{n-1}\vee x_n\vee \neg y)\wedge \phi (\mathbf{x})$$

$$\begin{array}[]{c}\mathcal{P}(n)\leq|\varphi_{1}|\leq\mathcal{P}(n)+1\\ \mathcal{P}(n)\leq|\varphi_{2}|\leq\mathcal{P}(n)+1\end{array}$$

$$(\neg x_1\vee z)\wedge \phi (z,x_2,\dots ,x_n,\mathbf{y})$$

$$(x_1\vee \dots \vee x_n)\wedge \phi (\mathbf{x},\mathbf{y})$$

$$\phi {⊢}_{1}h⟹\phi [g_1\leftarrow g_2]{⊢}_{1}h\text{.}$$

$$t(e)=\{\begin{array}{ll}e& \text{if var(e)=var(g1)}\\ g_2& \text{if e=g1}\\ \neg g_2& \text{if e=¬g1.}\end{array}$$

$$C_i\in \phi$$

$$C_i\notin \phi$$

$$|\phi |\ge |\psi |+2\text{.}$$

$$|\phi |\ge |\psi |+2\ge |{\phi }^{\prime }|+3$$

$$Q_{\phi ,i}=\{C_1=\neg x_i\vee y,C_2=\neg x_i\vee z_1\vee \dots \vee z_{\ell }\}$$

$$\phi \wedge x_i/{⊢}_1\neg z_j$$

$$\phi \wedge y/{⊢}_1\neg z_j\text{.}$$

$${\mathcal{U}}_{\phi }(x_i)={\mathcal{U}}_{\phi }(y)\cup \{x_i\}$$

Full text

1 Introduction

In this paper we study the properties of one of the most basic cardinality constraints — the “at most one” constraint on $n$ boolean variables which requires that at most one input variable is set to $1$. This constraint is widely used when translating a problem into a conjunctive normal form (CNF). Since the “at most one” constraint is anti-monotone, it has a unique minimal prime CNF representation which requires $\binom{n}{2}=\Theta(n^{2})$ negative clauses, where $n$ is the number of input variables. However, there are CNF encodings of size $O(n)$ which use additional auxiliary variables. Several encodings for this constraint were considered in the literature. Let us mention sequential encoding [21] which addresses also more general cardinality constraints. The same encoding was also called ladder encoding in [17], and it forms the smallest variant of the commander-variable encodings [18]. After a minor simplification, it requires $3n-6$ clauses and $n-3$ auxiliary variables. Similar, but not smaller encodings can also be obtained as special cases of totalizers [5] and cardinality networks [1]. Currently the smallest known encoding is the product encoding introduced by Chen [10]. It consists of $2n+4\sqrt{n}+O(\sqrt[4]{n})$ clauses and uses $O(\sqrt{n})$ auxiliary variables. The sequential and the product encodings are described in Section 3.1 and Section 3.2 with some modifications. It is worth noting that the product encoding can be derived using the monotone circuit of size $kn+o(n)$ for the function $T^{n}_{k}$ described in [14] and in [22], if $k=2$. Section 3.3 provides more detail on this.

Other encodings introduced in the literature for the “at most one” constraint use more clauses than either sequential or product encoding does. These include the binary encoding [6, 16] and the bimander encoding [17].

All the encodings for the “at most one” constraint we have mentioned are in the form of a 2-CNF formula which is a CNF formula where all clauses consist of at most two literals. This restricted structure guarantees that the encodings are propagation complete. The notion of propagation completeness was introduced by [8] as a generalization of unit refutation completeness introduced by [13]. We say that a formula $\varphi$ is propagation complete if for any set of literals $e_{i},\;i\in I$, the following property holds: either $\varphi\wedge\bigwedge_{i\in I}e_{i}$ is contradictory and this can be detected by unit propagation, or unit propagation started with $\varphi\wedge\bigwedge_{i\in I}e_{i}$ derives all literals $g$ that logically follow from this formula. It was shown in [3] that a prime 2-CNF formula is always propagation complete. Since unit propagation is a standard tool used in state-of-the-art SAT solvers [7], this makes 2-CNF formulas as a part of a larger instance simple for them.

When encoding a constraint into a CNF formula, a weaker condition than propagation completeness of the resulting formula is often required. Namely, we require that unit propagation on the encoding is strong enough to enforce some kind of local consistency, for instance generalized arc consistency (GAC), see for example [4]. In this case we only care about propagation completeness with respect to input variables and not necessarily about behaviour on auxiliary variables. Later we formalize this notion as propagation complete encoding (PC encoding). Let us note that this name was also used in [9] to denote an encoding of a given constraint which is propagation complete with respect to all variables including the auxiliary ones.

Chen [10] conjectures that the product encoding is the smallest possible PC encoding of the “at most one” constraint. In this paper we provide support for the positive answer to this conjecture. Our lower bound almost matches the size of the product encoding. We show that any propagation complete encoding of the “at most one” constraint on $n$ variables requires at least $2n+\sqrt{n}-O(1)$ clauses. The lower bound actually holds for a related constraint “exactly one” as well. We also consider the important special case of 2-CNF encodings for which we achieve a better lower bound, namely, any 2-CNF encoding of the “at most one” constraint on $n$ variables requires at least $2n+2\sqrt{n}-O(1)$ clauses.

We should note that having a smaller encoding is not necessarily an advantage when a SAT solver is about to be used. Adding auxiliary variables can be costly because the SAT solver has to deal with them and possibly use them for decisions. However, encodings using auxiliary variables can be useful for constraints whose CNF representation is too large. Moreover, the experimental results in [20] suggest that a SAT solver can be modified to minimize the disadvantage of introducing auxiliary variables. Another experimental evaluation of various cardinality constraints and their encodings appears in [15]. A propagation complete encoding can also be used as a part of a general purpose CSP solver where unit propagation can serve as a propagator of GAC, see [4].

The paper is organized as follows. In Section 2, we give the necessary definitions and formulate the main result in Theorem 2.8. In particular, we introduce the notion of a P-encoding that captures the common properties of propagation complete encodings of the “at most one” and the “exactly one” constraints used for the lower bounds. Moreover, we define a specific form of a P-encoding which we call a regular form and formulate Theorem 2.10 that is the basis of the proofs of the lower bounds by considering separately the encodings in the regular form and the encodings not in this form. We also prove that Theorem 2.10 is sufficient for the lower bound $2n$ on the size of the considered encodings. In Section 3, we recall the known results and present some auxiliary results we use in the rest of the paper. In Section 4, we prove the properties of the encodings not in the regular form that imply Theorem 2.10. Section 5 contains the proof of a lower bound $2n+\sqrt{n}-O(1)$ on the size of any propagation complete encoding of the “at most one” and the “exactly one” constraints obtained by analysis of the encodings in the regular form. In Section 6 we prove a lower bound $2n+2\sqrt{n}-O(1)$ on the size of 2-CNF encodings of the “at most one” constraint by a different analysis of the encodings in the regular form. We close the paper with notes on possible directions for further research in Section 7 and concluding remarks in Section 8.

A preliminary version of this paper appeared in [19]. Due to page limitations, several proofs were omitted or only sketched in the conference version. In this version of the paper, we have included all proofs and improved their readability. The lower bounds were slightly improved since the conference version as well.

2 Definitions and Results

In this section we introduce the notions used throughout the paper, state the main results and give an overview of their proof. We use $\subset$ to denote strict inclusion.

2.1 At-Most-One and Exactly-One Functions

In this paper we are interested in two special cases of cardinality constraints represented by “at most one” and “exactly one” functions. These functions differ only on the zero input.

Definition 2.1**.**

For every $n\geq 1$, the function $\operatorname{\mathrm{AMO}}_{n}(x_{1},\dots,x_{n})$ (at most one) is defined as follows: Given an assignment $\alpha:\{x_{1},\ldots,x_{n}\}\to\{0,1\}$, the value $\operatorname{\mathrm{AMO}}_{n}(\alpha)$ is $1$ if and only if there is at most one index $i\in\{1,\dots,n\}$ for which $\alpha(x_{i})=1$.

Definition 2.2**.**

For every $n\geq 1$, the function $\operatorname{\mathrm{EO}}_{n}(x_{1},\dots,x_{n})$ (exactly one) is defined as follows: Given an assignment $\alpha:\{x_{1},\ldots,x_{n}\}\to\{0,1\}$, the value $\operatorname{\mathrm{EO}}_{n}(\alpha)$ is $1$ if and only if there is exactly one index $i\in\{1,\dots,n\}$ for which $\alpha(x_{i})=1$.

We study propagation complete encodings of these two functions using their common generalization called P-encoding introduced in Definition 2.5.

2.2 CNF Encoding

We work with formulas in conjunctive normal form (CNF formulas). For a standard notation see e.g. [11]. Namely, a literal is a variable $x$ (positive literal), or its negation $\neg x$ (negative literal). If $x$ is a variable, then let $\mathrm{lit}(x)=\{x,\neg x\}$. If $\mathbf{z}$ is a vector of variables, then we denote by $\mathrm{lit}(\mathbf{z})$ the union of $\mathrm{lit}(x)$ over $x\in\mathbf{z}$. For simplicity, we write $x\in\mathbf{z}$ if $x$ is a variable that occurs in $\mathbf{z}$, so $\mathbf{z}$ is considered as a set here, although, the order of the variables in $\mathbf{z}$ is important. Given a literal $g$, the term $\mathrm{var}(g)$ denotes the variable in the literal $g$, that is, $\mathrm{var}(g)=x$ for $g\in\mathrm{lit}(x)$. Given a set of literals $C$, $\mathrm{var}(C)=\{\mathrm{var}(g)\mid g\in C\}$.

A clause is a disjunction of a set of literals which does not contain a complementary pair of literals. A formula is in conjunctive normal form (CNF) if it is a conjunction of a set of clauses. In this paper, we consider only formulas in conjunctive normal form and we often simply refer to a formula, by which we mean a CNF formula. We treat clauses as sets of literals and formulas as sets of clauses. In particular, the order of the literals in a clause or clauses in a formula is not important and we use common set relations and operations (set membership, inclusion, set difference, etc.) on clauses and formulas. The empty clause (the contradiction) is denoted $\bot$ and the empty formula (the tautology) is denoted $\top$.

A unit clause consists of a single literal. A binary clause consists of two literals. A CNF formula, each clause of which contains at most $k$ literals, is said to be a $k$-CNF formula.

A partial assignment $\rho$ of variables $\mathbf{z}$ is a subset of $\mathrm{lit}(\mathbf{z})$ that does not contain a complementary pair of literals, so we have $|\rho\cap\mathrm{lit}(x)|\leq 1$ for each $x\in\mathbf{z}$. By $\varphi(\rho)$ we denote the formula obtained from $\varphi$ by the partial setting of the variables defined by $\rho$.

A CNF formula $\varphi(\mathbf{z})$ represents a boolean function $f$ on the variables in $\mathbf{z}$. We say that a clause $C$ is an implicate of a formula $\varphi$ if any satisfying assignment $\alpha$ of $\varphi$ satisfies $C$ as well, i.e. $\varphi(\alpha)=1$ implies $C(\alpha)=1$ for every assignment $\alpha$. We denote this property with $\varphi\models C$. We say that $C$ is a prime implicate of $\varphi$ if none $C^{\prime}\subset C$ is an implicate of $\varphi$. Note that whether a clause $C$ is a (prime) implicate of $\varphi$ depends only on the function $f$ represented by $\varphi$ and we can therefore speak about implicates of $f$ as well. We say that CNF $\varphi$ is prime if it consists only of prime implicates of $\varphi$. By the size of the formula $\varphi$ we mean the number of clauses in $\varphi$, it is denoted as $|\varphi|$ which is consistent with considering a CNF formula as a set of clauses.

In this paper we also consider encodings of boolean functions defined as follows.

Definition 2.3** (Encoding).**

Let $f(\mathbf{x})$ be a boolean function on variables $\mathbf{x}=(x_{1},\dots,x_{n})$. Let $\varphi(\mathbf{x},\mathbf{y})$ be a CNF formula on $n+\ell$ variables, where $\mathbf{y}=(y_{1},\dots,y_{\ell})$. We call $\varphi$ an encoding of $f$ if for every $\alpha\in{\{0,1\}}^{n}$ we have

[TABLE]

The variables in $\mathbf{x}$ and $\mathbf{y}$ are called input variables and auxiliary variables, respectively.

2.3 Propagation Complete Encoding

We are interested in encodings which are propagation complete. This notion relies on unit resolution which is a special case of general resolution. We say that two clauses $C_{1},C_{2}$ are resolvable, if there is exactly one literal $l$ such that $l\in C_{1}$ and $\neg l\in C_{2}$. The resolvent of these clauses is then defined as ${\cal R}(C_{1},C_{2})=(C_{1}\cup C_{2})\setminus\{l,\neg l\}$. If one of $C_{1}$ and $C_{2}$ is a unit clause, we say that ${\cal R}(C_{1},C_{2})$ is derived by unit resolution from $C_{1}$ and $C_{2}$. We say that a clause $C$ can be derived from $\varphi$ by unit resolution (or unit propagation), if $C$ can be derived from $\varphi$ by a series of unit resolutions. We denote this fact with $\varphi\vdash_{1}C$.

Definition 2.4** (Propagation complete encoding).**

Let $f(\mathbf{x})$ be a boolean function on variables $\mathbf{x}=(x_{1},\dots,x_{n})$. Let $\varphi(\mathbf{x},\mathbf{y})$ be a CNF formula on $n+\ell$ variables, where $\mathbf{y}=(y_{1},\dots,y_{\ell})$. We call $\varphi$ a propagation complete encoding (PC encoding) of $f(\mathbf{x})$ if it is an encoding of $f$ and for any $g_{1},\dots,g_{p}\in\mathrm{lit}(\mathbf{x})$, $p\geq 1$ and for each $h\in\mathrm{lit}(\mathbf{x})$, such that

[TABLE]

we have

[TABLE]

If $\varphi$ is a prime CNF formula, we call it prime PC encoding.

Note that the definition of a propagation complete encoding is less restrictive than requiring that formula $\varphi$ is propagation complete as defined in [8]. The difference is that in a PC encoding we only consider literals on input variables as assumptions and consequences of unit propagation. The definition of a propagation complete formula [8] does not distinguish input and auxiliary variables and the implication from (2) to (3) is required for all literals on all variables.

The following notation is used in the rest of the paper. Let $g_{1},\dots,g_{k}$ be literals on variables in $\varphi$. Then ${\cal U}_{\varphi}(g_{1},\dots,g_{k})$ denotes the set of literals that can be derived by unit resolution from $\varphi\wedge g_{1}\wedge\dots\wedge g_{k}$ that is

[TABLE]

2.4 Propagation Complete Encodings of $\operatorname{\mathrm{AMO}}_{n}$ and $\operatorname{\mathrm{EO}}_{n}$

Propagation complete encodings of $\operatorname{\mathrm{AMO}}_{n}$ and $\operatorname{\mathrm{EO}}_{n}$ share two common properties which we capture under the notion of P-encoding.

Definition 2.5** (P-encoding).**

Let $\varphi(\mathbf{x},\mathbf{y})$ be a formula with $\mathbf{x}=(x_{1},\dots,x_{n})$, $\mathbf{y}=(y_{1},\dots,y_{\ell})$, $n\geq 1$, $\ell\geq 0$. We say that $\varphi$ is a P-encoding if it satisfies the following two conditions.

1. (P1)

$\varphi\wedge x_{i}$ is satisfiable for each $i\in\{1,\dots,n\}$, 2. (P2)

$\varphi\wedge x_{i}\vdash_{1}\neg x_{j}$ holds for each $i,j\in\{1,\dots,n\}$ with $i\neq j$,

One can easily verify that being a P-encoding is a necessary condition for a formula to be a propagation complete encoding of $\operatorname{\mathrm{AMO}}_{n}$ or $\operatorname{\mathrm{EO}}_{n}$.

Lemma 2.6**.**

Let $\varphi(\mathbf{x},\mathbf{y})$ be a PC encoding of $\operatorname{\mathrm{AMO}}_{n}$ or $\operatorname{\mathrm{EO}}_{n}$. Then $\varphi$ is a P-encoding.

It turns out that conditions (P1) and (P2) are enough to show the lower bounds on the size of PC encodings of $\operatorname{\mathrm{AMO}}_{n}$ and $\operatorname{\mathrm{EO}}_{n}$ and these lower bounds are derived in the following sections by proving a lower bound on the size of P-encodings.

Every P-encoding with $n$ input variables is an encoding of either $\operatorname{\mathrm{AMO}}_{n}$ or $\operatorname{\mathrm{EO}}_{n}$, however, if it is an encoding of $\operatorname{\mathrm{EO}}_{n}$, it may not be propagation complete. In particular, this means that the converse of Lemma 2.6 is not true, see Section 3.4 for more detail.

2.5 The Main Result

Let us introduce the following notation.

Definition 2.7**.**

We denote the minimum size of a P-encoding with $n$ input variables by $\mathcal{P}(n)$ and the minimum size of a 2-CNF P-encoding with $n$ input variables by $\mathcal{P}_{2}(n)$.

We pay special attention to 2-CNF encodings of $\operatorname{\mathrm{AMO}}_{n}$. The minimum size of these encodings is $\mathcal{P}_{2}(n)$ as explained in Section 6. One can prove by contradiction that there are no 2-CNF encodings of $\operatorname{\mathrm{EO}}_{n}$ of $n\geq 3$ input variables as follows. Given an encoding $\varphi(\mathbf{x},\mathbf{y})$ of $\operatorname{\mathrm{EO}}_{n}$, we can eliminate an auxiliary variable $y$ from $\varphi$ by removing clauses containing $y$ or $\neg y$ and replacing them with the resolvents of all pairs of these clauses resolvable using the variable $y$. We call this step DP-elimination of $y$, since its repetition for all variables is one of the parts of Davis-Putnam algorithm [12] (see also [7]). After eliminating all auxiliary variables, the remaining formula is a 2-CNF representation of $\operatorname{\mathrm{EO}}_{n}$, since 2-CNF formulas are closed under resolution. This is a contradiction, since $x_{1}\lor\cdots\lor x_{n}$ is a prime implicate of $\operatorname{\mathrm{EO}}_{n}$.

We are now ready to state the main result of this paper.

Theorem 2.8**.**

Every PC encoding of $\operatorname{\mathrm{AMO}}_{n}$ or $\operatorname{\mathrm{EO}}_{n}$ has size at least $\mathcal{P}(n)$, the smallest size of a 2-CNF encoding of $\operatorname{\mathrm{AMO}}_{n}$ is equal to $\mathcal{P}_{2}(n)$, and

For $3\leq n\leq 8$ we have $\mathcal{P}(n)=\mathcal{P}_{2}(n)=3n-6$. 2. 2.

For $n\geq 9$ we have $\mathcal{P}(n)\geq 2n+\sqrt{n}-2$. 3. 3.

For $n\geq 9$ we have $\mathcal{P}_{2}(n)\geq 2n+2\sqrt{n}-3$.

The lower bound for $3\leq n\leq 8$ is tight, since for every $n\geq 3$, there is a 2-CNF encoding of $\operatorname{\mathrm{AMO}}_{n}$ of size $3n-6$ and it is a P-encoding. The lower bound for $n\geq 9$ is almost tight, since for every sufficiently large $n$, the product encoding [10] of $\operatorname{\mathrm{AMO}}_{n}$ has size $2n+4\sqrt{n}+O(n^{1/4})$ and is a 2-CNF P-encoding. Moreover, in Section 3.4, we prove that $\mathcal{P}(n)$ is a close estimate of the minimum size of PC encodings of the functions $\operatorname{\mathrm{AMO}}_{n}$ and $\operatorname{\mathrm{EO}}_{n}$. Namely, for each of these functions, there is a PC encoding of size at most $\mathcal{P}(n)+1$.

The first part of Theorem 2.8 follows from Lemma 2.6 and Lemma 6.1. Our proof of parts 2 and 3 relies on the notion of P-encodings in regular form we define below. Let $\varphi(\mathbf{x},\mathbf{y})$ be a P-encoding with input variables $x_{1},\ldots,x_{n}$. Given a variable $x_{i}$, $i=1,\ldots,n$, unit propagation on formula $\varphi\wedge x_{i}$ starts with clauses which contain the negative literal $\neg x_{i}$. It is important to distinguish different types of P-encodings according to the structure of these clauses. For each $i=1,\dots,n$ let us denote

[TABLE]

Definition 2.9**.**

Let $\varphi(\mathbf{x},\mathbf{y})$ be a P-encoding with input variables $x_{1},\ldots,x_{n}$. We say that $\varphi(\mathbf{x},\mathbf{y})$ is in regular form if the following holds for each $i\in\{1,\ldots,n\}$:

1. (R1)

$\left|Q_{\varphi,i}\right|=2$. 2. (R2)

Clauses in $Q_{\varphi,i}$ contain no input variables other than $x_{i}$. 3. (R3)

Clauses in $Q_{\varphi,i}$ are binary.

It is interesting to note that the construction of the product encoding introduced by Chen [10] leads to an encoding in regular form and this form is probably the best for most values of $n$. On the other hand, there are infinitely many rare values of $n$, for which using a P-encoding not in regular form allows to slightly reduce the size. This is used to describe the product encoding in Section 3.2.

The following theorem is used later to reduce the analysis of the minimum size P-encodings to the analysis of P-encodings in regular form and an induction argument. The theorem will be used for both general CNF and 2-CNF formulas. Since the minimum size of a P-encoding can be different in these two classes of formulas, we do not use the assumption that $\varphi(\mathbf{x},\mathbf{y})$ is a minimum size P-encoding and include condition (a) that has the same effect and can be used for both general CNF and 2-CNF formulas.

Theorem 2.10**.**

If $\varphi(\mathbf{x},\mathbf{y})$ is a prime P-encoding with input variables $x_{1},\ldots,x_{n}$, $n\geq 4$, then at least one of the following holds:

1. (a)

There is a P-encoding $\varphi^{\prime}$ with $n$ input variables, such that $|\varphi|\geq|\varphi^{\prime}|+1$. 2. (b)

There is a P-encoding $\varphi^{\prime}$ with $n-1$ input variables, such that $|\varphi|\geq|\varphi^{\prime}|+3$. 3. (c)

Formula $\varphi$ is in regular form.

Moreover if $\varphi$ is a 2-CNF formula, then so is $\varphi^{\prime}$ in cases (a) and (b).

We give a proof of Theorem 2.10 in Section 4. This theorem allows the following approach to proving a lower bound. If a given P-encoding $\varphi(\mathbf{x},\mathbf{y})$ is not in regular form, we use induction on $n$, and if it is in regular form, we prove a lower bound directly. Although we combine Theorem 2.10 later with additional arguments to prove stronger lower bounds, the following simple corollary of this theorem already gives the main term of the lower bound.

Corollary 2.11**.**

Let $\varphi(\mathbf{x},\mathbf{y})$ be a P-encoding with input variables $x_{1},\ldots,x_{n}$, $n\geq 6$. Then $\varphi$ consists of at least $\mathcal{P}(n)\geq 2n$ clauses.

Proof.

Assume that $\varphi$ is a minimum size P-encoding for $n\geq 3$ input variables. Without loss of generality, we can assume that it is a prime P-encoding (see also Lemma 3.5 below). We prove by induction on $n$ that $|\varphi|\geq\min(2n,3n-6)$. For $n\geq 6$, this implies the stated lower bound. For $n=3$, one can check (see also Lemma 5.1 below) that $\varphi$ must contain at least three clauses, thus $|\varphi|\geq 3=\min(2n,3n-6)$. Now let us assume that $n\geq 4$. Since $\varphi$ is of minimum size, no P-encoding with $n$ input variables with fewer clauses exists and item (a) of Theorem 2.10 does not apply. If $\varphi$ is not in regular form then by item (b) of Theorem 2.10, there is a P-encoding $\varphi^{\prime}$ with $n-1$ input variables such that $|\varphi|\geq|\varphi^{\prime}|+3$. By induction hypothesis $|\varphi^{\prime}|\geq\min(2(n-1),3(n-1)-6)\geq\min(2n,3n-6)-3$, thus

[TABLE]

If $\varphi$ is in regular form, then we have $|\varphi|\geq 2n\geq\min(2n,3n-6)$, since by definition, the union of $Q_{\varphi,i}$, $i=1,\ldots,n$, contains $2n$ clauses. ∎

In order to prove the lower bounds presented in Theorem 2.8, we perform a more careful analysis of P-encodings in regular form. In particular, in Section 5 we show the lower bound on $\mathcal{P}(n)$ and in Section 6 we show the lower bound on $\mathcal{P}_{2}(n)$.

3 Known and Auxiliary Results

In this section we state known and preliminary results used throughout the paper. We start by recalling some of the known good encodings of $\operatorname{\mathrm{AMO}}_{n}$ with some modifications.

3.1 Sequential Encoding

Let us present a variant of the sequential encoding [21], which addresses also more general cardinality constraints. This construction has also been called ladder encoding in [17]. The following recurrence describes the sequential encoding $\varphi^{s}_{n}$ of $\operatorname{\mathrm{AMO}}_{n}$ with a minor simplification which reduces its size to $3n-6$ and the number of auxiliary variables to $n-3$. The base case is

[TABLE]

and for each $n>3$, let

[TABLE]

where $y$ is an auxiliary variable not used in $\varphi^{s}_{n-1}$. By induction on $n$, one can verify that $\varphi^{s}_{n}$ is an encoding of $\operatorname{\mathrm{AMO}}_{n}$ with $n-3$ auxiliary variables and of size $|\varphi^{s}_{n}|=3n-6$. Since it is a prime 2-CNF, it is propagation complete, see [3]. Hence, we have the following.

Lemma 3.1**.**

For every $n\geq 3$, there is a 2-CNF PC encoding of $\operatorname{\mathrm{AMO}}_{n}$ of size $3n-6$.

Since $\operatorname{\mathrm{AMO}}_{n-1}$ is a symmetric function, the order of the variables in the formula for this function can be chosen arbitrarily without changing the function. When a different order of the variables is used in a recurrence, the obtained formula has a different form. Let us introduce the tree encoding by the following recurrence. The base case is

[TABLE]

and for each $n>3$, let

[TABLE]

where $y$ is an auxiliary variable not used in $\varphi^{t}_{n-1}$. By a similar argument as above, $\varphi^{t}_{n}$ is a PC encoding of $\operatorname{\mathrm{AMO}}_{n}$.

The size of the formulas $\varphi^{s}_{n}$ and $\varphi^{t}_{n}$ is the same and both are 2-CNF formulas. Let us consider a graph, whose vertices are variables and edges are the two-element sets $\mathrm{var}(C)$, where $C$ is a clause in the formula. Both the formulas $\varphi^{s}_{n}$ and $\varphi^{t}_{n}$ can be decomposed into triples of clauses which correspond to triangles in their graph and the triangles are connected via their vertices into a tree structure. In the graph for $\varphi^{s}_{n}$, these triangles form a path of length $n-3$ and in the graph for $\varphi^{t}_{n}$, they form a tree with diameter $O(\log n)$.

3.2 Product Encoding

Chen [10] introduced the product encoding of $\operatorname{\mathrm{AMO}}_{n}$ which has size $2n+4\sqrt{n}+O(\sqrt[4]{n})$. It turns out that $n=25$ is the smallest number of the variables, for which the product encoding outperforms the sequential encoding ($68$ vs. $69$ clauses). On the other hand, we show below that the sequential encoding is the smallest possible for $n\leq 8$. It is not clear whether this holds also for $9\leq n\leq 24$.

Let us present a slightly optimized version of the product encoding using a combination with sequential encoding for some values of $n$. The combination is obtained by considering two candidates for the recursive construction of the product encoding $\varphi^{p}_{n}$ and using the better of them for each $n\geq 7$. The base case for $n=3$ is

[TABLE]

If $n\geq 4$, the first candidate formula for $\varphi^{p}_{n}(\mathbf{x})$ is

[TABLE]

as in the recurrence used for the sequential encoding. If $n\leq 6$, let $\varphi^{p}_{n}(\mathbf{x})$ be (5). If $n\geq 7$, we use the formula described by Chen [10]. Let $m_{1}=\lceil\sqrt{n}\,\rceil$ and $m_{2}=\lceil n/m_{1}\rceil$. Clearly, we have $m_{1}\geq m_{2}\geq 3$. Arrange the input variables in $n$ pairwise different cells of a rectangular array of dimension $m_{1}\times m_{2}$. Let $r:\{1,\ldots,n\}\to\{1,\ldots,m_{1}\}$ and $c:\{1,\ldots,n\}\to\{1,\ldots,m_{2}\}$ be the functions, such that $r(i)$ is the row index and $c(i)$ the column index of the cell containing $x_{i}$. Let $y_{j}$, $j=1,\ldots,m_{1}$ and $z_{j}$, $j=1,\ldots,m_{2}$ be new auxiliary variables. Then, the second candidate for $\varphi^{p}_{n}(\mathbf{x})$ is the formula

[TABLE]

It is worth noting that formula (6) is in regular form, see Definition 2.9. The size of (5) is $3+|\varphi^{p}_{n-1}|$ and the size of (6) is $2n+|\varphi^{p}_{m_{1}}|+|\varphi^{p}_{m_{2}}|$. Let $\varphi^{p}_{n}(\mathbf{x})$ be the smaller of these formulas, where any of the candidates can be used, if their sizes are the same. It appears that formula (5) is smaller than (6) for $n\leq 23$ and for infinitely many other numbers, in particular, for the numbers $n=m^{2}+1$ and $n=m(m+1)+1$, where $m\geq 5$ is an integer. This can be explained as follows. If $n=m^{2}$ or $n=m(m+1)$, then $\varphi^{p}_{n}(\mathbf{x})$ is given by (6). In this case, the size of the candidate for $\varphi^{p}_{n+1}(\mathbf{x})$ given by (6) is at least $|\varphi^{p}_{n}(\mathbf{x})|+4$ and the size of the candidate for $\varphi^{p}_{n+1}(\mathbf{x})$ given by (5) is $|\varphi^{p}_{n}(\mathbf{x})|+3$.

Clearly, the size of $\varphi^{p}_{n}$ is at most $3+|\varphi^{p}_{n-1}|$ which is the size of (5) and using this, one can prove by induction on $n$ that for all $n\geq 3$, we have

[TABLE]

Asymptotically, a better bound was proven by Chen [10]. We present here a proof of this bound for completeness.

Lemma 3.2** (Chen [10]).**

We have $|\varphi^{p}_{n}|=2n+4\,\sqrt{n}+O(\sqrt[4]{n})$.

Proof.

If $n\geq 7$ and $m=\lceil\sqrt{n}\,\rceil$, the size of the product encoding satisfies

[TABLE]

By (7), we have $|\varphi^{p}_{m}|\leq 3m-6$. Together with (8) we obtain

[TABLE]

Using this bound for $|\varphi^{p}_{m}|$ and using (8) again, we obtain

[TABLE]

as required. ∎

3.3 Relationship to Monotone Circuits

Let us briefly describe a connection between the product encoding and the monotone circuit of the size $kn+o(n)$ for the function $T^{n}_{k}$, described in [14] and in Section 6, Theorem 2.3 in [22]. If $k=2$, the construction yields the product encoding for $\operatorname{\mathrm{AMO}}_{n}$. More generally, if $k$ is any constant, we obtain a PC encoding of “at most $(k-1)$” of size $kn+o(n)$. This is the smallest known encoding for this constraint, if $k\leq 16$. On the other hand, for every $k\geq 32$, a smaller encoding can be obtained using Batcher’s sorting network. For large $k$, an even smaller encoding of size $C_{k}n+O(1)$, where $C_{k}=O(\log k)$, can be obtained using AKS sorting networks.

Let $T^{n}_{k}$ be the threshold function “at least $k$” of $n$ variables. By the results cited above, there is a monotone circuit for this function consisting of $kn+o(n)$ binary AND and OR gates. In order to obtain asymptotically the same number of clauses in an encoding, the circuit has to be transformed in such a way that we replace groups of binary OR gates computing a disjunction of several previous gates by a single OR gate with multiple inputs. The Horn part of the Tseitin encoding of the circuit after this transformation consists of $kn+o(n)$ clauses. If we add a negative unit clause on the output of the circuit, we obtain an encoding of the “at most $(k-1)$” constraint. Moreover, using the specific structure of the circuit, one can verify that this encoding is propagation complete. In particular, if $k=2$, the obtained encoding is the product encoding of the constraint “at most one”.

3.4 P-Encodings and Encodings of $\operatorname{\mathrm{AMO}}_{n}$ and $\operatorname{\mathrm{EO}}_{n}$

We use P-encodings as a representation of common properties of PC encodings of $\operatorname{\mathrm{AMO}}_{n}$ and $\operatorname{\mathrm{EO}}_{n}$. Although the converse of Lemma 2.6 is not true (see below for an example) a partial converse is valid.

Lemma 3.3**.**

A P-encoding with $n$ input variables is an encoding (not necessarily propagation complete) of either $\operatorname{\mathrm{AMO}}_{n}$ or $\operatorname{\mathrm{EO}}_{n}$.

Proof.

Consider a P-encoding $\varphi(\mathbf{x},\mathbf{y})$ where $\mathbf{x}=(x_{1},\ldots,x_{n})$. The functions $\operatorname{\mathrm{AMO}}_{n}$ and $\operatorname{\mathrm{EO}}_{n}$ differ only on the zero assignment. In order to prove the statement, it is sufficient to prove that the function encoded by $\varphi(\mathbf{x},\mathbf{y})$ agrees with $\operatorname{\mathrm{AMO}}_{n}$ and $\operatorname{\mathrm{EO}}_{n}$ on the remaining assignments.

Consider a non-zero assignment $\alpha$ of the input variables. First, assume that $\alpha(x_{i})=\alpha(x_{j})=1$ for two indices $1\leq i<j\leq n$. Such $\alpha$ is a falsifying assignment of both functions $\operatorname{\mathrm{AMO}}_{n}$ and $\operatorname{\mathrm{EO}}_{n}$. By condition (P2) $\alpha$ cannot be extended to a model of $\varphi$. For the remaining case assume that $\alpha(x_{i})=1$ for some $i\in\{1,\ldots,n\}$ and $\alpha(x_{j})=0$ for all $j\in\{1,\ldots,n\}\setminus\{i\}$. Such $\alpha$ is a satisfying assignment of both the functions $\operatorname{\mathrm{AMO}}_{n}$ and $\operatorname{\mathrm{EO}}_{n}$. By condition (P1) we have that $\varphi\land x_{i}$ is satisfiable and condition (P2) implies that any satisfying assignment of $\varphi\land x_{i}$ sets all other input variables to [math]. This means that $\alpha$ can be extended to a satisfying assignment of $\varphi$. ∎

Consider the formula

[TABLE]

where $\varphi(\mathbf{x})$ is the prime representation of $\operatorname{\mathrm{AMO}}_{n}$ and $y$ is an auxiliary variable. One can verify that this formula is a P-encoding, is an encoding of $\operatorname{\mathrm{EO}}_{n}$, however, is not a PC encoding of $\operatorname{\mathrm{EO}}_{n}$, since $\varphi^{\prime}\wedge\bigwedge_{j\in\{1,\ldots,n-1\}}\neg x_{j}\not\vdash_{1}x_{n}$. This implies that the converse of Lemma 2.6 is not true.

Although we believe that the size of the smallest PC encoding of $\operatorname{\mathrm{AMO}}_{n}$ is $\mathcal{P}(n)$ and the size of the smallest PC encoding of $\operatorname{\mathrm{EO}}_{n}$ is $\mathcal{P}(n)+1$, we can prove only the following bounds.

Proposition 3.4**.**

Let $n\geq 2$, let $\varphi_{1}(\mathbf{x},\mathbf{y})$ be a smallest PC encoding of $\operatorname{\mathrm{AMO}}_{n}(\mathbf{x})$ and let $\varphi_{2}(\mathbf{x},\mathbf{z})$ be a smallest PC encoding of $\operatorname{\mathrm{EO}}_{n}(\mathbf{x})$. Then

[TABLE]

Proof.

The lower bounds follow from Lemma 2.6. Let $\varphi(\mathbf{x},\mathbf{y})$ be a P-encoding of size $\mathcal{P}(n)$. One can verify that

[TABLE]

where $z$ is a new auxiliary variable, is a PC encoding of $\operatorname{\mathrm{AMO}}_{n}(\mathbf{x})$. This implies $|\varphi_{1}|\leq\mathcal{P}(n)+1$. Moreover, one can verify that

[TABLE]

is a PC encoding of $\operatorname{\mathrm{EO}}_{n}(\mathbf{x})$. This implies $|\varphi_{2}|\leq\mathcal{P}(n)+1$. ∎

3.5 Simple Reductions of Encodings

In this section we present additional properties of encodings that can be assumed without loss of generality, since every encoding can be modified to satisfy them without increase of the size.

Lemma 3.5**.**

The prime CNF formula obtained from a given P-encoding $\varphi(\mathbf{x},\mathbf{y})$ by replacing every clause by a prime implicate contained in it, is also a P-encoding.

Proof.

Consider a clause $C$ in the original formula and a prime implicate $C^{\prime}$ contained in it. Replacing $C$ by $C^{\prime}$ does not change the function represented by the formula and one can verify that the conditions (P1) and (P2) remain satisfied. Repeating this for all clauses of $\varphi(\mathbf{x},\mathbf{y})$ proves the lemma. ∎

If the number of occurrences of an auxiliary variable $y$ in an encoding $\varphi$ is at most 4, then DP-elimination of $y$ does not increase the size of the formula (see Section 2.5 for definition of DP-elimination) and leads to an encoding of the same function with a smaller number of auxiliary variables. This allows us to make the following observation.

Lemma 3.6**.**

Let $\varphi(\mathbf{x},\mathbf{y})$ be an encoding of a function $f(\mathbf{x})$ of minimum size that, moreover, has the minimum number of auxiliary variables among such encodings. Then any auxiliary variable $y\in\mathbf{y}$ occurs in at least 5 clauses of $\varphi$.

With a little effort one can show that DP-elimination also preserves propagation completeness of an encoding. In particular, Lemma 3.6 holds also for a PC encoding of minimum size, however, this is not used in this paper.

3.6 Substituting Variables in Unit Propagation

One of the reduction steps we use later to simplify an encoding is the substitution of a variable with a literal on a variable already present in the formula. If $\varphi(\mathbf{z})$ is a formula and $g_{1},g_{2}\in\mathrm{lit}(\mathbf{z})$, we denote by $\varphi[g_{1}\leftarrow g_{2}]$ the formula obtained from $\varphi$ using the substitution $g_{1}\leftarrow g_{2}$. More precisely, if the literal $g_{1}$ is positive, then the variable $\mathrm{var}(g_{1})$ is substituted by the literal $g_{2}$. If $g_{1}$ is negative, then the variable $\mathrm{var}(g_{1})$ is substituted by the literal $\neg g_{2}$. An important property of this operation is that this kind of substitution preserves unit propagation.

Lemma 3.7**.**

Let $\varphi(\mathbf{z})$ be a formula, let $g_{1},g_{2},h\in\mathrm{lit}(\mathbf{z})$, such that $\mathrm{var}(g_{1})\not=\mathrm{var}(h)$ and assume, $\varphi[g_{1}\leftarrow g_{2}]$ is satisfiable. Then

[TABLE]

Lemma 3.7 is a consequence of a more general statement with an essentially the same proof which we are going to show first. Let us consider a substitution $t:\mathbf{z}\to\mathrm{lit}(\mathbf{z})$ of the variables in $\mathbf{z}$ by literals on the same set of the variables. The substitution extends to the literals so that for every $x\in\mathbf{z}$, we have $t(\neg x)=\neg t(x)$. Moreover, the substitution extends to the clauses and the formulas in CNF as follows. If $C=g_{1}\vee\cdots\vee g_{k}$ is a clause with variables from $\mathbf{z}$ then $t(C)$ is defined as $t(g_{1})\vee\cdots\vee t(g_{k})$, if there is no complementary pair of literals among $t(g_{1}),\ldots,t(g_{k})$, and $\top$ otherwise. If $\varphi$ is a CNF formula, then $t(\varphi)=\bigwedge_{C\in\varphi}t(C)$, where $t(\varphi)=\top$ in case $t(C)=\top$ for all $C\in\varphi$. In particular, $\varphi[g_{1}\leftarrow g_{2}]=t(\varphi)$ where $t$ is a map on the literals defined for every literal $e$ as

[TABLE]

Applying a substitution to a formula preserves resolution proofs as we show in the following lemma.

Lemma 3.8**.**

Let $\varphi(\mathbf{z})$ be a formula on the variables $\mathbf{z}$ and let $C_{1},\ldots,C_{k}$ be a resolution proof of $C_{k}$ from $\varphi$. If $t:\mathbf{z}\to\mathrm{lit}(\mathbf{z})$ is a substitution as above, then there is a sequence $D_{1},\ldots,D_{k}$, where each $D_{i}$ is a clause or $\top$, such that the following implications are satisfied

[TABLE]

and the sequence of clauses contained in $D_{1},\ldots,D_{k}$ is a resolution proof of the clauses contained in it from the clauses in $t(\varphi)$. If the original proof is a unit resolution proof, so is the derived proof.

Proof.

For each $i=1,\ldots,k$, we have either $C_{i}\in\varphi$ or $C_{i}={\cal R}(C_{r},C_{s})$, where $r,s<i$. In order to prove the claim, let us construct $D_{i}$ by induction on $i=1,\ldots,k$. Some of the clauses can repeat in the constructed sequence. Assume, the sequence $D_{1},\ldots,D_{i-1}$ is constructed and is empty or satisfies the requirements formulated above. If $C_{i}\in\varphi$, choose $D_{i}=t(C_{i})$. If $C_{i}\not\in\varphi$, then $C_{i}={\cal R}(C_{r},C_{s})$, where $r,s<i$ and $C_{r}=g\vee A$, $C_{s}=\neg g\vee B$, and $C_{i}=A\vee B$ for some literal $g$ and sets of literals $A$ and $B$. If $t(C_{i})=t(A\vee B)=\top$, then choose $D_{i}=\top$. Otherwise, there is no conflict in $t(A)\cup t(B)$.

If, moreover, the variable $\mathrm{var}(t(g))$ has no occurence in $t(A)\cup t(B)$, then $t(C_{r})$ and $t(C_{s})$ are clauses and are resolvable using the literals $t(g)$ and $t(\neg g)$. This implies $D_{r}\subseteq t(C_{r})$, $D_{s}\subseteq t(C_{s})$, and $t(C_{i})={\cal R}(t(C_{r}),t(C_{s}))$. If $D_{r}$ and $D_{s}$ are resolvable, then ${\cal R}(D_{r},D_{s})\subseteq t(C_{i})$ and we can choose $D_{i}={\cal R}(D_{r},D_{s})$. Otherwise, either $t(g)\not\in D_{r}$ and we have $D_{r}\subseteq t(C_{i})$ or $t(\neg g)\not\in D_{s}$ and we have $D_{s}\subseteq t(C_{i})$. Hence, we can choose $D_{i}=D_{r}$ or $D_{i}=D_{s}$ so that $D_{i}\subseteq t(C_{i})$.

Assume, some of the literals $t(g)$ and $t(\neg g)$ has an occurence in $t(A)\cup t(B)$. Since $t(A)\cup t(B)$ is a clause, only one of the literals $t(g)$ and $t(\neg g)$ is contained in it. If $t(g)\in t(A)\cup t(B)$, then $t(C_{r})=t(g)\cup t(A)\subseteq t(A)\cup t(B)=t(C_{i})$ and we can choose $D_{i}=D_{r}\subseteq t(C_{r})\subseteq t(C_{i})$. Similarly, if $t(\neg g)\in t(A)\cup t(B)$, we can choose $D_{i}=D_{s}\subseteq t(C_{s})\subseteq t(C_{i})$.

If $C$ is a unit clause, then $t(C)$ is a unit clause. This implies the last statement of the lemma. ∎

Lemma 3.7 now easily follows from Lemma 3.8.

Proof of Lemma 3.7.

If $t$ is defined as in (10), then $\varphi[g_{1}\leftarrow g_{2}]=t(\varphi)$ and $t(h)=h$. Lemma 3.8 implies $t(\varphi)\vdash_{1}\bot$ or $t(\varphi)\vdash_{1}t(h)$. The first is excluded because $\varphi[g_{1}\leftarrow g_{2}]=t(\varphi)$ is satisfiable. Hence, we have $\varphi[g_{1}\leftarrow g_{2}]\vdash_{1}h$ as required. ∎

4 Reducing to Regular Form

This section is devoted to the proof of Theorem 2.10. We start with basic properties of P-encodings.

Lemma 4.1**.**

Let $n\geq 2$ and let $\varphi(\mathbf{x},\mathbf{y})$ be a P-encoding with input variables $\mathbf{x}=(x_{1},\dots,x_{n})$ and auxiliary variables $\mathbf{y}=(y_{1},\dots,y_{\ell})$. For each distinct $x_{i},x_{j}\in\mathbf{x}$ it holds that

1. (a)

$\varphi\wedge x_{i}\not\vdash_{1}x_{j}$, 2. (b)

$\varphi\wedge\neg x_{i}\not\vdash_{1}\neg x_{j}$, 3. (c)

$\varphi$* contains a binary clause containing the literal $\neg x_{i}$.*

Proof.

Suppose that $\varphi$ satisfies the assumption. The claims of the lemma can be proven as follows.

1. (a)

If $\varphi\wedge x_{i}\vdash_{1}x_{j}$, then $\varphi\wedge x_{i}\vdash_{1}\bot$, since $\varphi\wedge x_{i}\vdash_{1}\neg x_{j}$ by condition (P2). This contradicts condition (P1). 2. (b)

If $\varphi\wedge\neg x_{i}\vdash_{1}\neg x_{j}$, then $\varphi\wedge x_{j}\vdash_{1}\bot$, since $\varphi\wedge x_{j}\vdash_{1}\neg x_{i}$ by condition (P2). This contradicts condition (P1). 3. (c)

Since $\varphi\wedge x_{i}\vdash_{1}\neg x_{j}$, there is a series of unit resolutions starting from $x_{i}$, whose first step uses a binary clause containing $\neg x_{i}$. ∎

The following lemma shows that fixing any set of input variables to zero in a P-encoding gives us a P-encoding on the remaining input variables.

Lemma 4.2**.**

Let $\varphi(\mathbf{x},\mathbf{y})$ be a P-encoding and let $I\subset\{1,\ldots,n\}$ be a non-empty set of indices and consider the partial assignment $\rho=\{\neg x_{j}\ |\ j\not\in I\}$. Then $\varphi(\rho)$ is a P-encoding with the input variables $x_{i}$, $i\in I$.

Proof.

If $i\in I$, then $\varphi\wedge x_{i}$ derives all the literals $\neg x_{k}$ for $k\in\{1,\ldots,n\}\setminus\{i\}$ including all the literals in $\rho$ and does not derive a contradiction. Hence, the propagation from $\varphi(\rho)\wedge x_{i}$ cannot derive a contradiction and derives $\neg x_{k}$ for all $k\in I\setminus\{i\}$. It follows that $\varphi(\rho)$ with the input variables $x_{I}$ satisfies (P1) and (P2). ∎

We now concentrate on clauses with negative literals on input variables.

Lemma 4.3**.**

Let $\varphi(\mathbf{x},\mathbf{y})$ be a prime P-encoding, $C\in\varphi$, and $\neg x_{i}\in C$. Then one of the following is satisfied

1. (i)

$C=\neg x_{i}\vee A$, where $\emptyset\not=A\subseteq\mathrm{lit}(\mathbf{y})$, 2. (ii)

$C=\neg x_{i}\vee\neg x_{j}$* for some $j\not=i$.*

Proof.

We have $C=\neg x_{i}\vee A$ for a non-empty set of literals $A$. If $A$ contains a literal on an input variable, consider the following two cases.

• •

If there is a literal $\neg x_{j}\in A$ for some $j\neq i$, consider the clause $\neg x_{i}\vee\neg x_{j}$. This clause is an implicate of $\varphi(\mathbf{x},\mathbf{y})$ due to property (P2) and it is prime due to property (P1). Hence, necessarily $C=\neg x_{i}\vee\neg x_{j}$.

• •

If $x_{j}\in A$ for some $j\neq i$ then $C\setminus\{x_{j}\}={\cal R}(C,\neg x_{i}\vee\neg x_{j})$ is an implicate as well which is in contradiction with primality of $\varphi$.

Otherwise, $\emptyset\not=A\subseteq\mathrm{lit}(\mathbf{y})$. ∎

The following proposition shows that $|Q_{\varphi,i}|\geq 2$ for every input variable $x_{i}\in\mathbf{x}$ in a minimum size P-encoding $\varphi(\mathbf{x},\mathbf{y})$.

Proposition 4.4**.**

Let $n\geq 3$ and let $\varphi(\mathbf{x},\mathbf{y})$ be a P-encoding with $n$ input variables $\mathbf{x}=(x_{1},\ldots,x_{n})$. Let $x_{i}\in\mathbf{x}$ and suppose that $|Q_{\varphi,i}|=1$. Then there is another P-encoding $\varphi^{\prime}$ with input variables $\mathbf{x}$ and satisfying $|\varphi|\geq|\varphi^{\prime}|+1$. Moreover, if $\varphi$ is a 2-CNF formula, then so is $\varphi^{\prime}$.

Proof.

Using Lemma 3.5, we can assume that $\varphi$ is a prime formula. By Lemma 4.1, there is a binary clause $C=\neg x_{i}\vee e\in\varphi$ with some $e\in\mathrm{lit}(\mathbf{x}\cup\mathbf{y})$. Let us assume for a contradiction that $\mathrm{var}(e)=x_{j}$ with $j\neq i$. By Lemma 4.3, $C=\neg x_{i}\vee\neg x_{j}$. Let $x_{k}\in\mathbf{x}\setminus\{x_{i},x_{j}\}$. We have that $\varphi\wedge x_{i}\vdash_{1}\neg x_{k}$. Since $C$ is the only clause of $\varphi$ containing $\neg x_{i}$, unit resolution uses $x_{i}$ to derive $\neg x_{j}$ and does not use $x_{i}$ in any of the later steps. Hence, we have $\varphi\wedge\neg x_{j}\vdash_{1}\neg x_{k}$, which is a contradiction with Lemma 4.1(b). This implies $e\in\mathrm{lit}(\mathbf{y})$.

Consider the substitution $e\leftarrow x_{i}$ and let us show that $\varphi^{\prime}=\varphi[e\leftarrow x_{i}]$ satisfies the conditions (P1) and (P2).

1. (P1)

Let us show that $\varphi^{\prime}\wedge x_{k}$ is a satisfiable formula for each $k\in\{1,\dots,n\}$. If $k=i$, we have that $\varphi\wedge x_{i}$ is satisfiable and that $\varphi\wedge x_{i}\vdash_{1}e$ using the clause $C$. Thus, the formula $\varphi\wedge x_{i}\wedge e$ is satisfiable and both literals $x_{i}$ and $e$ get value $1$ in each of its satisfying assignments. It follows that $\varphi^{\prime}\wedge x_{i}=(\varphi\wedge x_{i})[e\leftarrow x_{i}]$ is satisfiable as well.

If $k\neq i$, we have $\varphi\wedge x_{k}\vdash_{1}\neg x_{i}$. Since $C=\neg x_{i}\vee e$ is the only clause in $\varphi$ that contains $\neg x_{i}$, it holds that $\varphi\wedge x_{k}\vdash_{1}\neg e$. Thus, both literals $x_{i}$ and $e$ get value [math] in any satisfying assignment of $\varphi\wedge x_{k}$. It follows that $\varphi^{\prime}\wedge x_{k}=(\varphi\wedge x_{k})[e\leftarrow x_{i}]$ is satisfiable as well. 2. (P2)

Follows from Lemma 3.7 for the formula $\varphi^{\prime}\wedge x_{k}=(\varphi\wedge x_{k})[e\leftarrow x_{i}]$ and $h=\neg x_{\ell}$, where $k,\ell\in\{1,\dots,n\}$, $k\not=\ell$.

The substitution $e\leftarrow x_{i}$ changes $C$ to $\top$ which is omitted in $\varphi^{\prime}$. Hence $\varphi^{\prime}$ has size smaller than $\varphi$. This completes the proof. ∎

Let us present an example of a formula which shows that Proposition 4.4 does not hold for PC encodings of $\operatorname{\mathrm{AMO}}_{n}$ instead of P-encodings. The formula (9) with auxiliary variables $\mathbf{z}=(z,\mathbf{y})$ is a PC encoding of $\operatorname{\mathrm{AMO}}_{n}(\mathbf{x})$ with a single occurence of $\neg x_{1}$, for which the construction in Proposition 4.4 provides a formula $\varphi^{\prime}$ which is a PC encoding of $\operatorname{\mathrm{EO}}_{n}(\mathbf{x})$.

P-encodings that are not in regular form can be reduced to P-encodings with a smaller number of input variables by the following statements. We start with P-encodings which violate Condition (R1) of Definition 2.9. Recall that this condition requires that $|Q_{\varphi,i}|=2$ for every input variable $x_{i}\in\mathbf{x}$ of a P-encoding in regular form.

Proposition 4.5**.**

Let $\varphi(\mathbf{x},\mathbf{y})$ be a P-encoding with $n\geq 3$ input variables $\mathbf{x}=(x_{1},\ldots,x_{n})$, such that $\left|Q_{\varphi,i}\right|\neq 2$ for some $i\in\{1,\ldots,n\}$. Then, there is a formula $\varphi^{\prime}$, which satisfies one of the following

1. (a)

$\varphi^{\prime}$* is a P-encoding with $n$ input variables and $|\varphi|\geq|\varphi^{\prime}|+1$,* 2. (b)

$\varphi^{\prime}$* is a P-encoding with $n-1$ input variables and $|\varphi|\geq|\varphi^{\prime}|+3$.*

Moreover, if $\varphi$ is 2-CNF, then so is $\varphi^{\prime}$.

Proof.

Assume, $\left|Q_{\varphi,i}\right|\not=2$ for some $i\in\{1,\dots,n\}$. Lemma 4.1 implies that $|Q_{\varphi,i}|\geq 1$. Assume, $|Q_{\varphi,i}|=1$. According to Proposition 4.4, there is a P-encoding satisfying condition (a) of the conclusion. If $|Q_{\varphi,i}|\geq 3$, then setting $x_{i}=0$ yields a formula $\varphi^{\prime}$ of size at most $|\varphi|-3$ and this formula is a P-encoding with $n-1$ input variables by Lemma 4.2. Hence, condition (b) of the conclusion is satisfied. In both cases, $\varphi^{\prime}$ is obtained from $\varphi$ by a substitution that does not increase the size of clauses, so also the last part of the statement is satisfied. ∎

Now, we look at P-encodings which satisfy Condition (R1) but do not satisfy Condition (R2) of Definition 2.9. For this purpose, we use the following auxiliary lemma.

Lemma 4.6**.**

Let $\varphi(\mathbf{x},\mathbf{y})$ be a P-encoding with $n\geq 4$ input variables $\mathbf{x}=(x_{1},\ldots,x_{n})$ and let $i,j,k\in\{1,\dots,n\}$ be three different indices. Then $Q_{\varphi,i}\neq\{\neg x_{i}\vee\neg x_{j},\,\neg x_{i}\vee\neg x_{k}\}$.

Proof.

Let $\ell\in\{1,\dots,n\}\setminus\{i,j,k\}$. We have $\varphi\wedge x_{i}\vdash_{1}\neg x_{\ell}$. Assume, $Q_{\varphi,i}$ consists of the two clauses $\neg x_{i}\vee\neg x_{j}$ and $\neg x_{i}\vee\neg x_{k}$. Then, we have $\varphi\wedge\neg x_{j}\wedge\neg x_{k}\vdash_{1}\neg x_{\ell}$. This implies that $x_{j}\vee x_{k}\vee\neg x_{\ell}$ is an implicate of $\varphi$ which is in contradiction with the conditions (P1) and (P2) used for the formula $\varphi\wedge x_{\ell}$. ∎

Let $\varphi(\mathbf{x},\mathbf{y})$ be a P-encoding with $n$ input variables $\mathbf{x}=(x_{1},\ldots,x_{n})$. Recall that Condition (R2) of Definition 2.9 states that clauses in $Q_{\varphi,i}$ do not contain other input variables than $x_{i}$ for every $i=1,\ldots,n$, if $\varphi(\mathbf{x},\mathbf{y})$ is in regular form.

Proposition 4.7**.**

Let $\varphi(\mathbf{x},\mathbf{y})$ be a prime P-encoding with $n\geq 4$ input variables $\mathbf{x}=(x_{1},\ldots,x_{n})$, such that (R1) is satisfied and (R2) is not satisfied. Then there is a P-encoding $\varphi^{\prime}$ with $n-1$ input variables, such that $|\varphi|\geq|\varphi^{\prime}|+3$. If $\varphi$ is a 2-CNF formula, then so is $\varphi^{\prime}$.

Proof.

Let $i$ be an index, for which (R2) is not satisfied which means that some clause $C\in Q_{\varphi,i}$ contains another input variable $x_{j}$, $j\neq i$ in addition to the literal $\neg x_{i}$. By Lemma 4.3 we get that $C=\neg x_{i}\vee\neg x_{j}$. Without loss of generality, assume $i=1$, $j=2$, so $\varphi$ contains clauses $\neg x_{1}\vee\neg x_{2}$,  $\neg x_{1}\vee B_{1}$,  $\neg x_{2}\vee B_{2}$ for some sets of literals $B_{1},B_{2}$. By Lemma 4.3 and Lemma 4.6, both $B_{1}$ and $B_{2}$ are sets of auxiliary literals. By Lemma 4.2 we have that $\psi=\varphi(\{\neg x_{1}\})$ is a P-encoding with $n-1$ input variables $x_{2},\ldots,x_{n}$. Since $\varphi$ satisfies (R1), we have that $|Q_{\varphi,i}|=2$ and thus

[TABLE]

Since $\varphi$ satisfies (R1), the literal $\neg x_{2}$ occurs only once in $\psi$. Hence, Proposition 4.4 implies that there is a P-encoding $\varphi^{\prime}$ with $n-1$ input variables satisfying $|\psi|\geq|\varphi^{\prime}|+1$. Together with (11) we get

[TABLE]

as required. ∎

We are now ready to give a proof of Theorem 2.10. Since we have already analyzed encodings not satisfying some of the conditions (R1) and (R2), the main step of the proof is to deal with encodings not satisfying Condition (R3). Let us recall that (R3) requires that for every $i=1,\ldots,n$ the set $Q_{\varphi,i}$ consists of two binary clauses. Let us also recall that ${\cal U}_{\varphi}(g_{1},\dots,g_{k})$ denotes the set of literals that can be derived by unit resolution from $\varphi\wedge g_{1}\wedge\dots\wedge g_{k}$.

Proof of Theorem 2.10.

Let $\varphi(\mathbf{x},\mathbf{y})$ be a prime P-encoding with input variables $\mathbf{x}=(x_{1},\ldots,x_{n})$. If $\varphi$ is in regular form, we are done. If some of the conditions (R1) and (R2) is not satisfied, the conclusion follows from propositions 4.5 and 4.7. For the rest of the proof assume that $\varphi$ satisfies  (R1) and (R2). If $\varphi$ is a 2-CNF, the condition (R3) is satisfied and we are done.

If $\varphi$ is not a 2-CNF, assume that $\varphi$ does not satisfy (R3) for some $i\in\{1,\ldots,n\}$. By Lemma 4.1 we have that one of the clauses in $Q_{\varphi,i}$ is a binary clause. By (R1), we have $|Q_{\varphi,i}|=2$ and since $Q_{\varphi,i}$ does not satisfy (R3), the other clause consists of at least three literals. Moreover, due to (R2) the only input variable which appears in some clause in $Q_{\varphi,i}$ is $x_{i}$. Thus we can write

[TABLE]

for some literals $y,z_{1},\ldots,z_{\ell}$ on auxiliary variables where $\ell>1$. We claim that for every $j\in\{1,\ldots,\ell\}$ we have

[TABLE]

and

[TABLE]

Let us assume for a contradiction that there is $j\in\{1,\ldots,\ell\}$ satisfying the negation of (12) or the negation of (13). If $\varphi\wedge y\vdash_{1}\neg z_{j}$, then $\varphi\wedge x_{i}\vdash_{1}\neg z_{j}$, since $C_{1}\in\varphi$. Hence, we can assume $\varphi\wedge x_{i}\vdash_{1}\neg z_{j}$. This implies that $\neg x_{i}\vee\neg z_{j}$ is an implicate of $\varphi$. However, the resolvent ${\cal R}(\neg x_{i}\vee\neg z_{j},C_{2})$ is a strict subclause of $C_{2}$ which is in contradiction with primality of $C_{2}$.

Consider any input variable $x_{j}$, $j\not=i$. Since $\varphi$ satisfies (P2) we have that $\varphi\wedge x_{i}\vdash_{1}\neg x_{j}$. Clause $C_{1}$ is the only one in $\varphi$ that becomes unit when resolved with $x_{i}$. Moreover, we can observe that clause $C_{2}$ is not used in the derivation $\varphi\land x_{i}\vdash_{1}\neg x_{j}$. This follows by (12), because in order for $C_{2}$ to be used in a unit resolution derivation, at least one of $\neg z_{1},\ldots,\neg z_{\ell}$ must be derived first. Thus necessarily

[TABLE]

and in particular

[TABLE]

Let $\psi=(\varphi\setminus\{C_{2}\})\cup\{C_{3}\}$, where $C_{3}=\neg y\vee z_{1}\vee\ldots\vee z_{\ell}$. We prove below that $\psi$ is a P-encoding with input variables $\mathbf{x}$. Since $|\psi|=|\varphi|$ and $|\psi|$ contains only one occurrence of $\neg x_{i}$, Proposition 4.4 implies that there is a P-encoding $\varphi^{\prime}$ with $n$ input variables satisfying $|\varphi|\geq|\varphi^{\prime}|+1$ thus satisfying condition (a). According to Definition 2.5 it remains to show that $\psi$ satisfies conditions (P1) and (P2).

1. (P1)

Let $x_{j}$, $j\in\{1,\ldots,n\}$ be an arbitrary input variable and let us show that $\psi\wedge x_{j}$ is satisfiable.

• •

If $j=i$, we have $\varphi\wedge x_{i}\models z_{1}\vee\cdots\vee z_{\ell}$, since $C_{2}$ is contained in $\varphi$. Consequently, $\varphi\wedge x_{i}\models C_{3}$.

• •

If $j\neq i$, we have $\varphi\models\neg y\vee\neg x_{j}$ by (15). Hence, $\varphi\wedge x_{j}\models\neg y$ and $\varphi\wedge x_{j}\models C_{3}$.

In both cases, since $\varphi\wedge x_{j}$ is satisfiable, so is $\psi\wedge x_{j}$, and $\psi$ satisfies (P1). 2. (P2)

Let $j,k\in\{1,\ldots,n\}$ be two different indices of input variables and let us show that $\psi\wedge x_{j}\vdash_{1}\neg x_{k}$. Let us look at derivation of $\varphi\wedge x_{j}\vdash_{1}\neg x_{k}$.

• •

If $j=i$, then clause $C_{2}$ is not used in the derivation $\varphi\wedge x_{i}\vdash_{1}\neg x_{k}$. This follows by (12), because in order for $C_{2}$ to be used in a unit resolution derivation, at least one of $\neg z_{1},\ldots,\neg z_{\ell}$ must be derived first. It follows that $\psi\wedge x_{i}\vdash_{1}\neg x_{k}$ as well.

• •

Assume $j\neq i$. If $C_{2}$ is not used in the derivation $\varphi\wedge x_{j}\vdash_{1}\neg x_{k}$, then also $\psi\wedge x_{j}\vdash_{1}\neg x_{k}$ and we are done. Assume, $C_{2}$ is used in the derivation $\varphi\wedge x_{j}\vdash_{1}\neg x_{k}$. If $C_{2}$ is used to derive some of the literals $z_{1},\ldots,z_{\ell}$, then in order to do that we need $\varphi\wedge x_{j}\vdash_{1}x_{i}$, which is not true. Hence, we can assume that $C_{2}$ is used to derive $\neg x_{i}$. Before that we have $\varphi\wedge x_{j}\vdash_{1}\neg z_{r}$ for all $r\in\{1,\ldots,\ell\}$ and these derivations are possible in $\psi$ as well. Hence, $\psi\wedge x_{j}\vdash_{1}\neg z_{r}$ for all $r\in\{1,\ldots,\ell\}$. Moreover, we obtain $\psi\wedge x_{j}\vdash_{1}\neg x_{i}$ because we can replace the step using $C_{2}$ in the original unit resolution derivation with two steps using $C_{3}$ to derive $\neg y$ and then $C_{1}$ to derive $\neg x_{1}$. Together, we get that also in this case $\psi\wedge x_{j}\vdash_{1}\neg x_{k}$.

This concludes the proof of Theorem 2.10. ∎

The following notation will be used in the subsequent sections. Assume, $\varphi(\mathbf{x},\mathbf{y})$ is a P-encoding with input variables $\mathbf{x}=(x_{1},\ldots,x_{n})$ in regular form. For each $i=1,\dots,n$, let

[TABLE]

Clearly, for all $i=1,\ldots,n$, we have $|L_{\varphi,i}|=2$, Moreover, since $\neg x_{i}$ is not an implicate of $\varphi$, the set $L_{\varphi,i}$ does not contain complementary literals and we have $|L^{\mathrm{v}}_{\varphi,i}|=2$. The following is now an easy observation.

Lemma 4.8**.**

If $i,j\in\{1,\ldots,n\}$ are two different indices of input variables, then $L_{\varphi,i}\neq L_{\varphi,j}$.

Proof.

Assuming $L_{\varphi,i}=L_{\varphi,j}$, we get a contradiction with conditions (P1) and (P2) as follows. The formula $\varphi\wedge x_{i}$ is satisfiable and derives both literals in $L_{\varphi,i}=L_{\varphi,j}$. Hence, it is not possible to have $\varphi\wedge x_{i}\vdash_{1}\neg x_{j}$. ∎

Note that it follows from Lemma 4.8 that $\varphi$ contains at least $\sqrt{n/2}$ auxiliary variables in $\mathbf{y}$. This is because if the number of auxiliary variables is $\ell$, then we have at most $\binom{2\ell}{2}$ sets $L_{\varphi,i}$. It follows that $\binom{2\ell}{2}\geq n$ and $\ell\geq\sqrt{n/2}$ and this gives a hint on how $\sqrt{n}$ gets into the lower bound. In order to obtain a corresponding term $\Omega(\sqrt{n})$ in the lower bound on the number of clauses, we distinguish two types of clauses in a P-encoding in regular form as follows:

• •

Clauses from $\bigcup_{i=1}^{n}Q_{\varphi,i}$ are of type Q.

• •

The remaining clauses in $\varphi$ are of type R.

A P-encoding in regular form with $n$ input variables contains $2n$ clauses of type Q. This was used in Corollary 2.11 to prove a lower bound $2n$ on the size of every P-encoding with a sufficiently large number $n$ of input variables. In order to prove the lower bounds stated in the introduction, we prove in the next two sections lower bounds on the number of clauses of type R in cases of general CNF P-encodings and 2-CNF P-encodings.

5 A Lower Bound For General P-Encodings

This section is devoted to the proof of a lower bound on $\mathcal{P}(n)$, i.e. the proof of statement 1 for $\mathcal{P}(n)$ and statement 2 of Theorem 2.8. The proof consists of a lower bound on the size of a P-encoding in regular form and an inductive argument based on Theorem 2.10. We have observed at the end of Section 4 that if $\varphi(\mathbf{x},\mathbf{y})$ is a P-encoding with $n$ input variables in regular form, then the number of auxiliary variables is at least $\sqrt{n/2}$. We improve this bound and, moreover, we show that there must be an input variable $x_{i}$ such that unit propagation starting from $\varphi\land x_{i}$ derives at least $\sqrt{n-3/4}+1/2$ literals on auxiliary variables. This implies that there must be almost as many R clauses in $\varphi$ implying the lower bound.

We start with the base cases for induction. By CNF complexity of a boolean function, we mean the minimum size of a CNF formula expressing the function. Clearly, this is also the minimum size of an encoding of the function without auxiliary variables. One can easily verify that the CNF complexity of $\operatorname{\mathrm{AMO}}_{n}$ is $\binom{n}{2}$ and the CNF complexity of $\operatorname{\mathrm{EO}}_{n}$ is $\binom{n}{2}+1$.

Lemma 5.1**.**

Let $\mathcal{A}(n)$ denote the minimum size of a PC encoding of $\operatorname{\mathrm{AMO}}_{n}$ and let $\mathcal{E}(n)$ denote the minimum size of a PC encoding of $\operatorname{\mathrm{EO}}_{n}$. Then, we have

[TABLE]

Proof.

Representations of $\operatorname{\mathrm{AMO}}_{n}$ and $\operatorname{\mathrm{EO}}_{n}$ containing all the prime implicates achieve these bounds, are the smallest possible, and are propagation complete. This implies the required upper bounds on $\mathcal{A}(n)$, $\mathcal{E}(n)$, and $\mathcal{P}(n)$ for $n=2,3$.

Lemma 3.6 implies that if a function has a representation of size at most $4$, then the size of the smallest encoding (not necessarily propagation complete) is equal to the size of the smallest representation. This implies the stated values of $\mathcal{A}(n)$ and $\mathcal{E}(n)$.

As explained in Section 3.4, every P-encoding with $n$ input variables is either an encoding of $\operatorname{\mathrm{AMO}}_{n}$ or an encoding of $\operatorname{\mathrm{EO}}_{n}$. Hence, the lower bounds from the previous paragraph hold also for P-encodings and this implies the stated values of $\mathcal{P}(n)$. ∎

Let us prove additional properties of sets $L_{\varphi,i}$ introduced at the end of Section 4.

Lemma 5.2**.**

Let $\varphi$ be a P-encoding with input variables $(x_{1},\ldots,x_{n})$ in regular form. Let $i,j,k$ be different indices with $L_{\varphi,i}=\{g,h_{1}\}$, $L_{\varphi,j}=\{g,h_{2}\}$, and $L_{\varphi,k}=\{g,h_{3}\}$ for $g,h_{1},h_{2},h_{3}\in\mathrm{lit}(\mathbf{y})$. Then variables $\mathrm{var}(h_{1})$, $\mathrm{var}(h_{2})$, and $\mathrm{var}(h_{3})$ are pairwise different.

Proof.

Let us show by contradiction that $\mathrm{var}(h_{1})\neq\mathrm{var}(h_{2})$. To this end, assume $\mathrm{var}(h_{1})=\mathrm{var}(h_{2})$. Since $L_{\varphi,i}\neq L_{\varphi,j}$ by Lemma 4.8, we have $h_{1}=\neg h_{2}$. By condition (P2), $\varphi\wedge x_{k}\vdash_{1}\neg x_{i}$ and $\varphi\wedge x_{k}\vdash_{1}\neg x_{j}$. Since $\varphi\wedge x_{k}\vdash_{1}g$, necessarily $\varphi\wedge x_{k}\vdash_{1}\neg h_{1}$ and $\varphi\wedge x_{k}\vdash_{1}\neg h_{2}$. However, then $\varphi\wedge x_{k}\vdash_{1}\bot$ which is in contradiction with (P1).

The remaining cases, i.e. $\mathrm{var}(h_{1})\neq\mathrm{var}(h_{3})$ and $\mathrm{var}(h_{2})\neq\mathrm{var}(h_{3})$ are symmetrical. ∎

Using Lemma 5.2 for all triples of indices of input variables, we obtain the following.

Corollary 5.3**.**

Assume, $\varphi(\mathbf{x},\mathbf{y})$ is a P-encoding with input variables $\mathbf{x}=(x_{1},\ldots,x_{n})$ in regular form. Let

[TABLE]

where $h\in\mathrm{lit}(\mathbf{y})$, and define

[TABLE]

If $|I_{h}|\geq 3$, then $L_{h}$ contains literals on different variables and $|L_{h}|=|I_{h}|+1$.

Proof.

This is a corollary of Lemma 5.2. If we remove literal $h$ from each $L_{\varphi,i}$, $i\in I_{h}$, then the remaining literals are on pairwise different variables different from $\mathrm{var}(h)$. ∎

We are now ready to show the lower bound on the size of a P-encoding in regular form.

Lemma 5.4**.**

If $\varphi(\mathbf{x},\mathbf{y})$ is a P-encoding with $n\geq 7$ input variables $\mathbf{x}=(x_{1},\ldots,x_{n})$ in regular form, then $|\varphi|\geq 2n+\sqrt{n-3/4}-3/2$.

Proof.

Since the formula $\varphi(\mathbf{x},\mathbf{y})$ contains $2n$ clauses of type Q, it is sufficient to prove that it contains at least $\sqrt{n-3/4}-3/2$ clauses of type R.

Let $L=\bigcup_{i=1}^{n}L_{\varphi,i}$ be the set of auxiliary literals in clauses of type Q. For each $h\in L$, let $I_{h}$ and $L_{h}$ be defined as in Corollary 5.3. Choose $g\in L$ that maximizes $\left|I_{g}\right|$, fix some $i\in I_{g}$ and denote $M_{i}={\cal U}_{\varphi}(x_{i})\cap\mathrm{lit}(\mathbf{y})$. Each literal in $M_{i}\setminus L_{\varphi,i}$ is derived by unit propagation from $\varphi\wedge x_{i}$ using a different clause of type R. Hence, the number of the clauses of type R is at least $|M_{i}|-2$.

For each $j\in\{1,\ldots,n\}\setminus\{i\}$, the literal $\neg x_{j}$ must be derived from some $h\in M_{i}$ using a clause of type Q containing $\neg h$. As $\left|I_{\neg h}\right|\leq\left|I_{g}\right|$ for every $\neg h\in L$, each $h\in M_{i}$ can derive $\neg x_{j}$ for at most $\left|I_{g}\right|$ values of $j$. Thus,

[TABLE]

If $\left|I_{g}\right|\geq 3$, then according to Corollary 5.3, we get $|L_{g}|=|I_{g}|+1$. In order to derive all $\neg x_{j}$, $j\in I_{g}\setminus\{i\}$ from $\varphi\wedge x_{i}$, $M_{i}$ has to contain the negations of the literals in $L_{g}\setminus L_{\varphi,i}$. Since $M_{i}$ contains also $L_{\varphi,i}$ and these literals are on variables not in $\mathrm{var}(L_{g}\setminus L_{\varphi,i})$, we have

[TABLE]

Combining the two bounds, we get

[TABLE]

as follows. If $\left|I_{g}\right|\geq 3$, the claims (21) and (20) apply. If $\left|I_{g}\right|\leq 2$, observe that by (20), $\left|M_{i}\right|\geq(n-1)/2\geq 3\geq|I_{g}|+1$, since $n\geq 7$.

For $s\geq 1$, the smallest value of the function $s\mapsto\max\{s+1,(n-1)/s\}$ is $s_{0}+1$ for $s_{0}\geq 1$, such that $s_{0}+1=(n-1)/s_{0}$. Hence, we have $|M_{i}|\geq\sqrt{n-3/4}+1/2$ and the number of clauses of type R is at least $\sqrt{n-3/4}-3/2$. ∎

Let us conclude the section with the following theorem which represents the statement 1 for $\mathcal{P}(n)$ and statement 2 of Theorem 2.8.

Theorem 5.5**.**

For $n\geq 3$, the minimum size $\mathcal{P}(n)$ of a P-encoding with $n$ input variables satisfies

If $n\leq 8$, then $\mathcal{P}(n)=3n-6$. 2. 2.

If $n\geq 9$, then $\mathcal{P}(n)\geq 2n+\sqrt{n}-2$.

Proof.

We treat the two claims separately:

It was shown in Lemma 3.1 and Lemma 2.6 that $\mathcal{P}(n)\leq 3n-6$. To show that $\mathcal{P}(n)\geq 3n-6$ for $3\leq n\leq 8$, we proceed by induction on $n$. The basis $\mathcal{P}(3)=3$ is given by Lemma 5.1. Let $\varphi$ be a prime P-encoding with $n\geq 4$ input variables of size $\mathcal{P}(n)$. Theorem 2.10 implies that either $\left|\varphi\right|\geq\mathcal{P}(n-1)+3$ or $\varphi$ is in regular form. In the first case, the induction hypothesis implies

[TABLE]

If $\varphi$ is in regular form and $n\leq 6$, then the structure of the regular form implies $|\varphi|\geq 2n\geq 3n-6$. If $\varphi$ is in regular form and $7\leq n\leq 8$, then Lemma 5.4 implies

[TABLE] 2. 2.

We proceed by induction on $n$ using the previous case as the basis. Let $\varphi$ be a prime P-encoding with $n\geq 9$ input variables of size $\mathcal{P}(n)$. It follows from Theorem 2.10 that either $\left|\varphi\right|\geq\mathcal{P}(n-1)+3$ or $\varphi$ is in regular form. In the first case, observe that:

• •

If $n=9$, we obtain $\mathcal{P}(n-1)+3=21>2n+\sqrt{n}-2$ by the first claim of this theorem.

• •

If $n\geq 10$, the induction hypothesis and $\sqrt{n-1}+1>\sqrt{n}$ imply

[TABLE]

as required.

If $\varphi$ is in regular form, Lemma 5.4 implies

[TABLE]

as required.

∎

Note that the upper bound $3n-6$ in Theorem 5.5 for $n\leq 8$ is achieved by the sequential encoding of $\operatorname{\mathrm{AMO}}_{n}$ described in Section 3.1. It follows that actually $\mathcal{P}(n)=\mathcal{A}(n)=3n-6$ in this case where $\mathcal{A}(n)$ denotes the minimum size of a PC encoding of $\operatorname{\mathrm{AMO}}_{n}$.

6 A Lower Bound For 2-CNF P-Encodings

In this section we prove the remaining parts of Theorem 2.8. In particular, we prove a lower bound $2n+2\sqrt{n}-3$ on $\mathcal{P}_{2}(n)$ and prove that $\mathcal{P}_{2}(n)$ is equal to the minimum size of a 2-CNF encoding of $\operatorname{\mathrm{AMO}}_{n}$, even if we do not require propagation completeness. Importance of the special case of 2-CNF encodings for $\operatorname{\mathrm{AMO}}_{n}$ comes from the fact that the smallest known encodings are in 2-CNF as well as all the other encodings suggested in the literature.

We have already argued at the beginning of Section 2.5 that a 2-CNF P-encoding $\varphi$ with $n\geq 3$ input variables cannot encode $\operatorname{\mathrm{EO}}_{n}$. It follows by Lemma 3.3 that $\varphi$ is an encoding of $\operatorname{\mathrm{AMO}}_{n}$. The correspondence holds also in the opposite direction in the following sense.

Lemma 6.1**.**

A minimum size 2-CNF encoding of $\operatorname{\mathrm{AMO}}_{n}$ does not have unit implicates, is a prime P-encoding, and its size is equal to $\mathcal{P}_{2}(n)$.

Proof.

Let $\varphi(\mathbf{x},\mathbf{y})$ be a minimum size 2-CNF encoding of $\operatorname{\mathrm{AMO}}_{n}$. Since $\operatorname{\mathrm{AMO}}_{n}$ does not have unit implicates, $\varphi$ does not have a unit implicate on an input variable. Assume for a contradiction that $\varphi$ has a unit implicate $l$ on an auxiliary variable. Setting this variable, so that $l$ is satisfied, leads to a PC encoding of $\operatorname{\mathrm{AMO}}_{n}$. Moreover, since the literal $l$ has at least one occurence in $\varphi$, at least one clause can be removed and this contradicts the assumption. Hence, $\varphi$ does not have unit implicates. It follows that $\varphi$ is a prime 2-CNF and by results of [3] we get that $\varphi$ is propagation complete. It follows that it is a P-encoding and thus $|\varphi|\geq\mathcal{P}_{2}(n)$. On the other hand, we have observed above that a 2-CNF P-encoding with $n\geq 3$ inputs is an encoding of $\operatorname{\mathrm{AMO}}_{n}$ and thus $\mathcal{P}_{2}(n)\geq|\varphi|$. Hence, we have $|\varphi|=\mathcal{P}_{2}(n)$ for all $n\geq 1$, since the cases $n\leq 2$ can easily be verified. ∎

It follows that refering to minimum size 2-CNF encodings of $\operatorname{\mathrm{AMO}}_{n}$ is the same as refering to minimum size 2-CNF P-encodings. In order to prove a lower bound on the size of a 2-CNF encoding of $\operatorname{\mathrm{AMO}}_{n}$, we use Theorem 2.10 similarly as in Section 5 to handle encodings, which are not in regular form. However, the analysis of encodings in regular form is different and implies a stronger lower bound.

One of the differences in case of 2-CNF formulas is that a unit resolution derivation can be reversed in the following sense. If one step of unit propagation can derive $h$ from $\neg g$, then we can also derive $g$ from $\neg h$ in one step, since both these steps are possible if and only if the clause $g\vee h$ is contained in the formula. Due to this, it is useful to represent a 2-CNF formula with an implication graph introduced in [2] as follows. For a formula $\varphi=\varphi(\mathbf{z})$, let $G_{\varphi}=(V,E)$ be a directed graph with the set of vertices $V=\mathrm{lit}(\mathbf{z})$ and with the set of directed edges $E$ containing $(\neg g,h)$ and $(\neg h,g)$ for each clause $(g\vee h)\in\varphi$. These two directed edges (arcs) represent the implications $\neg g\to h$ and $\neg h\to g$, respectively. This graph is skew-symmetric (also called duality property in [12] and mirror property in [11]), meaning that $(g,h)\in E$ if and only if $(\neg h,\neg g)\in E$. We can exploit the properties of the implication graph to show stronger properties of the sets of literals $L_{\varphi,i}$ defined in (16) than in the case of general CNF encodings. In particular, we show that the part of the analysis that determines the constant of the term $\sqrt{n}$ in the lower bound can be reduced to the case where the sets $L^{\mathrm{v}}_{\varphi,i}=\mathrm{var}(L_{\varphi,i})$ are pairwise different for $i=1,\ldots,n$. Recall that in the general case we were only able to show in Lemma 4.8 that the sets $L_{\varphi,i}$ are pairwise different.

The following two basic properties of 2-CNF formulas are used implicitly throughout this section. See, e.g., Theorem 5.6 in [11] for the omitted proof of Lemma 6.2.

Lemma 6.2**.**

Let $\varphi(\mathbf{z})$ be a 2-CNF formula. Then, for each $g\in\mathrm{lit}(\mathbf{z})$, we have $\varphi\vdash_{1}g$ if and only if there is a literal $h$ which forms a unit clause in $\varphi$ and there is a path from $h$ to $g$ in $G_{\varphi}$.

We are mainly interested in the properties of the minimum size 2-CNF encodings of $\operatorname{\mathrm{AMO}}_{n}$ and these encodings do not contain unit clauses by Lemma 6.1.

Lemma 6.3**.**

Let $\varphi(\mathbf{z})$ be a 2-CNF formula not containing unit clauses and let $g,h\in\mathrm{lit}(\mathbf{z})$. Then the following conditions are equivalent:

1. (i)

$\varphi\wedge g\vdash_{1}\neg h$, 2. (ii)

$\varphi\wedge h\vdash_{1}\neg g$.

Proof.

Assume (i). By Lemma 6.2, there is a path in $G_{\varphi}$ from a unit clause in the formula $\varphi\wedge g$ to $\neg h$. By the assumption, this path starts in $g$. Since $G_{\varphi}$ is skew-symmetric, it contains also a path from $h$ to $\neg g$ and, hence, we have (ii). By symmetry, also (ii) implies (i). ∎

The following series of statements analyze properties of minimum size 2-CNF encodings of $\operatorname{\mathrm{AMO}}_{n}$ and finally leads to Theorem 6.10.

Lemma 6.4**.**

Let $\varphi(\mathbf{x},\mathbf{y})$ be a minimum size 2-CNF encoding of $\operatorname{\mathrm{AMO}}_{n}$ and let $i,j\in\{1,\dots,n\}$, $i\neq j$. Then there exist literals $e_{0},e_{1},\dots,e_{p}\in\mathrm{lit}(\mathbf{x}\cup\mathbf{y})$, $p\geq 1$, such that:

1. (i)

$e_{0}=x_{i}$, $e_{p}=\neg x_{j}$, and $e_{0},e_{1},\dots,e_{p}$ form a path in $G_{\varphi}$, 2. (ii)

$e_{1},\dots,e_{p-1}$* are pairwise distinct literals from $\mathrm{lit}(\mathbf{y})$.*

Proof.

By assumption, $\varphi\not\vdash_{1}\neg x_{j}$ and $\varphi\wedge x_{i}\vdash_{1}\neg x_{j}$. Hence, by Lemma 6.2, there is a path from $x_{i}$ to $\neg x_{j}$ in $G_{\varphi}$. Let $x_{i}=e_{0},e_{1},\dots,e_{p}=\neg x_{j}$ be a shortest such path. If $p=1$, the proof is finished. Suppose that $p\geq 2$ and let us show that the path meets (ii). Since the sequence is the shortest possible and $\varphi\wedge x_{i}\not\vdash_{1}\bot$, the literals $e_{0},\dots,e_{p}$ are on pairwise different variables. Assume for a contradiction that there is a literal $e_{q}$ on an input variable $x_{k}$, $k\not\in\{i,j\}$. If $e_{q}=x_{k}$, then $\varphi\wedge x_{i}\vdash_{1}x_{k}$ and if $e_{q}=\neg x_{k}$, then $\varphi\wedge\neg x_{k}\vdash_{1}\neg x_{j}$. Both these cases contradict Lemma 4.1. ∎

The following proposition shows that we can restrict our consideration to 2-CNF encodings of $\operatorname{\mathrm{AMO}}_{n}$ with no positive occurrences of input variables. This is a difference from the case of general PC encodings of $\operatorname{\mathrm{AMO}}_{n}$. In Section 7, we present an example of an irredundant prime PC encoding of $\operatorname{\mathrm{AMO}}_{n}$ of size $\Theta(n^{2})$ containing positive occurrences of input variables. We believe that positive occurrences of input variables cannot occur in a minimum size prime PC encoding of $\operatorname{\mathrm{AMO}}_{n}$, however, we do not have a proof of this conjecture.

Lemma 6.5**.**

A minimum size 2-CNF encoding of $\operatorname{\mathrm{AMO}}_{n}$ contains no positive occurrence of an input variable.

Proof.

Assume, $\varphi$ is a 2-CNF encoding of $\operatorname{\mathrm{AMO}}_{n}$ of minimum size and contains a clause containing a positive literal on an input variable. Let $\varphi^{\prime}$ be the formula obtained by removing all such clauses from $\varphi$. Since $\varphi^{\prime}$ is a subset of $\varphi$, it satisfies (P1). Moreover, by Lemma 6.4, for every $i,j\in\{1,\ldots,n\}$, there is a series of resolutions witnessing $\varphi\wedge x_{i}\vdash_{1}\neg x_{j}$ that does not derive any literal on an input variable except of $\neg x_{j}$. The clauses used in this series of resolutions contain only the literals $\neg x_{i}$, $\neg x_{j}$, and literals on auxiliary variables. Hence, this series of resolutions can be used also in $\varphi^{\prime}$ and this implies that $\varphi^{\prime}$ satisfies (P2). This is a contradiction with minimality of $\varphi$. ∎

Using Lemma 6.1 and Theorem 2.10, we obtain that a minimum size 2-CNF encoding $\varphi$ of $\operatorname{\mathrm{AMO}}_{n}$ either satisfies $|\varphi|\geq\mathcal{P}_{2}(n-1)+3$ or it is in regular form introduced in Definition 2.9. The purpose of several following propositions concluded by Proposition 6.9 is to show that in case of 2-CNF encodings we can reduce the analysis to an even more restricted form. Recall the notation $L_{\varphi,i}$ from (16). In addition to the conditions of the regular form this restricted regular form requires that the following two conditions are satisfied.

• •

The sets $L^{\mathrm{v}}_{\varphi,1},\ldots,L^{\mathrm{v}}_{\varphi,n}$ are pairwise distinct.

• •

For any three different indices $r,s,t\in\{1,\ldots,n\}$ we have $\left|L^{\mathrm{v}}_{\varphi,r}\cup L^{\mathrm{v}}_{\varphi,s}\cup L^{\mathrm{v}}_{\varphi,t}\right|>3$.

Lemma 6.6 and Proposition 6.7 show how to deal with encodings not satisfying the first of these conditions.

Lemma 6.6**.**

Let $\varphi(\mathbf{x},\mathbf{y})$ be a minimum size 2-CNF encoding of $\operatorname{\mathrm{AMO}}_{n}$ in regular form, $n\geq 3$. Let $r,s\in\{1,\ldots,n\}$ be different and let us suppose $L^{\mathrm{v}}_{\varphi,r}=L^{\mathrm{v}}_{\varphi,s}$ and $L_{\varphi,r}=\{g,h\}$ for $g,h\in\mathrm{lit}(\mathbf{y})$. Then $L_{\varphi,s}=\{\neg g,\neg h\}$.

Proof.

Assume without loss of generality $r=1$ and $s=2$. Hence, we have $L_{\varphi,1}=\{g,h\}$. By Lemma 4.8, $L_{\varphi,2}\not=\{g,h\}$. In order to prove the lemma, it is sufficient to exclude the cases $L_{\varphi,2}=\{\neg g,h\}$ and $L_{\varphi,2}=\{g,\neg h\}$. Since these cases are symmetrical, we consider only the first of them.

Assume $L_{\varphi,2}=\{\neg g,h\}$ and let

[TABLE]

We show that $\varphi^{\prime}$ satisfies the conditions (P1) and (P2), thus it encodes $\operatorname{\mathrm{AMO}}_{n}$, which contradicts minimality of $\varphi$.

1. (P1)

For every $i$, the formula $\varphi\wedge x_{i}$ is satisfiable. Since the added clause $\neg x_{1}\vee\neg x_{2}$ is an implicate of $\operatorname{\mathrm{AMO}}_{n}$ and removing clauses preserves any satisfying assignments, the formula $\varphi^{\prime}\wedge x_{i}$ is satisfiable as well. 2. (P2)

Let us prove $\varphi^{\prime}\wedge x_{i}\vdash_{1}\neg x_{j}$ for every $i,j\in\{1,\dots,n\}$, $i\neq j$. Due to Lemma 6.3, we can assume $i<j$. If $i,j\not\in\{1,2\}$, then $\varphi^{\prime}\wedge x_{i}\vdash_{1}\neg x_{j}$ using the chain $e_{0},\dots,e_{p}$ provided by Lemma 6.4 applied to $\varphi$. This chain is not affected by (22) and can thus be used in $\varphi^{\prime}$ as well. Let $i\in\{1,2\}$. The case $i=1,\,j=2$ is trivial, so let $j>2$. The set ${\cal U}_{\varphi}(x_{j})$ contains a negation of a literal from each of the sets $L_{\varphi,1}$ and $L_{\varphi,2}$. Since it cannot contain both $g$ and $\neg g$, it contains $\neg h$ and by Lemma 6.4, there is a path in $G_{\varphi}$ from $x_{j}$ to $\neg h$ that does not contain a literal on an input variable except of the starting node. By Lemma 6.3, this implies that $\varphi\wedge h\vdash_{1}\neg x_{j}$ by a path that does not use the clauses omitted in $\varphi^{\prime}$, so we have $\varphi^{\prime}\wedge x_{i}\vdash_{1}\neg x_{j}$.

∎

The size of an encoding not satisfying the first condition of restricted regular form can be estimated as follows.

Proposition 6.7**.**

Let $n\geq 5$ and let $\varphi(\mathbf{x},\mathbf{y})$ be a minimum size 2-CNF encoding of $\operatorname{\mathrm{AMO}}_{n}$ with the minimum number of auxiliary variables and, moreover, assume that $\varphi$ is in regular form. If there are two different indices $r,s\in\{1,\ldots,n\}$, such that $L_{\varphi,r}=\{g,h\}$ and $L_{\varphi,s}=\{\neg g,\neg h\}$ for $g,h\in\mathrm{lit}(\mathbf{y})$, then $\left|\varphi\right|\geq\mathcal{P}_{2}(n-2)+7$.

Proof.

Without loss of generality, assume $r=1$ and $s=2$. Hence, $L_{\varphi,1}=\{g,h\}$ and $L_{\varphi,2}=\{\neg g,\neg h\}$. Denote

[TABLE]

For a proof of $A\cup B=\{3,\dots,n\}$, assume $j\geq 3$. The set ${\cal U}_{\varphi}(x_{j})$ contains a negation of a literal from each of the sets $L_{\varphi,1}=\{g,h\}$ and $L_{\varphi,2}=\{\neg g,\neg h\}$, however, it cannot contain complementary literals. It follows that either ${\cal U}_{\varphi}(x_{j})=\{\neg g,h\}$ or ${\cal U}_{\varphi}(x_{j})=\{g,\neg h\}$, so $j\in A\cup B$.

Let us prove that $A\neq\emptyset$ and $B\neq\emptyset$ by contradiction. If $A=\emptyset$, we prove that the formula $\varphi^{\prime}=\varphi\setminus\{\neg x_{1}\vee g\}$ encodes $\operatorname{\mathrm{AMO}}_{n}(\mathbf{x})$ by verifying the conditions (P1) and (P2) in contradiction to minimality of $\varphi$:

1. (P1)

For every $i\in\{1,\ldots,n\}$, $\varphi^{\prime}\wedge x_{i}$ is satisfiable, since $\varphi\wedge x_{i}$ is satisfiable and $\varphi^{\prime}$ is a subset of $\varphi$. 2. (P2)

Let us verify $\varphi\wedge x_{i}\vdash_{1}\neg x_{j}$ for each $i,j\in\{1,2\}\cup B$, $i\neq j$. Due to Lemma 6.3, we can assume $i<j$.

• •

If $i=1$, then $j\in B\cup\{2\}$. Thus, $\varphi\wedge x_{1}\vdash_{1}h$ and $\varphi\wedge x_{j}\vdash_{1}\neg h$. By Lemma 6.3 we get $\varphi\wedge h\vdash_{1}\neg x_{j}$ and, hence, $\varphi\wedge x_{1}\vdash_{1}\neg x_{j}$.

• •

If $i\geq 2$, then Lemma 6.4 guarantees that $\varphi\wedge x_{i}\vdash_{1}\neg x_{j}$ is witnessed by a series of unit resolutions not using the clause $\neg x_{1}\vee g$.

Similarly, if $B=\emptyset$, then $\varphi\setminus\{\neg x_{1}\vee h\}$ encodes $\operatorname{\mathrm{AMO}}_{n}(\mathbf{x})$ in contradiction to minimality of $\varphi$. Altogether, $A\neq\emptyset$ and $B\neq\emptyset$.

For the last step of the proof, consider the formula

[TABLE]

where $\gamma=\{C\in\varphi\mid g\in C\text{ or }\neg g\in C\}$. By Lemma 3.6 we get that $|\gamma|\geq 5$ and $\left|\varphi\right|\geq|\varphi^{\prime}|+7$. Let us show that $\varphi^{\prime}$ encodes $\operatorname{\mathrm{AMO}}_{n-2}(x_{3},\dots,x_{n})$ by verifying the conditions (P1) and (P2).

1. (P1)

For every $i\in\{3,\ldots,n\}$, $\varphi^{\prime}\wedge x_{i}$ is satisfiable, since $\varphi\wedge x_{i}$ is satisfiable and $\varphi^{\prime}$ is a subset of $\varphi$. 2. (P2)

Let us verify $\varphi^{\prime}\wedge x_{i}\vdash_{1}\neg x_{j}$ for each $i,j\in\{3,\dots,n\}$. Each of the sets $\{g,h\}$, $\{g,\neg h\}$, $\{\neg g,h\}$, $\{\neg g,\neg h\}$ is a subset of ${\cal U}_{\varphi}(x_{k})$ for some $k\in\{1,\ldots,n\}$. Hence, each of the formulas

[TABLE]

is satisfiable. Distinguish the following cases:

• •

If $i\in A$ and $j\in B$, let $e_{0},\dots,e_{p}\in\mathrm{lit}(\mathbf{x}\cup\mathbf{y})$ be a chain of literals derived in a series of unit resolutions witnessing $\varphi\wedge x_{i}\vdash_{1}h$. If $e_{q}\in\{g,\neg g\}$ for some $q\in\{1,\dots,p-1\}$, then $\varphi\wedge e_{q}\vdash_{1}h$, which contradicts $\varphi\wedge e_{q}\wedge\neg h$ being satisfiable. Thus, the chain is present in $\varphi^{\prime}$ as well and we have $\varphi^{\prime}\wedge x_{i}\vdash_{1}h$. On the other hand, we have $\varphi\wedge x_{j}\vdash_{1}\neg h$ and by a similar argument, we obtain $\varphi^{\prime}\wedge x_{j}\vdash_{1}\neg h$. This implies $\varphi^{\prime}\wedge h\vdash_{1}\neg x_{j}$ and thus $\varphi^{\prime}\wedge x_{i}\vdash_{1}\neg x_{j}$.

• •

The case of $i\in B$, $j\in A$ follows from the previous one by Lemma 6.3.

• •

If $i,j\in A$, let $e_{0},\dots,e_{p}\in\mathrm{lit}(\mathbf{x}\cup\mathbf{y})$ be a chain of literals derived in a series of unit resolutions witnessing $\varphi\wedge x_{i}\vdash_{1}\neg x_{j}$ according to Lemma 6.4 that does not use the clauses $\neg x_{1}\vee h$ and $\neg x_{2}\vee\neg h$. Assume, for a contradiction, $e_{q}\in\{g,\neg g\}$ for some $q\in\{1,\dots,p-1\}$. Then, we have either $\varphi\wedge x_{i}\vdash_{1}g$ or $\varphi\wedge x_{j}\vdash_{1}g$ by Lemma 6.3. This is not possible, since $i,j\in A$ implies $\varphi\wedge x_{i}\vdash_{1}\neg g$ and $\varphi\wedge x_{j}\vdash_{1}\neg g$. Thus, the chain is present in $\varphi^{\prime}$ as well and we have $\varphi^{\prime}\wedge x_{i}\vdash_{1}\neg x_{j}$.

• •

The case of $i,j\in B$ is analogous to case $i,j\in A$. In this case, we use that $i,j\in B$ implies $\varphi\wedge x_{i}\vdash_{1}g$ and $\varphi\wedge x_{j}\vdash_{1}g$.

Hence, $\varphi^{\prime}$ encodes $\operatorname{\mathrm{AMO}}_{n-2}$ and $\left|\varphi\right|\geq|\varphi^{\prime}|+7\geq\mathcal{P}_{2}(n-2)+7$ as required. ∎

The following proposition will be used in the proof of Theorem 6.10 to handle the encodings not satisfying the second condition of the restricted regular form. These are encodings, for which there is a triangle in the graph whose vertices are auxiliary variables and the edges are the sets $L^{\mathrm{v}}_{\varphi,i}$ for $i\in\{1,\ldots,n\}$.

Proposition 6.8**.**

Let $n\geq 4$ and let $\varphi(\mathbf{x},\mathbf{y})$ be a minimum size 2-CNF encoding of $\operatorname{\mathrm{AMO}}_{n}$ with the minimum number of auxiliary variables and, moreover, assume that $\varphi$ is in regular form. If there are different indices $r,s,t\in\{1,\ldots,n\}$, such that

$L^{\mathrm{v}}_{\varphi,r}$, $L^{\mathrm{v}}_{\varphi,s}$, and $L^{\mathrm{v}}_{\varphi,t}$ are pairwise distinct, 2. 2.

$\left|L^{\mathrm{v}}_{\varphi,r}\cup L^{\mathrm{v}}_{\varphi,s}\cup L^{\mathrm{v}}_{\varphi,t}\right|=3$,

then $\left|\varphi\right|\geq\mathcal{P}_{2}(n-2)+6$.

Proof.

Without loss of generality, let us assume that $r=1$, $s=2$, and $t=3$ and let $L=L_{\varphi,1}\cup L_{\varphi,2}\cup L_{\varphi,3}$. Since $\varphi$ is in regular form, we have $\left|L_{\varphi,1}\right|=\left|L_{\varphi,2}\right|=\left|L_{\varphi,3}\right|=2$. Let us distinguish four cases according to the size of $L$. Note that there are $|L|-3$ variables in $L^{\mathrm{v}}_{\varphi,1}\cup L^{\mathrm{v}}_{\varphi,2}\cup L^{\mathrm{v}}_{\varphi,3}$ that occur with both signs in $L$.

If $|L|=3$, then

[TABLE]

for some $g_{\mathrm{A}},g_{\mathrm{B}},g_{\mathrm{C}}\in\mathrm{lit}(\mathbf{y})$. The clause $D=\neg g_{\mathrm{A}}\vee\neg g_{\mathrm{B}}\vee\neg g_{\mathrm{C}}$ is an implicate of $\varphi$ because $\varphi\land\neg D=\varphi\land g_{\mathrm{A}}\land g_{\mathrm{B}}\land g_{\mathrm{C}}$ is unsatisfiable. Indeed, any satisfying assignment of $\varphi\wedge g_{\mathrm{A}}\wedge g_{\mathrm{B}}\wedge g_{\mathrm{C}}$ would remain satisfying even if any two of the variables $x_{1},x_{2},x_{3}$ are changed to 1 which would be in contradiction with the fact that $\varphi$ encodes $\operatorname{\mathrm{AMO}}_{n}$. On the other hand, since $\varphi$ satisfies (P1), any two of the literals $g_{\mathrm{A}},g_{\mathrm{B}},g_{\mathrm{C}}\in\mathrm{lit}(\mathbf{y})$ can be satisfied in a satisfying assignment of $\varphi$. Hence, $D$ is a prime implicate, which contradicts $\varphi$ being a 2-CNF formula. 2. 2.

If $|L|=4$, we can assume due to symmetry that

[TABLE]

for some $g_{\mathrm{A}},g_{\mathrm{B}},g_{\mathrm{C}}\in\mathrm{lit}(\mathbf{y})$. The set ${\cal U}_{\varphi}(x_{3})$ contains the literals $g_{\mathrm{B}}$ and $g_{\mathrm{C}}$ and has a non-empty intersection with each of the sets $\{\neg g_{\mathrm{A}},\neg g_{\mathrm{B}}\}$, $\{g_{\mathrm{A}},\neg g_{\mathrm{C}}\}$. One can verify that this implies that for some $e\in\{g_{\mathrm{A}},g_{\mathrm{B}},g_{\mathrm{C}}\}$, the set ${\cal U}_{\varphi}(x_{3})$ contains both $e$ and $\neg e$. This is a contradiction with (P1). 3. 3.

If $|L|=5$, we can assume due to symmetry that

[TABLE]

for some $g_{\mathrm{A}},g_{\mathrm{B}},g_{\mathrm{C}}\in\mathrm{lit}(\mathbf{y})$. Consider the formula $\varphi^{\prime}$ obtained from $\varphi$ by omitting all clauses containing variables $x_{1}$, $x_{2}$, and $x_{3}$. Let $x_{n+1}$ be a new input variable and consider the formula

[TABLE]

Since $x_{n+1}$ has no occurence in $\varphi^{\prime}$, this substitution is the same as renaming $\mathrm{var}(g_{\mathrm{C}})$ to $x_{n+1}$ or to $\neg x_{n+1}$, so that the literal $g_{\mathrm{C}}$ becomes equal to $x_{n+1}$. Formula $\psi$ has $n-2$ input variables $x_{4},\ldots,x_{n},x_{n+1}$ and $\left|\varphi\right|\geq\left|\psi\right|+6$. Let us check the conditions (P1) and (P2) to show that $\psi$ is an encoding of $\operatorname{\mathrm{AMO}}_{n-2}$:

1. (P1)

If $i\in\{4,\ldots,n\}$, a satisfying assignment of $\varphi\wedge x_{i}$ is a satisfying assignment of $\varphi^{\prime}\wedge x_{i}$. Moreover, any satisfying assignment of $\varphi\wedge x_{2}$ satisfies $\varphi\wedge g_{\mathrm{C}}$ and, hence, also $\varphi^{\prime}\wedge g_{\mathrm{C}}$. Renaming $g_{\mathrm{C}}$ to $x_{n+1}$ as described above in $\varphi^{\prime}\wedge x_{i}$ and $\varphi^{\prime}\wedge g_{\mathrm{C}}$ yields the formulas $\psi\wedge x_{i}$ and $\psi\wedge x_{n+1}$, so these formulas are satisfiable as well. 2. (P2)

Let us check $\psi\wedge x_{i}\vdash_{1}\neg x_{j}$ for each $i,j\in\{4,\dots,n+1\}$, $i<j$. If $j\leq n$, observe that the series of unit resolutions witnessing $\varphi\wedge x_{i}\vdash_{1}\neg x_{j}$ according to Lemma 6.4 does not use the omitted clauses and, hence, is present also in $\varphi^{\prime}$ and $\psi$. If $j=n+1$, note that ${\cal U}_{\varphi}(x_{i})$ contains a negation of a literal from each of the sets $L_{\varphi,1}$, $L_{\varphi,2}$, $L_{\varphi,3}$ and does not contain complementary literals. This implies $\neg g_{\mathrm{C}}\in{\cal U}_{\varphi}(x_{i})$ and, hence, $\neg x_{n+1}\in{\cal U}_{\psi}(x_{i})$. 4. 4.

If $|L|=6$, we can assume due to symmetry that

[TABLE]

for some $g_{\mathrm{A}},g_{\mathrm{B}},g_{\mathrm{C}}\in\mathrm{lit}(\mathbf{y})$. Note that the collection of the sets $\{L_{\varphi,1},L_{\varphi,2},L_{\varphi,3}\}$ is invariant under a cyclic shift of the list $(g_{\mathrm{A}},g_{\mathrm{B}},g_{\mathrm{C}})$. Clearly, $\varphi\wedge g_{\mathrm{A}}\not\vdash_{1}g_{\mathrm{B}}$, since otherwise $\varphi\wedge x_{1}\vdash_{1}\bot$ in contradiction to (P1). By symmetry, all of the following statements are satisfied

[TABLE]

Assume for a contradiction that any two of the statements

[TABLE]

are satisfied. For each pair of these statements, we get a contradiction with (23). Hence, at most one of these statements is satisfied. It follows that we can assume without loss of generality

[TABLE]

The following claim will be used later.

Claim. If $k\geq 4$, then the set ${\cal U}_{\varphi}(x_{k})$ contains either all of the literals $g_{\mathrm{A}},g_{\mathrm{B}},g_{\mathrm{C}}$ or all of the literals $\neg g_{\mathrm{A}},\neg g_{\mathrm{B}},\neg g_{\mathrm{C}}$.

Proof.

Since $\varphi\wedge x_{k}\vdash_{1}\neg x_{1}$, we have $g_{\mathrm{B}}\in{\cal U}_{\varphi}(x_{k})$ or $\neg g_{\mathrm{A}}\in{\cal U}_{\varphi}(x_{k})$. In the first case, the set ${\cal U}_{\varphi}(x_{k})$ contains $g_{\mathrm{C}}$ to derive $\neg x_{3}$ and contains $g_{\mathrm{A}}$ to derive $\neg x_{2}$. In the second case, the set ${\cal U}_{\varphi}(x_{k})$ contains $\neg g_{\mathrm{C}}$ to derive $\neg x_{2}$ and contains $\neg g_{\mathrm{B}}$ to derive $\neg x_{3}$. ∎

By Lemma 3.6 we get that the variable $\mathrm{var}(g_{\mathrm{A}})$ occurs in at least 5 clauses. Thus, the formula $\psi$ obtained from $\varphi$ by omitting all clauses containing some of the literals $\neg x_{1}$, $\neg x_{2}$, $g_{\mathrm{A}}$, and $\neg g_{\mathrm{A}}$ satisfies $\left|\varphi\right|\geq\left|\psi\right|+7$. It remains to check the conditions (P1) and (P2) to show that $\psi(x_{3},\ldots,x_{n})$ is an encoding of $\operatorname{\mathrm{AMO}}_{n-2}$:

1. (P1)

As $\psi$ is a subset of $\varphi$, each satisfying assignment of $\varphi\wedge x_{i}$ for $i\in\{3,\ldots,n\}$ can be restricted to a satisfying assignment of $\psi\wedge x_{i}$. 2. (P2)

Let us check $\psi\wedge x_{i}\vdash_{1}\neg x_{j}$ for each $i,j\in\{3,\dots,n\}$, $i\not=j$. By Lemma 6.3, we can assume $i<j$. Let us consider separately the cases $i=3$ and $i\geq 4$. Case $i\geq 4$.

Fix a series of unit resolutions witnessing $\varphi\wedge x_{i}\vdash_{1}\neg x_{j}$ according to Lemma 6.4. This series does not use any clause containing the literals $\neg x_{1}$, $\neg x_{2}$. If this series does not derive a literal on the variable $\mathrm{var}(g_{\mathrm{A}})$, then $\psi\wedge x_{i}\vdash_{1}\neg x_{j}$ and we are done. Assume, the series of resolutions derives a literal $h\in\{g_{\mathrm{A}},\neg g_{\mathrm{A}}\}$. In order to prove $\psi\wedge x_{i}\vdash_{1}\neg x_{j}$, we split this series into the two parts at the occurrence of the literal $h$ and replace each of these parts by another series of resolutions in such a way that they can be combined via a literal on the variable $\mathrm{var}(g_{\mathrm{C}})$ and do not derive a literal on the variable $\mathrm{var}(g_{\mathrm{A}})$. Using this, we obtain a series witnessing $\psi\wedge x_{i}\vdash_{1}\neg x_{j}$.

By Lemma 6.3, we have $\varphi\wedge x_{i}\vdash_{1}h$ and $\varphi\wedge x_{j}\vdash_{1}\neg h$. Let us prove that for each $k\in\{4,\ldots,n\}$, we have

• •

$\varphi\wedge x_{k}\vdash_{1}g_{\mathrm{A}}$ implies $\psi\wedge x_{k}\vdash_{1}g_{\mathrm{C}}$

• •

$\varphi\wedge x_{k}\vdash_{1}\neg g_{\mathrm{A}}$ implies $\psi\wedge x_{k}\vdash_{1}\neg g_{\mathrm{C}}$

If $\varphi\wedge x_{k}\vdash_{1}g_{\mathrm{A}}$, the set ${\cal U}_{\varphi}(x_{k})$ contains $g_{\mathrm{C}}$ by the claim above. Consider a series of resolutions witnessing $\varphi\wedge x_{k}\vdash_{1}g_{\mathrm{C}}$. As $g_{\mathrm{A}}\in{\cal U}_{\varphi}(x_{k})$, this series does not derive $\neg g_{\mathrm{A}}$. By (24), this series does not derive $g_{\mathrm{A}}$. Together, we have $\psi\wedge x_{k}\vdash_{1}g_{\mathrm{C}}$.

If $\varphi\wedge x_{k}\vdash_{1}\neg g_{\mathrm{A}}$, the set ${\cal U}_{\varphi}(x_{k})$ contains $\neg g_{\mathrm{C}}$ by the claim above. Consider a series of resolutions witnessing $\varphi\wedge x_{k}\vdash_{1}\neg g_{\mathrm{C}}$. As $\neg g_{\mathrm{A}}\in{\cal U}_{\varphi}(x_{k})$, this series does not derive $g_{\mathrm{A}}$. By (23) and Lemma 6.3, this series does not derive $\neg g_{\mathrm{A}}$. Together, we have $\psi\wedge x_{k}\vdash_{1}\neg g_{\mathrm{C}}$.

If $h=g_{\mathrm{A}}$, then $\varphi\wedge x_{i}\vdash_{1}g_{\mathrm{A}}$ and $\varphi\wedge x_{j}\vdash_{1}\neg g_{\mathrm{A}}$. By the above implications, we have $\psi\wedge x_{i}\vdash_{1}g_{\mathrm{C}}$ and $\psi\wedge x_{j}\vdash_{1}\neg g_{\mathrm{C}}$. Using this and Lemma 6.3, we obtain $\psi\wedge x_{i}\vdash_{1}\neg x_{j}$. If $h=\neg g_{\mathrm{A}}$, we obtain $\psi\wedge x_{i}\vdash_{1}\neg x_{j}$ by a similar argument using a series of resolutions deriving $\neg g_{\mathrm{C}}$ as an intermediate step.

Case $i=3$.

We have either $\varphi\wedge x_{j}\vdash_{1}\neg g_{\mathrm{B}}$ or $\varphi\wedge x_{j}\vdash_{1}g_{\mathrm{C}}$. Assume $\varphi\wedge x_{j}\vdash_{1}\neg g_{\mathrm{B}}$ and consider a series of unit resolutions witnessing this. By the claim above, this series does not derive the literal $g_{\mathrm{A}}$. By (24) and Lemma 6.3, it does not derive $\neg g_{\mathrm{A}}$. Hence, $\psi\wedge x_{j}\vdash_{1}\neg g_{\mathrm{B}}$ and we have $\psi\wedge x_{3}\vdash_{1}\neg x_{j}$.

Assume $\varphi\wedge x_{j}\vdash_{1}g_{\mathrm{C}}$ and consider a series of unit resolutions witnessing this. By the claim above, this series does not derive the literal $\neg g_{\mathrm{A}}$. By (24), it does not derive $g_{\mathrm{A}}$. Hence, $\psi\wedge x_{j}\vdash_{1}g_{\mathrm{C}}$ and we have $\psi\wedge x_{3}\vdash_{1}\neg x_{j}$. ∎

It remains to estimate the size of an encoding of $\operatorname{\mathrm{AMO}}_{n}$ that satisfies both the additional conditions of the restricted regular form.

Proposition 6.9**.**

Let $n\geq 4$ and let $\varphi(\mathbf{x},\mathbf{y})$ be a minimum size 2-CNF encoding of $\operatorname{\mathrm{AMO}}_{n}$ with the minimum number of auxiliary variables and, moreover, assume that $\varphi$ is in regular form. If $\varphi$ satisfies the following two conditions

• •

The sets $L^{\mathrm{v}}_{\varphi,1},\ldots,L^{\mathrm{v}}_{\varphi,n}$ are pairwise distinct.

• •

For any three different indices $r,s,t\in\{1,\ldots,n\}$ we have $\left|L^{\mathrm{v}}_{\varphi,r}\cup L^{\mathrm{v}}_{\varphi,s}\cup L^{\mathrm{v}}_{\varphi,t}\right|>3$,

then $|\varphi|\geq 2n+2\sqrt{n}-3$.

Proof.

Consider the undirected graph $G=(\mathbf{y},E)$, whose vertices are auxiliary variables and different variables $u,v\in\mathbf{y}$ are connected by an edge $(u,v)\in E$ if and only if $(g\vee h)\in\varphi$ for some $g\in\mathrm{lit}(u)$ and $h\in\mathrm{lit}(v)$. Let $\mathcal{K}$ denote the set of the connected components of $G$. Note that the elements of $\mathcal{K}$ are sets of variables, which form a partition of $\mathbf{y}$. For $i\in\{1,\dots,n\}$, let

[TABLE]

Since $\varphi$ is in regular form, $|K_{\varphi,i}|\leq 2$. Fix $i\not=j$ and let $e_{0},e_{1},\dots,e_{p}\in\mathrm{lit}(\mathbf{x}\cup\mathbf{y})$ be a sequence of literals derived in a series of resolutions witnessing $\varphi\wedge x_{i}\vdash_{1}\neg x_{j}$ according to Lemma 6.4. Hence, $e_{1}\in L_{\varphi,i}$ and $\neg e_{p-1}\in L_{\varphi,j}$. Then, the variables $\mathrm{var}(e_{1}),\ldots,\mathrm{var}(e_{p-1})$ form a path in $G$ between a vertex in one of the components in $K_{\varphi,i}$ and a vertex in one of the components in $K_{\varphi,j}$. Since all the vertices of a path belong to the same connected component, we have $K_{\varphi,i}\cap K_{\varphi,j}\neq\emptyset$.

Let us prove that $|\mathcal{K}|\leq 3$ by contradiction. Assume $|\mathcal{K}|\geq 4$ and distinguish two cases:

There exists $K_{1}\in\mathcal{K}$, such that $K_{1}\in K_{\varphi,i}$ for all $i\in\{1,\dots,n\}$. Choose different components $K_{2},K_{3}\in\mathcal{K}$ different from $K_{1}$, choose variables $u\in K_{2},v\in K_{3}$, and consider the formula $\varphi^{\prime}=\varphi[u\leftarrow v]$. We show that $\varphi^{\prime}$ satisfies the conditions (P1) and (P2), thus it encodes $\operatorname{\mathrm{AMO}}_{n}$ in contradiction to the assumption that $\varphi$ has the minimum number of auxiliary variables.

1. (P1)

For every $i\in\{1,\dots,n\}$, we prove that there is a satisfying assignment $\alpha$ of $\varphi\wedge x_{i}$, such that $\alpha(u)=\alpha(v)$. This implies that $\varphi^{\prime}\wedge x_{i}$ is satisfiable as well.

Clearly, $K_{2}\not\in K_{\varphi,i}$ or $K_{3}\not\in K_{\varphi,i}$, because $|K_{\varphi,i}|\leq 2$ and $K_{1}\in K_{\varphi,i}$. Due to the symmetry between $K_{2}$ and $K_{3}$ and the variables $u$ and $v$, we can assume $K_{2}\not\in K_{\varphi,i}$. As $\varphi\wedge x_{i}$ is satisfiable, there is a literal $e\in\mathrm{lit}(v)$ such that $\varphi\wedge x_{i}\wedge e$ is satisfiable. Lemma 6.5 and the assumption that $\varphi$ is in regular form imply that the set ${\cal U}_{\varphi}(x_{i},e)$ contains only the literal $x_{i}$, literals $\neg x_{j}$ for $j\not=i$, and literals on some of the auxiliary variables in the components contained in $K_{\varphi,i}$ and in $K_{3}$. In particular, we have ${\cal U}_{\varphi}(x_{i},e)\cap\mathrm{lit}(K_{2})=\emptyset$. By Lemma 6.1, $\varphi$ is propagation complete. Hence, none of the literals $u$ and $\neg u$ is an implicate of $\varphi\wedge x_{i}\wedge e$. Consequently, there exists a satisfying assignment $\alpha$ of the formula $\varphi\wedge x_{i}\wedge e$ such that $\alpha(u)=\alpha(v)$ as required. 2. (P2)

Since $\varphi^{\prime}\wedge x_{i}$ is satisfiable for every $i\in\{1,\ldots,n\}$, Lemma 3.7 for the formula $\varphi\wedge x_{i}$ and the substitution $[u\leftarrow v]$ implies $\varphi^{\prime}\wedge x_{i}\vdash_{1}\neg x_{j}$ for all $j\not=i$. 2. 2.

Assume that for each $K\in\mathcal{K}$ there exists $i\in\{1,\dots,n\}$ such that $K\not\in K_{\varphi,i}$. It follows that $\left|K_{\varphi,i}\right|=2$ for each $i\in\{1,\dots,n\}$. Indeed, if $K_{\varphi,j}=\{K\}$ for some $j$ and $K\in\mathcal{K}$, then $K\in K_{\varphi,i}$ for all $i$, since $K_{\varphi,i}\cap K_{\varphi,j}\neq\emptyset$.

By the assumptions, there are $i,j$, such that $K_{\varphi,i}\not=K_{\varphi,j}$. Since $K_{\varphi,i}$ and $K_{\varphi,j}$ have a non-empty intersection, there are $K_{1},K_{2},K_{3}\in\mathcal{K}$, such that

[TABLE]

By the assumptions, there is $k$, such that $K_{1}\not\in K_{\varphi,k}$. Since $K_{\varphi,k}$ has a non-empty intersection with both $K_{\varphi,i}$ and $K_{\varphi,j}$, we have

[TABLE]

Since $|\mathcal{K}|\geq 4$, there is $K_{4}\in\mathcal{K}\setminus\{K_{1},K_{2},K_{3}\}$ and, moreover, there is $l$, such that $K_{\varphi,l}=\{K_{4},K_{5}\}$ for some $K_{5}\in\mathcal{K}$. Since $K_{\varphi,l}$ has a non-empty intersection with each of the sets $K_{\varphi,i}$, $K_{\varphi,j}$, $K_{\varphi,k}$, each of these sets contains $K_{5}$. This is a contradiction, since these sets have no common element.

Let $\psi\subset\varphi$ denote the set of clauses of $\varphi$ that contain only variables from $\mathbf{y}$. As $G$ has at most three connected components and the number of edges of $G$ is $|\psi|$, we have $\left|\psi\right|\geq\left|\mathbf{y}\right|-3$.

Consider an undirected graph $G^{\prime}$ with vertices $\mathbf{y}$, whose edges are the sets $L^{\mathrm{v}}_{\varphi,1},\dots,L^{\mathrm{v}}_{\varphi,n}$. By assumption, $G^{\prime}$ contains $n$ edges and does not contain a triangle. Since $G^{\prime}$ contains $|\mathbf{y}|$ vertices, Mantel’s theorem (a special case of Turán’s theorem) implies $n\leq\frac{1}{4}|\mathbf{y}|^{2}$. Thus, $\left|\mathbf{y}\right|\geq 2\sqrt{n}$ and $\left|\psi\right|\geq 2\sqrt{n}-3$. Finally, we obtain $|\varphi|=2n+|\psi|\geq 2n+2\sqrt{n}-3$ as required. ∎

The following theorem presents the second main result of this paper. Namely, it shows part 1 for $\mathcal{P}_{2}(n)$ and part 3 of Theorem 2.8.

Theorem 6.10**.**

For $n\geq 3$, the minimum size $\mathcal{P}_{2}(n)$ of a 2-CNF encoding of $\operatorname{\mathrm{AMO}}_{n}$ satisfies

If $n\leq 10$, then $\mathcal{P}_{2}(n)=3n-6$. 2. 2.

If $n\geq 9$, then $\mathcal{P}_{2}(n)\geq 2n+2\sqrt{n}-3$.

Proof.

If $3\leq n\leq 8$, the conclusion follows from Lemma 6.1, Theorem 5.5 and Lemma 3.1. For the rest of the proof, let $\varphi$ be a minimum size 2-CNF encoding of $\operatorname{\mathrm{AMO}}_{n}$ that, morever, has the minimum number of auxiliary variables among such encodings. In particular, we have $|\varphi|=\mathcal{P}_{2}(n)$. We first analyze the cases $n=9$ and $n=10$. The upper bound $\mathcal{P}_{2}(n)\leq 3n-6$ follows from Lemma 3.1. The lower bound $\mathcal{P}_{2}(n)\geq 3n-6$ for $n=9$ and $n=10$ can be proven as follows.

• •

Assume $n=9$. If $\varphi$ is not in regular form, we have by Theorem 2.10

[TABLE]

If $\varphi$ is in regular form and either assumptions of Proposition 6.7 or assumptions of Proposition 6.8 are satisfied, then we have

[TABLE]

It remains to consider $\varphi$ in regular form satisfying the assumptions of Proposition 6.9, for which we have

[TABLE]

Altogether, $\mathcal{P}_{2}(n)=|\varphi|\geq 21=3n-6$.

• •

Assume $n=10$. If $\varphi$ is not in regular form, we have by Theorem 2.10

[TABLE]

If $\varphi$ is in regular form and either assumptions of Proposition 6.7 or assumptions of Proposition 6.8 are satisfied, then we have

[TABLE]

It remains to consider $\varphi$ in regular form satisfying the assumptions of Proposition 6.9. Since $|\varphi|$ is an integer, we have

[TABLE]

Altogether, $\mathcal{P}_{2}(n)=|\varphi|\geq 24=3n-6$.

We prove $\mathcal{P}_{2}(n)\geq 2n+2\sqrt{n}-3$ for $n\geq 9$ by induction. Since $3n-6\geq 2n+2\sqrt{n}-3$ for $n=9$ and $n=10$, the lower bound $\mathcal{P}_{2}(n)\geq 2n+2\sqrt{n}-3$ is already proven for these values of $n$. Assume $n>10$ for the rest of the proof and consider three cases concerning the structure of $\varphi$.

If $\varphi$ is not in regular form, then Theorem 2.10 and the induction hypothesis imply

[TABLE]

because $1+2\sqrt{n-1}\geq 2\sqrt{n}$ holds whenever $n\geq 2$.

If $\varphi$ is in regular form and either assumptions of Proposition 6.7 or assumptions of Proposition 6.8 are satisfied, then using the induction hypothesis, we have

[TABLE]

because $2+2\sqrt{n-2}\geq 2\sqrt{n}$ holds whenever $n\geq 3$.

It remains to consider $\varphi$ in regular form satisfying the assumptions of Proposition 6.9. This lemma implies directly the required lower bound. ∎

7 Further Research

Since 2-CNF formulas are closed under resolution, a function can have a 2-CNF encoding only if it is expressible by a 2-CNF formula. The function $\operatorname{\mathrm{AMO}}_{n}$ can be represented by an anti-monotone 2-CNF formula. It is quite natural to ask if there is a minimum size PC encoding of $\operatorname{\mathrm{AMO}}_{n}$ that is a 2-CNF formula, or at least a CNF formula without positive occurrences of the input variables. More generally, we can pose the following questions. Note that by Lemma 6.5, a positive answer to Question 7.1 implies a negative answer to Question 7.2.

Question 7.1**.**

Assume, $f(\mathbf{x})$ is a boolean function expressible by a monotone or anti-monotone 2-CNF formula. Is there a PC encoding of the function $f$ of minimum size, which is, moreover, a 2-CNF formula?

Question 7.2**.**

Is there a PC encoding of $\operatorname{\mathrm{AMO}}_{n}$ of minimum size, which contains a positive occurence of an input variable?

We expect a negative answer to Question 7.2. However, for every sufficiently large $n$, there is an irredundant prime PC encoding of $\operatorname{\mathrm{AMO}}_{n}$ of size $\Theta(n^{2})$ that contains positive occurences of the input variables. Let us briefly present an example of such a formula. Let $A$, $B$, $C$, $D$ be non-empty sets that form a partition of $\{1,\ldots,n\}$ and consider auxiliary variables $y_{1},\ldots,y_{5}$. Let $E$ be the set of the edges of the complete graph on the vertices $\{1,\ldots,n\}$ except of the edges contained in the bipartite graph between $A$ and $B$ and the bipartite graph between $C$ and $D$. The formula

[TABLE]

is a prime PC encoding of $\operatorname{\mathrm{AMO}}_{n}$ containing a positive occurence of each input variable. Moreover, removing any of the clauses with a positive occurence of an input variable leads to a formula that is not a PC encoding of $\operatorname{\mathrm{AMO}}_{n}$. For example, if we remove the clause $\neg y_{1}\vee\bigvee_{i\in A}x_{i}$, then one can obtain a satisfying assignment inconsistent with the function $\operatorname{\mathrm{AMO}}_{n}$ as follows. Choose $i\in C$, $j\in D$, set $x_{i}=x_{j}=1$, $x_{k}=0$ for all $k\in\{1,\ldots,n\}\setminus\{i,j\}$, $y_{1}=1$, and $y_{2}=\cdots=y_{5}=0$.

It is plausible to assume that for every $n\geq 3$, there is a minimum size PC encoding of $\operatorname{\mathrm{EO}}_{n}$, which has the form

[TABLE]

where $\varphi(\mathbf{x},\mathbf{y})$ is a minimum size PC encoding of $\operatorname{\mathrm{AMO}}_{n}$. This suggests the following conjecture, which is a strengthening of Proposition 3.4.

Conjecture 7.3**.**

Let $\varphi$ be a propagation complete encoding of $\operatorname{\mathrm{AMO}}_{n}$ of minimum size and let $\psi$ be a propagation complete encoding of $\operatorname{\mathrm{EO}}_{n}$ of minimum size for $n\geq 2$. Then $|\psi|=|\varphi|+1$.

The requirement that an encoding is propagation complete can be relaxed to unit refutation completeness introduced in [13]. An encoding $\varphi(\mathbf{x},\mathbf{y})$ is unit refutation complete, if for every partial assignment of $\mathbf{x}$ that makes $\varphi$ unsatisfiable, a contradiction can be derived by unit propagation. This makes no difference for a 2-CNF formula. A minimum size 2-CNF encoding is propagation complete and, hence, unit refutation complete. It follows that for 2-CNF, the minimum size of a unit refutation complete encoding and the minimum size of a propagation complete encoding of the same function are the same. However, for general CNF formulas, a unit refutation complete encoding can be smaller than the smallest propagation complete encoding and, hence, a lower bound on the size of a unit refutation complete encodings is harder to prove.

Question 7.4**.**

Is the minimum size of a unit refutation complete encoding of $\operatorname{\mathrm{AMO}}_{n}$ or $\operatorname{\mathrm{EO}}_{n}$ at least $2n+\Omega(\sqrt{n})$?

8 Conclusion

We have shown that any propagation complete encoding of the $\operatorname{\mathrm{AMO}}_{n}$ or $\operatorname{\mathrm{EO}}_{n}$ constraint for $n\geq 9$ contains at least $2n+\sqrt{n}-2$ clauses. This shows that the best known upper bound of $2n+4\sqrt{n}+O(\sqrt[4]{n})$ clauses achieved by product encoding introduced by Chen [10] is essentially best possible. Let us point out that the product encoding is an encoding of $\operatorname{\mathrm{AMO}}_{n}$ in regular form which is the notion playing central role in our proof.

For the special case of 2-CNF encodings, we have shown for $n\geq 9$ a better lower bound $2n+2\sqrt{n}-3$. This case is important, because the encodings that appear in the literature are 2-CNF formulas including the product encoding mentioned above.

We have also shown that for $3\leq n\leq 8$, the number of clauses in a propagation complete encoding of $\operatorname{\mathrm{AMO}}_{n}$ is at least $3n-6$. This number of clauses is achieved by sequential encoding and therefore in this case the lower and upper bound match for both general CNF formulas and 2-CNF formulas.

Acknowledgments

Petr Kučera was supported by the Czech Science Foundation (grant GA15-15511S). Petr Savický was supported by CE-ITI and GAČR under the grant GBP202/12/G061 and by the institutional research plan RVO:67985807.