Satisfiability Algorithm for Syntactic Read-k-times Branching Programs

Abstract

The satisfiability of a given branching program is to determine whether there exists a consistent path from the root to 1-sink. In a syntactic read-k-times branching program, each variable appears at most k times in any path from the root to a sink. In a preliminary version of this paper, we provide a satisfiability algorithm for syntactic read-k-times branching programs with n variables and m edges that runs in time $O\left (\text {poly}(n, m^{k^{2}})\cdot 2^{(1-4^{-k-1})n}\right )$. In this paper, we improve the bounds for k = 2. More precisely, we show that the satisfiability of syntactic read-twice branching programs can be solved in time $O\left (\text {poly}(n, m)\cdot 2^{5n/6}\right )$. Our algorithm is based on the decomposition technique shown by Borodin, Razborov and Smolensky [Computational Complexity, 1993].

1 Introduction

Branching programs (BPs) are well studied computation models in theory and practice. A BP is a directed acyclic graph with a unique root node and two sink nodes. Each nonsink node is labeled using a variable, and the edges correspond to a variable’s value of zero or one. Sink nodes are labeled either 0 or 1 depending on the output value. A BP computes a Boolean function naturally: it follows the edge corresponding to the input value from the root node to a sink node.

There exist two main restricted models, width-k and read-k-times BPs. A width-k BP is a leveled BP and each level has at most k nodes. Barrington [2] showed that any function in NC¹ can be computed by width-5 BPs of polynomial length. Thus, it is a challenge to prove super-polynomial lower bounds for width-5 BPs. Despite of many efforts, such bounds are known for only width-2 BPs by Yao [20].

Read-k-times BPs have two models, semantic and syntactic. A read-k-times BP is syntactic if each variable appears at most k times in any path. It is semantic if each variable appears at most k times in any computational path. Beame, Saks, and Thathachar [3] showed that polynomial-size semantic read-twice BP can compute functions requiring exponential size on any syntactic read-k-times BP. Thus, the semantic model is substantially stronger than the syntactic model. For the semantic case, Jukna [12] proved an exponential lower bound for syntactic read-k-times BPs over large domain D, where |D| = 2^3k+ 10. In case of read-once BPs, Cook, Edmonds, Medabalimi, and Pitassi [7] proved exponential lower bounds for |D| = 3.

The syntactic model is well studied. Borodin, Razborov, and Smolensky [5] exhibited an explicit function of the lower bound of $\exp \left ({\Omega }\left (\frac {n}{k^{3} 4^{k}}\right )\right )$. Jukna [11] provided an explicit function f such that nondeterministic read-once BPs of polynomial size can compute ¬f (i.e., the negation of f ); however, to compute f, nondeterministic read-k-times BPs require a size of $\exp \left ({\Omega }\left (\frac {\sqrt n}{k^{2k}}\right )\right )$. Thathachar [18] showed that for any k, the computational power of read-(k + 1)-times BPs is strictly stronger than that of read-k-times BPs. Sauerhoff [16] proved the exponential lower bound for randomized read-k-times BPs with a two-sided error.

The satisfiability of BPs (BP SAT), given a BP, is to determine whether there exists a consistent path from the root to 1-sink. Recently, BP SAT has become a significant problem because of the connection between satisfiability algorithms and lower bounds. Let $\mathcal {C}$ be a class of a circuit. Given a circuit in $\mathcal {C}$, $\mathcal {C}$-SAT is the determination of whether there exists an assignment to the input variables such that the circuit outputs 1. Williams [19] showed that to obtain $\mathbf {NEXP} \not \subseteq \mathcal {C}$, it suffices to develop an $O\left (2^{n-\omega (\log n)}\right )$ time algorithm for $\mathcal {C}$-SAT. By combining Barrignton’s theorem [2], if we would like to prove $\mathbf {NEXP} \not \subseteq \mathbf {NC^{1}}$, it is sufficient to develop an $O\left (2^{n-\omega (\log n)}\right )$ time algorithm for width-5 BP SAT. In addition, the hardness of BP SAT implies the hardness of the Edit Distance and Longest Common Sequence problem [1]. Thus, the design of a fast algorithm for BP SAT is one of the important tasks in the field of computational complexity.

We have another motivation for designing satisfiability algorithms. A technique for proving a lower bound against a class of circuit $\mathcal {C}$ is deeply connected to the design of an algorithm for $\mathcal {C}$-SAT. For example, Paturi, Pudlák, and Zane [14] proposed the satisfiability coding lemma, and applied it to design a satisfiability algorithm for CNF-SAT and to prove a lower bound for the parity function on depth-3 circuits. For AC⁰, Håstad’s switching lemma [8] helps us to prove an exponential lower bounds on the parity function. Impagliazzo, Matthews, and Paturi [10], by extending it, presented a satisfiability algorithm for AC⁰ and improved the correlation lower bound of AC⁰ with parity. Santhanam [15] presented a moderately exponential time algorithm for De Morgan formula SAT based on lower bound techniques by Subbotovskaya [17] and Håstad [9]. According to these results, we believe that any proof technique for a lower bound is translated into designing a satisfiability algorithm.

In this paper, we consider the satisfiability of syntactic read-k-times BPs. There exists no satisfiability algorithm for k ≥ 2 faster than a brute-force search, while the technique of lower bound by Borodin, Razborov, and Smolensky [5] is known. We present a moderately exponential time satisfiability algorithm based on the lower bound technique for read-k-times BPs where k ≥ 2. As a result, we get the following theorem.

Theorem 1

There exists a deterministic and polynomial space algorithm for a nondeterministic and syntactic read-k-times BP SAT with n variables and m edges that runs in time $O\left (\text {poly}(n, m^{k^{2}}) \cdot 2^{(1-4^{-k-1})n}\right )$.

When k = 2, we improve the running time of our algorithm.

Theorem 2

There exists a deterministic and polynomial space algorithm for a nondeterministic and syntactic read-twice BP SAT with n variables and m edges that runs in time $O\left (\text {poly}(n, m) \cdot 2^{5n/6}\right )$.

1.1 Our Techniques

Our satisfiability algorithm consists of two steps as follows: [Step 1: Decomposition] Given a syntactic read-k-times BP B of m edges, we obtain the representation of a function computed by B as a disjunction of at most $m^{2k^{2}}$ decomposed functions by using the decomposition algorithm proposed by Borodin, Razborov, and Smolensky [5]. It is sufficient to check the satisfiability of each decomposed function in the running time of Theorem 1, because if one of these functions is satisfiable then the input B is also satisfiable. Moreover, the property of the decomposition algorithm states that each decomposed function is a conjunction of at most 2k² functions on small variable sets. Let us represent a conjunction of functions as a set of functions ${\mathcal F}=\{f_{1}, f_{2}, \ldots , f_{\ell }\}$, where ℓ ≤ 2k². [Step 2: Satisfiability Checking] To check the satisfiability of ${\mathcal F}$, we find if there is an assignment that all functions f_i are satisfied at the same time. Let $({\mathcal F}_{1}, {\mathcal F}_{2})$ be a partition of ${\mathcal F}$. In addition, let X₁ and X₂ be sets of input variables appearing in only ${\mathcal F}_{1}$ and ${\mathcal F}_{2}$ respectively and X₃ be a set of input variables appearing in both F₁ and F₂. If X₃ is an empty set, we can check the satisfiability of ${\mathcal F}_{1}$ and ${\mathcal F}_{2}$ independently in time $O(2^{|X_{1}|} + 2^{|X_{2}|})$ by exhaustive search on each set X₁ and X₂. If both ${\mathcal F}_{1}$ and ${\mathcal F}_{2}$ are satisfiable, we know that ${\mathcal F}$ is also satisfiable. Our algorithm assigns 0/1 value to the variables in X₃ and then performs the exhaustive search on each set X₁ and X₂. Assuming that |X₁| + |X₂| + |X₃| = n, we obtain the satisfiability of ${\mathcal F}$ in time $O(2^{|X_{3}|}(2^{|X_{1}|} + 2^{|X_{2}|})) = O(2^{n-\min \limits \{|X_{1}|,|X_{2}|\}})$. Further, using probabilistic method, we show that the existence of a partition $({\mathcal F}_{1}, {\mathcal F}_{2})$ of ${\mathcal F}$ such that the value $\min \limits \{|X_{1}|,|X_{2}|\}$ is adequately large to imply the running time in Theorem 1. Thus, we can save the running time of our satisfiability algorithm.

1.2 Related Work

For the SAT of some restricted BPs, polynomial or moderately exponential time algorithms are known. An ordered binary decision diagram (OBDD) is a BP that has the same order of variables in all paths from the root to any sink. By checking the reachability from the root to 1-sink, the OBDD SAT can be solved in polynomial time. A k-OBDD is a natural extension of an OBDD with k layers; all layers are OBDDs with the same order of variables. Bollig, Sauerhoff, Sieling, and Wegener [4] provided a polynomial time algorithm that solves the k-OBDD SAT for any constant k. A k-indexed binary decision diagram (k-IBDD) is the same as a k-OBDD, except that an OBDD in each layer may have a different order of variables. A k-IBDD SAT is known to be NP-complete when k ≥ 2 [4]. Nagao, Seto, and Teruyama [13] proposed a satisfiability algorithm for any instances of k-IBDD SAT with cn edges, and its running time is $O\left (2^{(1-\mu _{k}(c))n}\right )$, where $\mu _{k}(c)={\Omega }\left (\frac {1}{(\log {c})^{2^{k-1}-1}}\right )$. Chen, Kabanets, Kolokolova, Shaltiel, and Zuckerman [6] showed that general BP SAT with o(n²) nodes can be determined in time $O\left (2^{n-\omega (\log {n})}\right )$.

1.3 Paper Organization

The remainder of this paper is organized as follows. In Section 2, we provide the notation and definitions. In Section 3, we provide two algorithms. One is a decomposition algorithm based on the technique in [5]. The other is a satisfiability algorithm for a specific class of Boolean functions. In Section 4, we propose our satisfiability algorithm for syntactic read-k-times BPs and improve this algorithm for k = 2 by modifying the satisfiability algorithm of Section 3.

2 Preliminaries

For a positive integer n, we denote by [n] a set of integers {1,2,…,n}. For a set S, |S| denotes the cardinality of S. Let X = {x₁,…,x_n} be a set of Boolean variables, and for x ∈ X, $\overline {x}$ denotes the negation of x. A branching program (BP), denoted by B = (V,E), is a rooted directed acyclic multigraph. A BP has a unique root node r and two sink nodes (0-sink and 1-sink). 0-sink and 1-sink are labeled by 0 and 1, respectively. Each node except for the sink nodes is labeled from X. Each edge e ∈ E has a label 0 (0-edge) or 1 (1-edge). We call node v an x_i-node when v’s label is x_i. A BP B is deterministic if any node except the two sink nodes in V has exactly two outgoing edges, a 0-edge and a 1-edge. Otherwise, B is nondeterministic. For an edge e = (u,v) ∈ E, u is a parent of v and the head of e. The in-degree of v is defined as the number of parents of v.

For a BP B on X, each input $\alpha = (\alpha _{1}, \ldots , \alpha _{n}) \in \{0,1\}^{n}$ activates all α_i-edges leaving the x_i-nodes in B, where 1 ≤ i ≤ n. A computation path is a path from r to a 0-sink or from r to a 1-sink using only activated edges. A BP B outputs 0 if there is no computation path from the root r to a 1-sink; otherwise, B outputs 1. Let $f : \{0,1\}^{n} \rightarrow \{0,1\}$ be a Boolean function. A BP B represents f if f(α) is equal to the output of B for any assignment α ∈{0,1}ⁿ. Two BPs B₁ and B₂ are equivalent if B₁ and B₂ represent the same function. The size of B, denoted by |B|, is defined as the number of edges in B. A BP is syntactic read-k-times if each variable appears at most k times in each path. Figure 1 is an example of syntactic read-twice BPs (k = 2). A BP is semantic read-k-times if each variable appears at most k times in each computation path. In this paper, we use only the syntactic model and for simplicity we call it read-k-times BP.

Fig. 1

Syntactic read-twice branching program

For a BP B and two nodes v,w, a subbranching program 〈B,v,w〉 is a subgraph of B that contains v, w, and every nodes and edges contained in all v-w paths in B. Given a BP B and nodes v,w ∈ V, we can construct 〈B,v,w〉 in O(|B|) time as follows:

• 1. Find the subset $V^{\prime }$ of V such that $V^{\prime }$ contains every node that is reachable from v and to w by the breadth-first search.

• 2. Obtain the subgraph of B induced by $V^{\prime }$.

A partial assignment to $x =(x_{1},\dots ,x_{n})$ is $\alpha = (\alpha _{1}, \ldots , \alpha _{n}) \in \{0,1,*\}^{n}$ such that x_i is unset when α_i = ∗; otherwise x_i is assigned to α_i. For any partial assignment α ∈{0,1,∗}ⁿ, a support of α is defined as S(α) := {x_i∣α_i≠∗}. For partial assignments α and $\alpha ^{\prime }$, $\alpha \circ \alpha ^{\prime }$ denotes the composition of α and $\alpha ^{\prime }$ defined as follows: $\alpha \circ \alpha ^{\prime }(i) = \alpha ^{\prime }(i)$ if $x_{i} \in S(\alpha ^{\prime })$, and $\alpha \circ \alpha ^{\prime }(i) = \alpha (i)$ otherwise. For instance, when α = (1,∗,1) and $\alpha ^{\prime } = (*, *, 0)$, we have $\alpha \circ \alpha ^{\prime } = (1, *, 0)$.

3 Key Lemmas

In this section, we provide two key lemmas for our algorithm. First, we introduce the decomposition algorithm developed by Borodin, Razborov, and Smolensky [5]. Their algorithm decomposes a (nondeterministic) read-k-times BP into a set of BPs with a small number of variables. Next, we provide a satisfiability algorithm for a specific class of Boolean functions that have three properties with parameters a and k. (1) Each function is composed of a disjunction of ka subfunctions. (2) Each variable belongs to at most k subfunctions. (3) Each subfunction has at most ⌈n/a⌉ variables. Our algorithm that checks the satisfiability of such a function is exponentially faster than a brute-force search.

Now, we analyze the running time of a decomposition algorithm by Borodin, Razborov, and Smolensky [5]. We will use this algorithm as a module to solve the syntactic read-k-times BP SAT in Section 4.1.

Lemma 1 (Theorem 1 in 5)

Let B be a (nondeterministic) syntactic read-k-times BP with n variables and size m and represent a Boolean function $f : \{0,1\}^{n} \rightarrow \{0,1\}$, and let a be a positive integer. There is an algorithm that constructs kam^ka BPs {B_i,j} from B, where i ∈ [m^ka] and j ∈ [ka], such that the following properties hold:

• 1. Let f_i,j be the Boolean function represented by B_i,j. Then,

  $$ \begin{array}{@{}rcl@{}} f = \bigvee_{i \in [m^{ka}]} \bigwedge_{j \in [ka]} f_{i,j}. \end{array} $$

• 2. Let X_i,j be the set of variables that appear in B_i,j. For each i and j, |X_i,j| is at most ⌈n/a⌉. For each i, each variable x belongs to at most k sets of {X_i,j}_{j= 1,…,ka}.

We revisit the algorithm given in the proof of Theorem 1 in [5]. Let B be a nondeterministic and syntactic read-k-times BP with n variables and size m. For each pair of nodes (v,w) ∈ V², X(v,w) denotes the set of all variables that appear in the labels on all possible paths from v to w except for the label of w. We find X(v,w) by dynamic programming for each pair of nodes v,w ∈ V.

We call a sequence e₁ := (w₁,v₂),e₂ := (w₂,v₃),…,e_ℓ := (w_ℓ,v_ℓ+ 1) of edges a trace if and only if the following properties hold:

• (a) For each j with 1 ≤ j ≤ ℓ + 1, we have |X(v_j,w_j)| < n/a.

• (b) For each j with 1 ≤ j ≤ ℓ, we have |X(v_j,v_j+ 1)|≥ n/a,

where we set v₁ as the root and w_ℓ+ 1 as the 1-sink. For each trace, any variable x belongs to at most k sets X(v_j,w_j), because B is a syntactic read-k-times BP. Note that any path from r to the 1-sink contains a unique trace. By property (b), for each trace, we have

$$ \begin{array}{@{}rcl@{}} \sum\limits_{j=1}^{\ell}|X(v_{j}, v_{j+1})| + |X(v_{\ell+1}, w_{\ell+1})| \geq \frac{n \ell}{a} + |X(v_{\ell+1}, w_{\ell+1})|, \end{array} $$

(1)

where w_ℓ+ 1 is the 1-sink. Since each variable belongs to at most k sets, the left-hand side can be bounded above by kn. This leads that the length ℓ of traces is at most ka.

Let ${\mathcal T}$ be the set of all traces. We construct ${\mathcal T}$ as follows. Enumerate all sequences of edges in E with the length of at most ka. For each sequence, check whether it satisfies the conditions (a) and (b) by using X(v,w). If it satisfies the conditions, then put it in ${\mathcal T}$. Note that the number of sequences needed to check is at most ${\sum }_{\ell =1}^{ka}\binom {m}{\ell } \leq m^{ka}$. Thus, we have $|{\mathcal T}| \leq m^{ka}$.

For each trace $T = (e_{1}=(w_{1}, v_{2}), \ldots , e_{\ell }=(w_{\ell }, v_{\ell +1})) \in {\mathcal T}$ and 1 ≤ j ≤ ℓ, let B_T,j be a BP constructed as follows:

• 1. Prepare the subbranching program 〈B,v_j,w_j〉, 0-sink, and 1-sink.

• 2. Create an edge from w_j to the 1-sink with the same label of (w_j,v_j+ 1).

• 3. If some node v does not have a 0-edge (resp. 1-edge) as an outgoing edge, create a 0-edge (resp. 1-edge) from v to the 0-sink.

Intuitively, B_T,j contains all paths from v_j to v_j+ 1 through w_j. Note that the index i of the statement corresponds to each trace T. Let g_T,j be the function represented by B_T,j. Thus, we have $f = \bigvee _{T \in {\mathcal T}} \bigwedge _{j=1}^{\ell +1}g_{T,j}$. Each function g_T,j depends on at most ⌈n/a⌉ variables by property (a). Because B is a syntactic read-k-times BP, for each trace T and each variable x, at most k functions g_T,j depend on x. Recalling that the left-hand side of inequality (1) is bounded above by kn and we have ℓ ≤ ka, ℓ = ka holds only if |X(v_ℓ+ 1,w_ℓ+ 1)| = 0, in which case g_T,ℓ+ 1 is a constant function. If this constant is 0, then $\bigwedge _{j=1}^{\ell +1}g_{T,j}$ is equal to 0 and we can drop whole terms. If it is 1, we can drop g_T,ℓ+ 1. Therefore, each conjunction part consists of at most ka terms.

Lemma 2

Given a (nondeterministic) syntactic read-k-times BP B with n variables and size m, the running time of the decomposition algorithm described above is O(kam^ka+ 1).

Proof

Let us analyze the running time of the above construction. First, for each pair of nodes v,w ∈ V, we find X(v,w) by dynamic programming in O(m) time. Therefore, the running time for enumerating all X(v,w) is O(m³). The running time for construction of ${\mathcal T}$ is O(kam^ka), because we have m^ka sequences and check the conditions for each sequence in O(ka) time. For each trace $T \in {\mathcal T}$, we construct at most ka branching programs B_t,j in O(kam) time. Since we have $|{\mathcal T}| \leq m^{ka}$, we construct at most kam^ka branching programs in O(kam^ka+ 1) time. Totally, the total running time is at most O(m³) + O(kam^ka) + O(kam^ka+ 1) = O(kam^ka+ 1). □

Next, we give the satisfiability algorithm for a specific class Boolean functions. Let a and k be positive integers with a ≤ n. We are given a set of ka functions {f_i} (i ∈ [ka]) with the following properties:

• 1. Each f_i depends on only at most ⌈n/a⌉ variables X_i ⊂ X, i.e., |X_i|≤⌈n/a⌉.

• 2. Each variable x belongs to at most k sets X_i.

• 3. Each function f_i can be computed in a time of at most t and a space of at most s.

Our task is to count the satisfiable assignments of the function $f = \bigwedge _{i \in [ka]} f_{i}$.

We describe a satisfiability algorithm for function f. See Algorithm 1. To explain our algorithm, we need some notations. Let us consider a subset F of [ka]. Note that the number of such sets is 2^ka. For $F \subseteq [ka]$, $\bar {F}$ is defined as [ka] ∖ F. We define the set of variables $V_{F} := \left (\bigcup _{i \in F} X_{i} \right ) \setminus \left (\bigcup _{i \in \bar {F}}X_{i} \right )$. The set V_F contains all variables that belong to only $\bigcup _{i \in F} X_{i}$. By the definition, for any $F \in {\mathcal F}$, V_F and $V_{\bar {F}}$ are disjoint.

First, our algorithm finds a subset F of [ka] that maximizes $\min \limits \{ |V_{F}|, |V_{{\bar F}}|\}$ at Line 2. For this F, let Y be a set of variables $X \setminus \left (V_{F} \cup V_{\bar {F}}\right )$. That is, any variable x ∈ Y appears both in X_i and X_j for some i ∈ F and $j \in \bar {F}$. Let us pick up a partial assignment α whose support is Y. All functions f_i|_α for i ∈ F (resp. $i \in \bar {F}$) depend on only the variables in V_F (resp. $V_{\bar {F}}$). Let A_F be a set of partial assignments α_F such that S(α_F) = V_F and f_i|_α(α_F) = 1 for all i ∈ F. We find A_F by an exhaustive search, i.e., checking the value f_i|_α(α_F) for all i ∈ F and all partial assignments with S(α_F) = V_F in Lines 6–10. Similarly, we find $A_{\bar {F}}$ which is a set of partial assignments $\alpha _{\bar {F}}$ such that $S(\alpha _{\bar {F}}) = V_{\bar {F}}$ and $f_{i}|_{\alpha }(\alpha _{\bar {F}})=1$ for all $i \in \bar {F}$ by an exhaustive search in Lines 11–15. For any α_F ∈ A_F and any $\alpha _{\bar {F}} \in A_{\bar {F}}$, we have $f(\alpha \circ \alpha _{F} \circ \alpha _{\bar F})=1$ holds, since $f = \bigwedge _{i=1}^{ka} f_{i}$. Therefore, the number of assignments that satisfy f and contain a partial assignment α is exactly $|A_{F}| \cdot |A_{\bar {F}}|$. In the for-loop (Lines 4–17), we sum up $|A_{F}| \cdot |A_{\bar {F}}|$ for all partial assignments with support Y and then obtain the number of all assignments that satisfy f.

We give the other key lemma.

Lemma 3

Let a and k be positive integers with a ≤ n. Suppose that we are given a set of ka functions {f_i} (i ∈ [ka]) that satisfy the following properties:

• 1. Each f_i depends on only at most ⌈n/a⌉ variables X_i ⊂ X, i.e., |X_i|≤⌈n/a⌉.

• 2. Each variable x belongs to at most k sets X_i.

• 3. Each function f_i can be computed in a time of at most t and a space of at most s.

Then, there exists a deterministic algorithm for counting the satisfiable assignments of the function $f = \bigwedge _{i} f_{i}$ that runs in time $O\left (2^{ka}kan\right ) + O(kat) \cdot 2^{\left (1- \frac {2}{4^{k+1}}\left (1 - \frac {k}{a} \right )\right )n}$ and space O(s + kan).

Proof

Let us assume that each variable x belongs to at least one set X_i. If all sets X_i do not contain a variable x, then ${\sum }_{i} |X_{i}| \leq k (n-1)$. This implies that there exists a set X_i such that |X_i|≤ (n − 1)/a < ⌈n/a⌉. Then, we can put the variable x into the set X_i while preserving the properties.

First, Algorithm 1 requires the computational space O(kan) at Line 2, and O(s) for computing functions f_i|_α(α_F) and $f_{i}|_{\alpha }(\alpha _{\bar {F}})$ at Lines 7 and 12.

Next, we give the analysis of the complexity of Algorithm 1. At Line 2, we compute a subset F ∈ [ka] that maximizes $\min \limits \{ |V_{F}|, |V_{{\bar F}}|\}$. For each $F \subseteq [ka]$, we have $\min \limits \{ |V_{F}|, |V_{{\bar F}}|\}$ in O(kan) time. Therefore, Line 2 requires O(2^kakan) time since the number of subsets of [ka] is 2^ka.

Let us fix a partial assignment α with support Y in the for-loop of Lines 5–17. We construct A_F by checking the value f_i|_α(α_F) for all i ∈ F and all partial assignments with S(α_F) = V_F in Lines 6–10. Thus, Lines 6–10 require $t \cdot |F| \cdot 2^{|V_{F}|} \leq tka \cdot 2^{|V_{F}|}$ time. Similarly, Lines 11–15 require at most $tka\cdot 2^{|V_{\bar {F}}|}$ time to construct $A_{\bar {F}}$. Since we have 2^{|Y |} partial assignments with support Y, Lines 4–17 require at most ${tka\cdot 2^{|Y|} \cdot \left (2^{|V_{F}|} + 2^{|V_{\bar {F}}|}\right )}$ time. Because $|Y| + |V_{F}| + |V_{\bar {F}}| = n$, we have

$$ 2^{|Y|} \cdot \left( 2^{|V_{F}|} + 2^{|V_{\bar{F}}|} \right) \leq 2^{|Y|} \cdot \left( 2^{\max\{|V_{F}|, |V_{\bar{F}}|\} + 1} \right) = 2^{n - \min\{|V_{F}|, |V_{\bar{F}}| \} + 1}. $$

Totally, the running time of Algorithm 1 is at most

$$ \begin{array}{@{}rcl@{}} O(2^{ka}kan) + 2kat \cdot 2^{n - \min\{ |V_{F}|, |V_{{\bar F}}|\}}. \end{array} $$

We will show that $\max \limits _{F \subseteq [ka] } \min \limits \{ |V_{F}|, |V_{{\bar F}}|\}$ is at least $\frac {2}{4^{k+1}}\left (1 - \frac {k}{a} \right )n - \frac {1}{2}$. It follows that the second term of the running time is

$$ \begin{array}{@{}rcl@{}} 2kat \cdot 2^{n - \min\{ |V_{F}|, |V_{{\bar F}}|\}} & \leq & 2kat \cdot 2^{n- \frac{2}{4^{k+1}}\left( 1 - \frac{k}{a} \right)n + \frac{1}{2}} \\ & = & O(kat) \cdot 2^{\left( 1- \frac{2}{4^{k+1}}\left( 1 - \frac{k}{a} \right)\right)n}. \end{array} $$

Thus, it leads the lemma.

To analyze $\max \limits _{F \subseteq [ka] } \min \limits \{ |V_{F}|, |V_{{\bar F}}|\}$, let us suppose that n is even for simplicity. (In the case when n is odd, we also obtain the same result in a similar way.) Let S be the set of variables {x₁,…,x_n/2} and L be the set of variables {x_(n/2)+ 1,…,x_n}. Now, we define good/bad pairs of variables. This notation is used in the proof of Theorem 6 in [5]. A pair $(x,x^{\prime }) \in S \times L$ is good iff there is no i ∈ [ka] such that X_i contains both x and $x^{\prime }$, and bad otherwise. For each i, we have |S ∩ X_i|⋅|L ∩ X_i| pairs $(x,x^{\prime }) \in S \times L$ such that X_i contains both x and $x^{\prime }$. Since $|S\cap X_{i}| + |L\cap X_{i}| = |X_{i}|\leq \left \lceil \frac {n}{a} \right \rceil$ hold, we have

$$ \begin{array}{@{}rcl@{}} |S\cap X_{i}| \cdot |L\cap X_{i}| \leq \frac{1}{4}\cdot\left\lceil \frac{n}{a} \right\rceil^{2}. \end{array} $$

By the union bound, the number of bad pairs is at most $\frac {ka}{4} \cdot \left \lceil \frac {n}{a} \right \rceil ^{2}$. Thus, using $\left \lceil \frac {n}{a} \right \rceil < \frac {n}{a} + 1$ and a ≤ n, the number of good pairs is at least

$$ \begin{array}{@{}rcl@{}} |S| \cdot |L| - (\text{\#bad pairs}) \geq \frac{n^{2}}{4} - \frac{ka}{4} \cdot \left\lceil \frac{n}{a} \right\rceil^{2} > \frac{1}{4}\left( 1 - \frac{k}{a} \right)n^{2} - \frac{3k}{4}n. \end{array} $$

Let us consider that a subset $F \subseteq [ka]$ is chosen uniformly at random. For any variable x ∈ X, we have

$$ \mathop\mathbf{Pr}[x \in V_{F}] = {\prod}_{i \in \{ i \mid x \in X_{i} \}} \mathop\mathbf{Pr}[i \in F] \geq 2^{-k}, $$

since x belongs to at most k sets X_i. Also, we have $\mathop \mathbf {Pr}[x \in V_{\bar F}] \geq 2^{-k}$. Therefore, for each good pair $(x, x^{\prime }) \in S \times L$, we have $\mathop \mathbf {Pr}[x \in V_{F}, x^{\prime } \in V_{\bar {F}}] \geq 4^{-k}$. Hence, the average number of good pairs $(x, x^{\prime }) \in S \times L$ such that $x \in V_{F}, x^{\prime } \in V_{\bar {F}}$ is at least

$$ \frac{1}{4^{k}}\left[\frac{1}{4}\left( 1 - \frac{k}{a} \right)n^{2} - \frac{3kn}{4} \right]. $$

This implies that there exists a set $F \subseteq [ka]$ such that

$$ |V_{F}| \cdot |V_{\bar{F}}| \geq |S \cap V_{F}| \cdot |L \cap V_{\bar{F}}| \geq \frac{1}{4^{k}}\left[\frac{1}{4}\left( 1 - \frac{k}{a} \right)n^{2} - \frac{3kn}{4}\right]. $$

For such a set F, we have

$$ \begin{array}{@{}rcl@{}} \min\{ |S \cap V_{F}|, |L \cap V_{{\bar F}}|\} &=& \frac{ |S \cap V_{F}|\cdot |L \cap V_{{\bar F}}| }{\max\{ |S \cap V_{F}|, |L \cap V_{{\bar F}}|\}} \\&\geq& \frac{2}{4^{k}n}\left[\frac{1}{4}\left( 1 - \frac{k}{a} \right)n^{2} - \frac{3kn}{4}\right], \end{array} $$

since $\max \limits \{ |S \cap V_{F}|, |L \cap V_{\bar {F}}| \} \leq \max \limits \{ |S|, |L| \} = \frac {n}{2}$. Thus, we have

$$ \begin{array}{@{}rcl@{}} \min\{ |V_{F}|, |V_{{\bar F}}|\} &\geq& \min\{ |S \cap V_{F}|, |L \cap V_{{\bar F}}|\}\\ &\geq& \frac{2}{4^{k}n}\left[\frac{1}{4}\left( 1 - \frac{k}{a} \right)n^{2} - \frac{3kn}{4}\right]\\ &=& \frac{2}{4^{k+1}}\left( 1 - \frac{k}{a} \right)n - \frac{6k}{4^{k+1}}\\ &>& \frac{2}{4^{k+1}}\left( 1 - \frac{k}{a} \right)n - \frac{1}{2}. \end{array} $$

The last inequality is by the fact that for any $k\geq 1, \frac {6k}{4^{k+1}} < \frac {1}{2}$ holds. This means that

$$ \max_{F \subseteq [ka] } \min\{ |V_{F}|, |V_{{\bar F}}|\} \geq \frac{2}{4^{k+1}}\left( 1 - \frac{k}{a} \right)n - \frac{1}{2} $$

and the proof is complete. □

4 Satisfiability Algorithms for Syntactic Read-k-times BPs

4.1 Satisfiability Algorithm

In this section, we detail our satisfiability algorithm for syntactic read-k-times BPs and analyze its running time. We describe the outline of our algorithm. Our algorithm consists of two steps.

First, applying the decomposition algorithm in Lemma 1 with a = 2k, we decompose the input syntactic read-k-times BP B into a disjunction of at most $m^{2k^{2}}$ BPs. Then, B is satisfiable iff at least one of these decomposed BPs is satisfiable. In addition, each decomposed BP consists of a conjunction of at most 2k² BPs.

Second, we determine the satisfiability of each decomposed BP by checking whether there exists an assignment that satisfies all BPs. Let a decomposed BP be a conjunction of BPs {B₁,…,B_ℓ}, where ℓ ≤ 2k². Applying Lemma 3 with a = 2k, we count the number of satisfiable assignments that satisfy all BPs.

Repeating the above operations for all decomposed BPs, we can determine the satisfiability of the input B.

Theorem 3 (Restatement of Theorem 1)

There exists a deterministic and polynomial space algorithm for a nondeterministic and syntactic read-k-times BP SAT with n variables and m edges that runs in time $O\left (\text {poly}(n, m^{k^{2}}) \cdot 2^{(1-4^{-k-1})n}\right )$.

Proof

Our algorithm consists of the following two steps: (1) decomposition and (2) satisfiability checking.

[Step 1: Decomposition] :

Setting a = 2k in Lemma 1, construct the set of BPs {B_i,j} from the input B. Let f and f_i,j be Boolean functions represented by B and B_i,j, respectively. Let X_i,j be the set of variables that appear in B_i,j. Then, the following properties hold:

• 1. $f = \bigvee _{i \in [m^{2k^{2}}]} \bigwedge _{j \in [2k^{2}]} f_{i,j}$.

• 2. For each i and j, |X_i,j| is at most $\left \lceil \frac {n}{2k} \right \rceil$. For each i, each variable x belongs to at most k sets of $\{X_{i,j}\}_{j=1, \ldots , 2k^{2}}$.

The computational time required in Step 1 is at most $O\left (2k^{2}m^{2k^{2}+1}\right )$.

[Step 2: Satisfiability Checking] :

In order to check the satisfiability of B, we check whether there exists an assignment that satisfies all branching programs $B_{i,1}, \ldots , B_{i,2k^{2}}$ for each $i \in [m^{2k^{2}}]$. Let us consider a fixed i. We denote B_i,j, f_i,j, and X_i,j simply by B_j, f_j, and X_j, respectively. Note that each function f_j can be computed in O(m) time and O(m) space by simulating the computation of B_j.

Our goal in this step is to determine whether there is an assignment that satisfies all f_j for j ∈ [2k²]. By applying Lemma 3 and setting a = 2k, t = O(m), and s = O(m), we count the satisfiable assignments that satisfy all f_j in a time of at most

$$ \begin{array}{@{}rcl@{}} O\left( 2^{2k^{2}}k^{2}n\right) + O(k^{2}m) \cdot 2^{(1- \frac{1}{4^{k+1}})n}. \end{array} $$

Therefore, the running time of Step 2 is at most

$$ \begin{array}{@{}rcl@{}} m^{2k^{2}} \cdot \left\{ O\left( 2^{2k^{2}}k^{2}n\right) + O(k^{2}m) \cdot 2^{\left( 1- \frac{1}{4^{k+1}}\right)n} \right\} = \text{poly}\left( n, m^{k^{2}}\right) \cdot 2^{\left( 1- \frac{1}{4^{k+1}}\right)n}. \end{array} $$

Combining the analyses of Step 1 and Step 2, the running time of our algorithm is at most

$$ \begin{array}{@{}rcl@{}} O\left( 2k^{2}m^{2k^{2}+1}\right) + \text{poly}\left( n, m^{k^{2}}\right) \cdot 2^{\left( 1- \frac{1}{4^{k+1}}\right)n} =\text{poly}\left( n, m^{k^{2}}\right) \cdot 2^{\left( 1- \frac{1}{4^{k+1}}\right)n}. \end{array} $$

Note that if a given B is a deterministic and syntactic read-k-times BP, then any satisfiable assignment of B satisfies only one conjunction part of the decomposed BPs. Then, the number of satisfiable assignments of B is equal to the sum of the results of Step 2. □

4.2 Improved Algorithm for k = 2

By Theorem 1, we can solve the satisfiability of syntactic read-twice BPs in time poly(n,m) ⋅ 2^63n/64. We improve this bounds to poly(n,m) ⋅ 2^5n/6.

Theorem 4 (Restatement of Theorem 2)

There exists a deterministic and polynomial space algorithm for a nondeterministic and syntactic read-twice BP SAT with n variables and m edges that runs in time $O\left (\text {poly}(n, m) \cdot 2^{5n/6}\right )$.

To prove theorem, we improve the analysis of the running time of Algorithm 1 when k = a = 2. Note that Lemma 3 does not give the upper bound of the running time when k = a holds.

Lemma 4

Suppose that we are given a set of four functions f_i (i = 1,2,3,4) that satisfy the following properties:

• 1. Each f_i depends on only at most ⌈n/2⌉ variables X_i ⊂ X, i.e., |X_i|≤⌈n/2⌉.

• 2. Each variable x belongs to at most two sets X_i.

• 3. Each function f_i can be computed in a time of at most t and a space of at most s.

Then, there exists a deterministic algorithm for counting the satisfiable assignments of the function $f = \bigwedge _{i} f_{i}$ that runs in time O(n) + O(t) ⋅ 2^5n/6 and space O(s + n).

Proof

By the same way of the proof of Lemma 3, we assume that each variable x belongs to at least one set X_i. By Lemma 3, Algorithm 1 requires the computational space O(s + kan) = O(s + n). Recall that for a set $F \subseteq [4]$, V_F is a set of variables that belong to only $\bigcup _{i \in F} X_{i}$. The running time of Algorithm 1 is at most

$$ O(n) + 8t \cdot 2^{n - \min\{ |V_{F}|, |V_{\bar{F}}| \}} $$

from the proof of Lemma 3 with k = a = 2. To complete the proof, we need to show that

$$ \max_{F \subseteq [4] }\min\{ |V_{F}|, |V_{\bar{F}}| \} \geq \frac{n}{6}. $$

We show the following lemma and give the proof later.

Lemma 5

Let w_i and v_i,j be non-negative real values, where i,j ∈ [4] and i≠j such that the following equations hold.

• 1. v_i,j = v_j,i,

• 2. for each i, $w_{i} +{\sum }_{j \neq i} v_{i, j} \leq 1/2$,

• 3. ${\sum }_{i \in [4]} w_{i} +{\sum }_{i, j \in [4], i < j} v_{i, j} = 1$.

Let x_i,j = w_i + w_j + v_i,j. Then,

$$ \max \left\{ \min\{ x_{1,2}, x_{3,4}\}, \min\{ x_{1,3}, x_{2,4}\}, \min\{ x_{1,4}, x_{2,3}\} \right\} \geq 1/6 $$

holds.

For i ∈ [4], we set w_i as the proportion of variables in only X_i. For i,j ∈ [4], we set v_i,j as the proportion of variables in both X_i and X_j. Under this setting, x_i,j = w_i + w_j + v_i,j corresponds that the proportion of variables in only X_i or X_j. Thus, we have $x_{i,j} = \frac {|V_{F}|}{n}$ with F = {i,j}. In order to apply Lemma 5, we need to confirm all conditions hold under this setting. By the symmetry of the setting of v_i,j, condition 1 clearly holds. The left side term $w_{i} + {\sum }_{j \neq i}v_{i,j}$ of condition 2 corresponds to a portion of variables that contains in X_i. By the property 1 of the statement of Lemma, condition 2 holds. The left side of condition 3 corresponds to a portion of variables that is in some set X_i, then condition 3 clearly holds. Thus, Lemma 5 implies that there exits a subset F of size two such that

$$ \begin{array}{@{}rcl@{}} \min \{ |V_{F}|, |V_{\bar{F}}| \} \geq n/6. \end{array} $$

It completes the proof. □

Proof Proof of Lemma 5

Without loss of generality, we can assume that one of the following two cases holds: (i) $\min \limits \{x_{1,2}, x_{3,4}\}=x_{1,2}$, $\min \limits \{x_{1,3}, x_{2,4}\}=x_{1,3}$, $\min \limits \{ x_{1,4}, x_{2,3}\}=x_{1,4}$ and (ii) $\min \limits \{x_{1,2}, x_{3,4}\}=x_{1,2}$, $\min \limits \{x_{1,3}, x_{2,4}\}=x_{1,3}$, $\min \limits \{ x_{1,4}, x_{2,3}\}=x_{2,3}$.

• (i) Let us assume that $\min \limits \{x_{1,2}, x_{3,4}\}=x_{1,2}$, $\min \limits \{x_{1,3}, x_{2,4}\}=x_{1,3}$, $\min \limits \{ x_{1,4}, x_{2,3}\}=x_{1,4}$. By x_1,i = w₁ + w_i + v_1,i for each i ∈{2,3,4}, we have $\max \limits \{x_{1,2}, x_{1,3}, x_{1,4}\} = w_{1} + \max \limits _{i \in \{2,3,4\}}\{w_{i} + v_{1,i} \}$. Recall the condition 2 that $w_{i} + {\sum }_{j \neq i} v_{i, j} \leq 1/2$ holds for each i. Summing up this inequality for i = 2,3,4, we have

  $$ \begin{array}{@{}rcl@{}} {}\sum\limits_{i \in \{2,3,4\}}\left( w_{i} + v_{1,i} \right) + 2\cdot (v_{2,3} + v_{2,4} + v_{3,4}) \!&\leq&\! \frac{3}{2} \\ v_{2,3} + v_{2,4} + v_{3,4} \!&\leq&\! \frac{3}{4} - \frac{{\sum}_{i \in \{2,3,4\}}\left( w_{i} + v_{1,i}\right)}{2}. \end{array} $$

  (2)

  Recalling we have condition 3 that ${\sum }_{i \in [4]} w_{i} +{\sum }_{i, j \in [4], i < j} v_{i, j} = 1$, we have

  $$ \begin{array}{@{}rcl@{}} 1 &=& \sum\limits_{i \in [4]} w_{i} +\sum\limits_{i, j \in [4], i < j} v_{i, j}\\ &=& w_{1} + \sum\limits_{i \in \{2,3,4\}}\left( w_{i} + v_{1,i}\right) + v_{2,3} + v_{2,4} + v_{3,4} \\ & \leq & w_{1} + \frac{ {\sum}_{i \in \{2,3,4\}}\left( w_{i} + v_{1,i} \right) }{2} + \frac{3}{4}. \end{array} $$

  The last inequality led by inequality (2). Simplifying the above inequality, we have

  $$ \begin{array}{@{}rcl@{}} \sum\limits_{i \in \{2,3,4\}}\left( w_{i} + v_{1,i} \right) \geq \frac{1}{2} - 2w_{1}. \end{array} $$

  (3)

  Therefore, we have

  $$ \begin{array}{@{}rcl@{}} w_{1} + \max_{i \in \{2,3,4\}}\{w_{i} + v_{1,i} \} &\geq& w_{1} + \frac{1}{3} \sum\limits_{i \in \{2,3,4\}}\left( w_{i} + v_{1,i} \right) \\ &\geq& w_{1} + \frac{1}{6} - \frac{2}{3}w_{1} \quad (\because \text{By inequality~{(3)}}) \\ &=& \frac{1}{6} + \frac{1}{3}w_{1} \geq \frac{1}{6}. \end{array} $$

• (ii) Let we assume that $\min \limits \{x_{1,2}, x_{3,4}\}=x_{1,2}$, $\min \limits \{x_{1,3}, x_{2,4}\}=x_{1,3}$ and $\min \limits \{ x_{1,4}, x_{2,3}\}=x_{2,3}$ hold. Recalling condition 3 again, we have

  $$ \begin{array}{@{}rcl@{}} 1 &=& \sum\limits_{i \in [4]} w_{i} +\sum\limits_{i, j \in [4], i < j} v_{i, j}\\ &=& x_{1,2} + x_{1,3} + x_{2,3} - \sum\limits_{i \in \{1,2,3\}}w_{i} + w_{4} + \sum\limits_{i \in\{1,2,3\}} v_{i,4} \\ &\leq & x_{1,2} + x_{1,3}+ x_{2,3} +1/2. \quad\quad(\because \text{By condition~2}) \end{array} $$

  Thus, we have x_1,2 + x_1,3 + x_2,3 ≥ 1/2 and this implies that $\max \limits \{x_{1,2},$ x_1,3,x_2,3}≥ 1/6 holds.

□

Proof Proof of Theorem 2

Improved algorithm for k = 2 also consists of the following two steps: (1) decomposition and (2) satisfiability checking.

[Step 1: Decomposition] :

Setting a = 2 in Lemma 1, construct a set of BPs {B_i,j∣i ∈ [m⁴],j ∈ [4]} from the input BP B. Let f and f_i,j be Boolean functions represented by B and B_i,j, respectively. Let X_i,j be the set of variables that appear in B_i,j. By Lemma 1, the following properties hold:

• 1. $f = \bigvee _{i \in [m^{4}]} \bigwedge _{j \in [4]} f_{i,j}$.

• 2. For each i and j, |X_i,j| is at most n/2.

• 3. For each i, each variable x belongs to at most two sets of {X_i,1,X_i,2, X_i,3,X_i,4}.

The running time required in Step 1 is at most poly(m).

[Step 2: Satisfiability Checking] :

In order to check the satisfiability of B, we check whether there exists an assignment that satisfies all four branching programs B_i,1,B_i,2,B_i,3 and B_i,4 for each i ∈ [m⁴]. Let us consider a fixed i. We denote B_i,j, f_i,j, and X_i,j simply by B_j, f_j, and X_j, respectively. Note that each function f_j can be computed in O(m) time and O(m) space by simulating the computation of B_j.

Now, our task is to decide whether there is an assignment that satisfies all f_j, where j ∈ [4]. By applying Lemma 4 and setting t = O(m), and s = O(m), we count the satisfiable assignments that satisfy all f_j in a time of at most

$$ \begin{array}{@{}rcl@{}} O(n) + O(m) \cdot 2^{5n/6}. \end{array} $$

Therefore, the running time of Step 2 is at most

$$ \begin{array}{@{}rcl@{}} m^{4} \cdot \left\{ O(n) + O(m) \cdot 2^{5n/6} \right\} = \text{poly}(n, m) \cdot 2^{5n/6}. \end{array} $$

Since the running time of Step 1 is dominated by the one of Step 2, the total of running time for solving the satisfiability problem for read-twice BPs is at most poly(n,m) ⋅ 2^5n/6. □