Exact Algorithms and Hardness Result for the Boolean Connectivity Problem of $k$-Horn Formulas

The Boolean connectivity problem asks whether the satisfying assignments of a given Boolean formula are connected over the $n$-dimensional hypercube. The structure and connectivity of the satisfying assignments are related to analyzing the satisfiability algorithm and the threshold of satisfiability. The satisfiability problem is characterized by the famous Schaefer dichotomy theorem [12]. Schaefer’s class denotes the class of formulas, e.g., $2$-CNF, (dual) Horn, and affine formulas. Ekin, Hammer, and Kogan [5] showed that the Boolean connectivity of DNF is solvable in time linear in the size of DNF, while determining the connectivity of falsifying assignments of DNF is $\mathrm{𝖼𝗈𝖭𝖯}$-hard, i.e., the Boolean connectivity of CNF is $\mathrm{𝖼𝗈𝖭𝖯}$-hard. Gopalan, Kolaitis, Maneva, and Papadimitriou [6] deeply investigated the computational complexity of the Boolean connectivity problem. They showed that it is either $\mathrm{𝖼𝗈𝖭𝖯}$-complete or $\mathrm{𝖯𝖲𝖯𝖠𝖢𝖤}$-complete for non-Schaefer’s class, and in $\mathrm{𝖼𝗈𝖭𝖯}$ for Schaefer’s class. They also conjectured that it is solvable in polynomial time for Schaefer’s class. Makino, Tamaki, and Yamamoto [7] and Schwerdtfeger [15] gave a negative answer by proving the $\mathrm{𝖼𝗈𝖭𝖯}$-completeness of the Boolean connectivity problem for $k$-Horn and other related formulas.

Although the trichotomy theorem of the Boolean connectivity problem has been fully established, only a few algorithms are known for instances beyond $𝖯$. For the connectivity of $k$-CNF formulas (Conn $k$-CNF), it is solvable in polynomial time when $k=2$ [6]. Makino et al. [8] presented a moderately exponential-time algorithm for Conn $k$-CNF ($k\ge 3$) over $n$ variables and $m$ clauses which is $\mathrm{𝖯𝖲𝖯𝖠𝖢𝖤}$-complete. Their algorithm constructs the solution graph over partial satisfying assignments and then determines the connectivity of the graph. It runs in $O^{\ast }(2^{(1-c_k)n})$ time and exponential space, where $c_k=\log {\beta }_k/(1+\log {\beta }_k)$ and is the largest positive real number that satisfies $x^k-x^{k-1}-\mathrm{\cdots }-x-1=0$. The $O^{\ast }$ notation suppresses polynomial factors in $n$ and $m$. Throughout this paper, the base of the logarithm is 2. Note that $c_k=1/2^{O(k)}$.

In this paper, we deeply investigate the complexity of the Boolean connectivity of $k$-Horn formulas (Conn $k$-Horn). We first consider an exact algorithm for Conn $k$-Horn without any structural restrictions. The algorithm of Makino et al. can also solve Conn $k$-Horn in the same running time since $k$-Horn formulas are subsets of $k$-CNF formulas. Hence, it is a natural question whether there exists a faster algorithm for Conn $k$-Horn. Makino et al. [7] presented an exact algorithm in polynomial time in terms of the number of variables and the size of the characteristic set of a given Horn formula. Unfortunately, the efficiency of finding the characteristic set of a given Horn formula is not yet well-known. We give an affirmative answer by utilizing the deterministic PPZ algorithm for $k$-SAT shown by Paturi, Pudlák, and Zane [10]. The deterministic PPZ algorithm can find not only a satisfiability assignment but also all locally minimal satisfying assignments. Moreover, Conn $k$-Horn can be solved to find a locally minimal satisfying assignment with Hamming weight at least one [6]. These help us solve Conn $k$-Horn exponentially faster than the algorithm of Conn $k$-CNF.

The slightly modified algorithm above can count the number of connected components in the solution graph of a given $k$-Horn formula.

We next consider Conn $3$-Horn with a bounded number of occurrences of each variable. We present both algorithmic and hardness results.

The key idea of our algorithm is based on the relationship between the solution graph of a Horn formula and a non-empty maximal self-implicating set, as shown in [15]. Any variable in a self-implicating set is forced to be true when all the other variables in the set are true. The solution graph is disconnected if and only if there exists a non-empty maximal self-implicating set and no clauses with only negative literals of these variables. We show that such a set can be found in polynomial time.

We first prove the complement of Conn $3$-Horn remains $\mathrm{𝖭𝖯}$-complete even if each variable appears at most four times by a polynomial-time reduction from Monotone Not-All-Equal 3-SAT with each variable appearing exactly four times. This problem is known to be $\mathrm{𝖭𝖯}$-complete [3]. We next show Theorem 4 by providing a polynomial-time reduction from the above problem.

Let $x$ be a Boolean variable that takes true (1) or false (0). A literal is a Boolean variable $x$ (positive literal) or its negation $\overline{x}$ (negative literal). A clause is a disjunction of literals. The length of clause $C$ is defined as the number of literals in $C$. A unit clause is a clause of length one. A conjunctive normal form (CNF) formula is a conjunction of clauses, and a $k$-CNF formula is a CNF formula if the length of each clause is at most $k$. A CNF formula is monotone if all clauses in the formula consist of only positive (or negative) literals. In this paper, we use Monotone CNF as CNF formulas with all positive literals unless otherwise stated. A Horn clause is a clause including at most one positive literal. A Horn formula is a CNF formula whose all clauses are Horn, and a $k$-Horn formula is a $k$-CNF formula and a Horn formula. Let $X=\{x_1,x_2,\mathrm{\dots },x_n\}$ be a set of Boolean variables. An assignment of a Boolean formula $\phi$ over $X$ is $\alpha =({\alpha }_1,{\alpha }_2,\mathrm{\dots },{\alpha }_n)\in {\{0,1\}}^n$ such that $x_i={\alpha }_i$ for all $i$. A partial assignment of a Boolean formula $\phi$ over $X$ is $\alpha =({\alpha }_1,{\alpha }_2,\mathrm{\dots },{\alpha }_n)\in {\{0,1,\ast \}}^n$ such that $x_i={\alpha }_i$ for all $i$. A partial assignment with ${\alpha }_i=\ast$ means variable $x_i$ is not assigned a 0/1 value. For a variable $x$ and an assignment $\alpha$, we denote by $\alpha (x)$ the value of $x$ under an assignment $\alpha$. We can simplify a Boolean formula $\phi$ by a partial assignment $\alpha$ in a natural way, and the resulting formula is denoted by ${\phi |}_{\alpha }$. An (partial) assignment $\alpha$ is a (partial) satisfying assignment of a Boolean formula $\phi$ if ${\phi |}_{\alpha }$ is true. The satisfiability problem is to determine whether there exists a satisfying assignment of a given Boolean formula $\phi$.

Many excellent exponential-time algorithms for the satisfiability problem of $k$-CNF formulas ($k$-CNF SAT) are known. One of the famous algorithms is shown by Paturi, Pudlák, and Zane [10].

For an assignment $\alpha \in {\{0,1\}}^n$, the Hamming weight of $\alpha$ is $|\{i:{\alpha }_i=1(1\le i\le n)\}|$. For two assignments $\alpha ,{\alpha }^{\prime }\in {\{0,1\}}^n$, the Hamming distance between $\alpha$ and ${\alpha }^{\prime }$, denoted by $d(\alpha ,{\alpha }^{\prime })$, is $|\{i:{\alpha }_i\ne {\alpha }_i^{\prime }(1\le i\le n)\}|$. We define the solution graph of a Boolean formula $\phi$ as $G_{\phi }≔(V_{\phi },E_{\phi })$, where $V_{\phi }$ is a set of all satisfying assignments of $\phi$, that is, $V_{\phi }=\{\alpha :{\phi |}_{\alpha }=1,\alpha \in {\{0,1\}}^n\}$, and $E_{\phi }=\{(\alpha ,{\alpha }^{\prime }):d(\alpha ,{\alpha }^{\prime })=1\text{ and }\alpha ,{\alpha }^{\prime }\in V_{\phi }\}$.

Makino, Tamaki, and Yamamoto [7] showed that Conn $3$-Horn is $\mathrm{𝖼𝗈𝖭𝖯}$-complete, thus the following lemma holds.

Given two assignments $\alpha ,{\alpha }^{\prime }\in {\{0,1\}}^n$, we denote $\alpha \le {\alpha }^{\prime }$ as the coordinate-wise partial order if ${\alpha }_i\le {\alpha }_i^{\prime }$ for each $1\le i\le n$. A satisfying assignment $\alpha$ for a given formula $\phi$ is locally minimal if $\alpha$ has no neighboring satisfying assignment ${\alpha }^{\prime }$ with $d(\alpha ,{\alpha }^{\prime })=1$ and ${\alpha }^{\prime }\le \alpha$. For $v,v^{\prime }\in V_{\phi }$, a monotone path from $v$ to $v^{\prime }$ is a path in $G_{\phi }$, $v\to u_1\to \mathrm{\cdots }\to u_r\to v^{\prime }$ such that $v\le u_1\le \mathrm{\cdots }\le u_r\le v^{\prime }$. Gopalan, Kolaitis, Maneva, and Papadimitriou [6] showed a notable connection between locally minimal satisfying assignments and the connectivity of Horn formulas.

The following corollary follows from that any Horn formula without unit clauses over $n$ variables has an all-zero satisfying assignment ($0^n$) and Lemma 8.

Let $P(C)$ (resp. $N(C)$) denote the set of variables that appear in positive (resp. negative) literals in a clause $C$ of $\phi$. Makino et al. [7] introduced the following Boolean formula ${\mathrm{\Phi }}_{\phi }$.

For example, given a Horn formula

then

Note that each $D_i$ is either a unit clause with a negative literal or a conjunction of one negative literal and disjunctions of positive literals. The satisfiability of ${\mathrm{\Phi }}_{\phi }$ is strongly related to the connectivity of the solution graph of a Horn formula $\phi$ because a satisfying assignment of ${\mathrm{\Phi }}_{\phi }$ is a locally minimal satisfying assignment of $\phi$.

A restraint clause is a clause with only negative literals, and a restraint set is a set of variables included in restraint clauses. An implication clause is a clause that has one positive literal and one or more negative literals. A Boolean variable $x$ is said to be implied by a set of variables $U$ if setting all variables in $U$ to true forces $x$ to be true. A self-implicating set $U$ is a set of variables, where every $x\in U$ is implied by $U\setminus \{x\}$. We also say that $U$ is a maximal self-implicating set if $U$ is a set of all variables implied by $U$. For maximal self-implicating sets, there exists a relation between locally minimal satisfying assignments and maximal self-implicating sets.

The following corollary follows from Lemma 11 and Corollary 9.

In this section, we present a faster algorithm for Conn $k$-Horn based on the deterministic PPZ algorithm [10]. Before presenting our new algorithm, we describe the notations and behaviors of the deterministic PPZ algorithm, referred to as DetPPZ. Let $\phi$ be a $k$-CNF formula with $n$ variables and $m$ clauses, and let $\alpha$ be a satisfying assignment. A clause $C_{(\alpha ,i)}$ is a critical clause for the variable $x_i$ at the solution $\alpha$ if $C_{(\alpha ,i)}$ is to be false by flipping ${\alpha }_i$. A variable $x_i$ is a critical variable if there exists a critical clause $C_{(\alpha ,i)}$. The DetPPZ first checks whether there exists a satisfying assignment of $\phi$ to check all assignments with Hamming weight at most $ϵn$ where . If there is no such satisfying assignment, the DetPPZ tries to find a locally minimal satisfying assignment $\alpha$ with Hamming weight at least $ϵn$. Note that $\phi$ is falsified by any assignment obtained by flipping any 1 in $\alpha$ to 0. Thus, $\alpha$ must have at least $ϵn$ critical variables. Let $\sigma =({\sigma }_1,\mathrm{\dots },{\sigma }_n)$ be a permutation of $\{1,\mathrm{\dots },n\}$. The DetPPZ picks up a permutation $\sigma$ in a “good” small sample space and branches by assigning a 0/1 value to $x_{{\sigma }_i}$ according to the order in $\sigma$. If any critical variable appears last among the variables in the corresponding critical clause, then it can be assigned correctly. It helps to reduce the number of branches in the algorithm. Modifying the DetPPZ such that it does not halt even if it finds a satisfying assignment with Hamming weight at most $ϵn$, the DetPPZ can find all locally minimal satisfying assignments. From Corollary 9, Conn $k$-Horn can be solved by checking whether there exists some locally minimal satisfying assignment except for $0^n$ assignment. Thus, by combining the (modified) DetPPZ and the procedure checking locally minimality, we solve Conn $k$-Horn in the same running time as the DetPPZ. We describe our algorithm, PPZ-Conn-$k$Horn, in Algorithm 1.

The following “good” sample space of permutations using $k$-wise independent variables is useful.

The following lemma immediately follows from the proof of correctness of the deterministic PPZ algorithm shown in [10]. We provide almost the same proof for self-containedness in this paper.

In this section, we consider the Boolean connectivity of $3$-Horn, whose variable occurrence is bounded. Section 4.1 presents a deterministic polynomial-time algorithm for Conn 3-Horn with each clause of length exactly three and each variable appearing at most three times (Conn E3-Horn-3). Section 4.2 shows the $\mathrm{𝖼𝗈𝖭𝖯}$-complete of Conn 3-Horn where each variable appears exactly four times (Conn 3-Horn-E4).

We proved that Conn $3$-Horn remains $\mathrm{𝖼𝗈𝖭𝖯}$-complete even when the length of each clause is at most three and each variable appears exactly four times. Furthermore, we provided a polynomial-time algorithm for Conn $3$-Horn with each variable appearing at most three times and the length of each clause exactly three. These results seem to give a borderline between $𝖯$ and $\mathrm{𝖼𝗈𝖭𝖯}$-complete. However, it remains the complexity of two cases of Conn 3-Horn:(a) the length of each clause is exactly three and each variable appears exactly or at most four times; (b) the length of each clause is at most three and each variable appears exactly or at most three times. The complexity of Monotone NAE 3-SAT might be closely related to that of Conn 3-Horn for the following reasons. Monotone NAE $3$-SAT is polynomial-time solvable when the length of each clause is exactly three and each variable appears at most three times in [11]. Monotone NAE 3-SAT remains $\mathrm{𝖭𝖯}$-complete even when the length of each clause is at most three and each variable appears exactly four times. These complexities are equivalent to those of DisConn 3-Horn with the same restrictions. Furthermore, Monotone NAE 3-SAT is $\mathrm{𝖭𝖯}$-complete even when the length of each clause is at most three and each variable appears exactly three times [4]. It also remains $\mathrm{𝖭𝖯}$-complete even when the length of each clause is exactly three and each variable appears exactly four times [3]. Thus, we conjecture that cases (a) and (b) are $\mathrm{𝖼𝗈𝖭𝖯}$-complete.