The phase transition in random regular exact (3 s + s,k )-SAT problem

Abstract

A CNF formula with each clause of length k and each variable occurring 4s times, where positive occurrences are 3s and negative occurrences are s, is a regular (3s + s, k)-CNF formula (F _3s+s,k formula). The random regular exact (3s + s, k)-SAT problem is whether there exists a set of Boolean variable assignments such that exactly one literal is true for each clause in the F _3s+s,k formula. By introducing a random instance generation model, the satisfiability phase transition of the solution is analyzed by using the first moment method, the second moment method, and the small subgraph conditioning method, which gives the phase transition point s* of the random regular exact (3s + s, k)-SAT problem for k≥3. When s < s*, F _3s+s,k formula is satisfiable with high probability; when s > s*, F _3s+s,k formula is unsatisfiable with high probability. Finally, through the experimental verification, the results show that the theoretical proofs are consistent with the experimental results.

Keywords

first moment method second moment method small subgraph conditioning method phase transition

1 Introduction

The satisfiability (SAT) problem is NP-hard problem, and the SAT problem with each clause of length k is a k-SAT problem, and the k-SAT problem with randomly generated variables of size n is called a random k-SAT problem [13]. The random regular exact (3s + s, k)-SAT problem is whether there exists a set of variable assignments such that exactly one literal is true for each clause in the (3s + s, k)-CNF formula. Obviously, the random regular exact (3s + s, k)-SAT problem is still NP-hard [11] problem. For the random k-SAT problem, researchers found that the ratio α (constraint density) of the number of clauses m to the number of variables n is closely related to the satisfiability phase transition of the random k-SAT problem, and this ratio portrays the degree of intractability and the critical features of the solution for the random k-SAT problem instances. However, the constraint density α is constant for the regular exact SAT problem, and thus α cannot measure the degree of intractability and the phase transition for the regular exact SAT problem instances. Therefore, the study of satisfiability phase transition of random regular exact (3s + s, k)-SAT problem is instructive for analyzing the phase transition threshold of regular (d,k)-SAT problem.

The regular (d,k)-SAT problem is a k-SAT problem in which the variable occurs d times, and it is worth noting that any k-SAT instance can be converted to the regular (d,k)-SAT problem. In order to understand the difficulty of solving the SAT problem, it is necessary to study the distribution pattern of the solutions to the problem and analyze the degree of difficulty in solving it. At present, the satisfiability phase transition of the random regular exact (3s + s, k)-SAT problem is still unclear, and there is a need to find new parameters to measure the satisfiability phase transition of the problem. For the similar problem of this problem, researchers have obtained some important research results on the satisfiability phase transition, which are important references for analyzing the satisfiability phase transition of the random regular exact (3s + s, k)-SAT problem. Achlioptas et al. [1] gave the satisfiability phase transition for the 3-NAE-SAT problem by the differential equation method and proved the existence of a nonuniform threshold. Further, Achlioptas et al. [2] applied the second moment method to give the satisfiability phase transition for the k-NAE-SAT problem and the random hypergraph 2-colourability problem. Subsequently, Coja-Oglan et al. [3] proposed a survey propagation based the second moment method for proving the random k-NAE-SAT problem [18]. Ding et al. [4] gave the satisfiability phase transition for the random regular (d,k)-NAE-SAT problem with phase transition control parameters. The satisfiability problem of making exactly one literal true in each clause under a set of variable assignments is called the exact satisfiability problem. For the 1-in-k-SAT problem, assuming that each clause does not contain negative literal, the problem is the exact cover problem of the set (positive 1-in-k-SAT). Knysh et al. [5] and Kalapala et al. [6] applied the differential equation method to give the satisfiability phase transition for the Positive 1-in-3-SAT problem. Moore [7] gave the satisfiability phase transition for the Positive 1-in-k-SAT problem and proved a lower bound on the satisfiability threshold by the small subgraph conditioning method. Panagiotou et al. [8] applied the second moment method and the small subgraph conditioning method to give the satisfiability phase transition for the 2-in-4-SAT problem. Wang et al. [9] gave the satisfiability phase transition for the balance regular exact (2 s,k)-SAT problem. Nie et al. [19] applied the first moment method and the second moment method to give the satisfiability phase transition for the random regular exact 2-(d,k)-SAT problem.

The main techniques for analyzing phase transition used in the above research results are the differential equation method, the first moment method and the second moment method. However, when the second moment method is applied to analyze the phase transition, it is very difficult to characterize the solution space structure of the problem. In analyzing the satisfiability phase transition of the random regular exact (3s + s, k)-SAT problem, a random instance generation model for the problem is introduced. The instance generation model adopts a perfect matching mechanism, in which the positive literal of each variable is replicated 3s times and the negative literal is replicated s times to form 4sn variable nodes; each clause is replicated k times to form mk clause nodes. A random perfect matching of variable nodes and clause nodes corresponds to a random regular (3s + s, k)-SAT instance.

In this paper, by introducing a generative model for random regular exact (3s + s, k)-SAT instances, we apply the first moment method, the second moment method, and the small subgraph conditioning method to analyze the satisfiability phase transition of the random regular exact (3s + s, k)-SAT problem and to give the phase transition point with respect to parameter s. Numerical experiments on two sets of random regular exact (3s + s, k)-SAT instances with k = 4 and k = 6 are carried out by taking the variable size n = 10, and the theoretical proofs are verified to be consistent with the experimental results.

2 Random regular exact (3s + s, k)-SAT instance generation model

Let the set of Boolean variables V = {x₁, x₂, . . . , x_n}. A Boolean variable x_i (1 ≤ i ≤ n) or the negation of Boolean variable ¬x_i is called a literal L. The disjunction of several literals represents a clause, denoted as C = L₁ ∨ L₂ ∨ L₃ ∨ . . . ∨ L_n, and the conjunction of several clauses composes a Conjunctive Normal Form (CNF), denoted as F = C₁ ∧ C₂ ∧ … ∧ C_m [20].

Let the set of Boolean variables V = {x₁, x₂, . . . , x_n}, and copy each variable 4s times to obtain the following variable matrix V ^*,

V^{*} = (\begin{matrix} x_{1, 1} & x_{1, 2} & \dots & x_{1, 4 s} \\ x_{2, 1} & x_{2, 2} & \dots & x_{2, 4 s} \\ ⋮ & ⋮ & ⋱ & ⋮ \\ x_{n, 1} & x_{n, 2} & \dots & x_{n, 4 s} \end{matrix}),

where x_n,4s is a Boolean variable.

Let the CNF formula F = (C₁ ∧ C₂ . . . ∧ C_m), and copy each clause k times to obtain the following position matrix F ^*,

F^{*} = (\begin{matrix} C_{1, 1} & C_{1, 2} & \dots & C_{1, k} \\ C_{2, 1} & C_{2, 2} & \dots & C_{2, k} \\ ⋮ & ⋮ & ⋱ & ⋮ \\ C_{m, 1} & C_{m, 2} & \dots & C_{m, k} \end{matrix}),

where C_m,k is a clause.

Note: For a regular (3s + s, k)-CNF formula, there is 4sn = mk.

Generate a random regular exact (3s + s, k)-SAT instance by following the steps below:

– –
Generate an unsigned formula: On the set S = {1, 2, ⋯ , mk}, the sample space is formed by all possible permutations, and there are (mk)! different permutations in the sample space. A permutation π is chosen at random to generate an unsigned formula.
–
Realization of the symbol matrix R : For each row i (1 ≤ i ≤ n, n ∈ N⁺)in the variable matrix V ^, choose any 3s subset in the set Q = {1, 2, ⋯ , 4s} and divide Q into two parts, +R_i and -R_i. After assigning positive “+” and negative “–” to +R_i and -R_i respectively, different rows of symbols are formed, which are denoted as $+ R_{i}^{1}$ and $- R_{i}^{0}$ . The total number of rows with symbols is $C_{4 s}^{3 s} = (4 s)! / [s! (3 s)!]$ . According to the column labels indicated by the set, an exact position symbol row R_i (row i of the symbol matrix R ) is formed. For each row of the symbol matrix R , there are $C_{4 s}^{3 s}$ such divisions. Thus, for n rows and 4s columns of the symbol matrix R there are $(C_{4 s}^{3 s})^{n}$ . The action of R on V ^ is called a realization. R ( V ^) is said to be a literal matrix by assigning symbols to the corresponding positions of the variable matrix V ^.
–
Generate random regular exact (3s + s, k)-SAT instance: Randomly take a permutation π and symbol matrix R , and use π as a one-to-one mapping from R ( V ^) to F ^, which corresponds to generating a random regular exact (3s + s, k)-SAT instance. The clause form is π (x_i,p) = C_j,q ⇔ R (x_i) ∈ C_j, where R (x_i) is determined by the symbols in the symbol matrix R with position (i, p). Thus, the number of random regular (3s + s, k)-SAT instances generated is $(C_{4 s}^{3 s})^{n} \cdot (mk)!$ .

3 Methods for phase transition analysis

For the study of satisfiability phase transitions of random regular SAT problems, the first moment method [17, 19] and the second moment method [14, 15] are mainly used. However, the use of the small subgraph conditioning method [10, 16] to study this problem provides new possibilities and accuracy. We write f (n) ∼ g (n) if $lim_{n \to \infty} f (n) / g (n) = 1$ . We say that a series of events E_n has high probability if $lim_{n \to \infty} Pr [E_{n}] \sim 1$ . The mathematical principles of these three methods of phase transition analysis are briefly described below.

3.1 First moment method

Let Z(n) be a random variable, and Z(n)≥0, then for any real number ξ > 0,we have

Pr [Z (n) \geq ξ] \leq \frac{E [Z (n)]}{ξ} .

(1)

The theoretical basis of the first moment method is Markov inequality. By proving that $lim_{n \to \infty} E [Z (n)] = 0$ , we have $lim_{n \to \infty} Pr [Z (n) \geq 1] \leq 0$ , thus the random regular SAT instance is high probability unsatisfiable.

3.2 Second moment method

Let Z(n) be a random variable, E[Z(n)] and D[Z(n)] denote the expectation and variance of the random variable Z(n), respectively, and we have

Pr [| Z (n) - E [Z (n)] | \geq E [Z (n)]] \leq \frac{D [Z (n)]}{E^{2} [Z (n)]} .

(2)

The theoretical basis of the second moment method is Chebyshev inequality. By proving that $lim_{n \to \infty} E [Z^{2} (n)] = lim_{n \to \infty} E^{2} [Z (n)] \cdot [1 + o (1)]$ , there is $lim_{n \to \infty} Pr [Z = 0] = 0 \Leftrightarrow lim_{n \to \infty} Pr [Z \geq 1] = 1$ , thus the random regular SAT instance is satisfiable with high probability.

3.3 Small subgraph conditioning method

Let Z, X₁, X₂, ⋯ X_n, ⋯ be random variables with non-negative integer values. Suppose E [Z] >0, and for ∀i ≥ 1, ∃ λ_i > 0, δ_i > -1 (λ_i and δ_i are constants), such that the following conditions are satisfied.

–For ∀j, X₁, X₂, ⋯ X_j obey approximately independent Poisson distribution, and E [X_i] ∼ λ_i.

–For ∀j, a non-negative integer series m₁, m₂, ⋯ , m_j, there is

\frac{E [Z {[X_{1}]}_{m_{1}} \dots {[X_{j}]}_{m_{j}}]}{E [Z]} \sim \prod_{i = 1}^{j} μ_{i}^{m_{i}},

(3)

where μ_i = λ_i (1 + δ_i).

$- \sum_{i = 1}^{\infty} λ_{i} δ_{i}^{2} < \infty$ , and

\frac{E [Z^{2}]}{E^{2} [Z]} \sim exp (\sum_{i = 1}^{\infty} λ_{i} δ_{i}^{2}) .

(4)

Then Pr [Z ≥ 1] =1 - o (1).

The principle of the small subgraph conditioning method is that by using the cycle counts to follow a Poisson distribution approximately, multiple cycles follow an approximately independent Poisson distribution. Then, the weighted probability space is constructed by solution counting, and the Poisson distribution is analyzed in the weighted space, so the random regular SAT instance is satisfiable with high probability.

4 Main results

Theorem 1.F_3s+s,k is an instance of the random regular exact (3s + s, k)-SAT problem, let

s^{*} = \frac{1}{4} \cdot (ln \frac{3}{2} + \frac{1}{2}) \cdot \frac{k}{k - 1} \cdot \frac{1}{ln k - ln (k - 1)} .

For any k≥3 and any integer s,

lim_{n \to \infty} Pr [F_{3 s + s, k} is satisfiable] = {\begin{matrix} 0 (s > s^{*}) \\ 1 (s < s^{*}) \end{matrix} .

Theorem 1 shows that when k≥3, for an F_3s+s,k instance, if s > s*, then F_3s+s,k is unsatisfiable with high probability; if s < s*, then F_3s+s,k is satisfiable with high probability. First, by using the first moment method and the second moment method, it is given that F_3s+s,k is not satisfiable with high probability when s > s* and is satisfiable with high probability when s < s*, respectively. Then, the latter is proved to be satisfiable with high probability by the small subgraph conditioning method. Proof of the following two lemmas to prove Theorem 1.

Lemma 1. For k≥3, when s > s*, then F_3s+s,k is unsatisfiable with high probability.

Lemma 2. For k≥3, when s < s*, then F_3s+s,k is satisfiable with high probability.

4.1 Lemma 1 Proof

Let F_3s+s,k = {C₁, C₂, ⋯ , C_m} be a random regular (3s + s, k)-SAT instance. Let there be a truth assignment δ = {δ₁, δ₂, ⋯ , δ_n} on the set V = {x₁, x₂, . . . , x_n} of Boolean variables, where δ_i ∈ {0, 1}. Let Z be the number of satisfiable assignments T (the number of solutions to a random F_3s+s,k instance), where |T| = n. The satisfiable assignments T = {l₁, l₂, ⋯ , l_n} are the set of literals corresponding to V that take on true values, with

l_{i} = {\begin{matrix} x_{i}, if v (x_{i}) = 1 \\ \neg x_{i}, if v (x_{i}) = 0 \end{matrix} .

The random regular exact (3s + s, k)-SAT problem is whether there exists an assignment T such that exactly one literal in each clause C_j is true, i.e., |T ∩ C_j|=1. Construct an realization R ( V ^*) that contains elements of a satisfying assignment T, replacing one element on each row of F ^* with an element of T, and no more than m (m clauses) rows can be replaced. Since one element is replaced in k positions in each row, there are m ! k^m possibilities for such permutations.

The k-1 empty positions in each row after the permutation are filled by eliminating the elements in T from R ( V ^*), and there are (mk - m) ! possibilities for such permutations. There are $(C_{4 s - 1}^{3 s - 1})^{n} + (C_{4 s - 1}^{s - 1})^{n}$ possibilities of realization R ( V ^*) by inclusion of satisfiable assignments T = {l₁, l₂, ⋯ , l_n}, so the number of formulas that can be satisfied in the instance is $2^{n} [(C_{4 s - 1}^{3 s - 1})^{n} + (C_{4 s - 1}^{s - 1})^{n}] \cdot m! k^{m} (mk - m)!$ . Applying the Stirling formula $x! = (1 + o (1)) \sqrt{2 π x} \cdot x^{x} e^{- x}$ gives the mathematical expectation of Z as:

\begin{matrix} E [Z] = \frac{2^{n} \cdot [{(C_{4 s - 1}^{3 s - 1})}^{n} + {(C_{4 s - 1}^{s - 1})}^{n}] \cdot m! k^{m} \cdot (mk - m)!}{{(C_{4 s}^{3 s})}^{n} \cdot (mk)!} \\ = \frac{2^{n} \cdot k^{m}}{C_{km}^{m}} \cdot [{(\frac{3}{4})}^{n} + {(\frac{1}{4})}^{n}] \\ = \sqrt{2 π (1 - \frac{1}{k})} \cdot [{(\frac{3}{4})}^{n} + {(\frac{1}{4})}^{n}] \\ \cdot exp [- 4 snH (\frac{1}{k}) + \frac{1}{2} ln \frac{4 sn}{k} + n ln 2 + \frac{4 sn}{k} ln k] \\ \leq \sqrt{2 π (1 - \frac{1}{k}) \frac{4 s}{k}} \cdot [{(\frac{3}{4})}^{n} + {(\frac{1}{4})}^{n}] \\ \cdot exp {n \cdot [- 4 sH (\frac{1}{k}) + \frac{1}{2} + ln 2 + \frac{4 s}{k} ln k]} \\ = \sqrt{2 π (1 - \frac{1}{k}) \frac{4 s}{k}} \cdot (exp [n φ_{1} (s)] + exp [n φ_{2} (s)]) . \end{matrix}

Set function

\begin{matrix} φ_{1} (s) = - 4 sH (\frac{1}{k}) + \frac{4 s}{k} ln k + ln \frac{3}{2} + \frac{1}{2}, \\ φ_{2} (s) = - 4 sH (\frac{1}{k}) + \frac{4 s}{k} ln k + ln \frac{1}{2} + \frac{1}{2}, \end{matrix}

where H (α) is the entropy function,

H (α) = - α ln (α) - (1 - α) ln (1 - α) .

Then we have

\begin{matrix} φ_{1} (s) = 4 s (1 - \frac{1}{k}) ln (1 - \frac{1}{k}) + ln \frac{3}{2} + \frac{1}{2}, \\ φ_{2} (s) = 4 s (1 - \frac{1}{k}) ln (1 - \frac{1}{k}) + ln \frac{1}{2} + \frac{1}{2} . \end{matrix}

When k ≥ 3 can be verified, the function φ₁ (s) and function φ₂ (s) are monotonically decreasing functions with regard to s respectively (see Fig. 1) and there are unique zeros s₁ and s₂, and s₁ > s₂. Therefore, we have

Fig. 1

Image of function φ(s) (k=4).

s^{*} = s_{1} = \frac{1}{4} \cdot (ln \frac{3}{2} + \frac{1}{2}) \cdot \frac{k}{k - 1} \cdot \frac{1}{ln k - ln (k - 1)} .

By the first moment method of Section 3.1 and the Markov inequality, it is sufficient to show that

lim_{n \to \infty} E [Z] = 0

holds, and Lemma 1 follows. Since φ₁ (s) =0 when s = s^*, and φ₁ (s) is a monotonically decreasing function with regard to s, there is

\underset{n \to \infty}{Pr} [Z > 0] \leq lim_{n \to \infty} E [Z] = lim_{n \to \infty} exp [- Ω (n)] = 0

when s > s^*. Therefore, when k ≥ 3 and s > s^*, the random regular exact (3s + s, k)-SAT problem is unsatisfiable with high probability, and Lemma 1 is proved.

4.2 Lemma 2 Proof

4.2.1 Proof and analysis by second moment method

The second moment method focuses on proving E [Z²]/E [Z] ² ∼ c, where c is a constant. Let F_3s+s,k = {C₁, C₂, ⋯ , C_m} be a random regular (3s + s, k)-SAT instance. Assuming that the formula for F_3s+s,k is satisfiable, there are a satisfiable assignments {T₁, T₂, ⋯ , T_a}. An assignment pair (T_i, T_j) is said to satisfies the F_3s+s,k formula if both assignments T_i and T_j satisfy the F_3s+s,k formula. Take variable Z to denote the number of assignments that satisfy the F_3s+s,k formula and variable Y to denote the number of assignment pairs that satisfy F_3s+s,k formula, we have Z = a ⇔ Y = a². Consider the set of assignment pairs {(T_i, T_j) :1 ≤ i, j ≤ a} consisting of a² assignment pairs and divide it into n + 1 classes. When |T_i - T_j| = |T_i′ - T_j′| = a, the assignment pair (T_i, T_j) and the assignment pair (T_i′, T_j′) are said to be in the same class, denoted as P_a = {(T_i, T_j) : |T_i - T_j| = a}. Obviously, P₀, P₁, ⋯ , P_n forms a partition of the set of assigned pairs with |P₀| + |P₁| + ⋯ + |P_n| = a². In order to express the summation in integral form, a normalization parameter ω, (0 ≤ ω ≤ 1) is introduced. Noting that Q_ω = P_ωn = {(T_i, T_j) : |T_i - T_j| = ωn}, the following conditions are satisfied in the Q_ω block:

\begin{matrix} | T_{i} - T_{j} | = | T_{j} - T_{i} | = ω n; | T_{i} \cap T_{j} | \\ = (1 - ω) n; | T_{i} \cup T_{j} | = (1 + ω) n . \end{matrix}

Specify a set T_i of size n, the number of sets T_i satisfying the above condition is

(2^{ω n} - 1) \cdot C_{n}^{(1 - ω) n}

, then

| Q_{ω} | = (2^{ω n} - 1) \cdot C_{n}^{ω n} \cdot 2^{(1 - ω) n} \approx 2^{n} \cdot C_{n}^{ω n}

.Take a set of satisfiable assignment pairs (T, T′) as an example, and calculate the number of satisfied formulas that can be generated. Let assignment

\begin{matrix} T = {l_{1}, \dots, l_{ω n}, l_{ω n + 1}, \dots, l_{n}}, \\ T^{'} = {l_{ω n + 1}, \dots, l_{n}, l_{n + 1}, \dots, l_{(1 + ω) n}}, \end{matrix}

with the following relations:

\begin{matrix} T - T^{'} = {l_{1}, \dots, l_{ω n}}; T^{'} - \\ T = {l_{n + 1}, \dots, l_{(1 + ω) n}}; T \cap T^{'} = {l_{ω n + 1}, . . ., l_{n}}; \\ T \cup T^{'} = {l_{1}, \dots, l_{ω n}, l_{ω n + 1}, \dots, l_{n}, \\ l_{n + 1}, \dots, l_{(1 + ω) n}}; \bar{T \cup T^{'}} = {l_{(1 + ω) n + 1}, \dots, l_{n}} . \end{matrix}

For each clause C_j in F_3s+s,k formula, we have |C_j ∩ T|=1, |C_j ∩ T′|=1. Calculate the number of formulas that are satisfied by assignment pair (T, T′) according to the matching relationship that satisfies the assignment and clause position. Due to |T - T′| = |T - T′| = ωn, we know that the number of clauses matched by this part of the literal is ωm. Since this part of the literal is not the same in T and T′, the number of permutations corresponding to this part of the literal is [(ωm) !] ² · [k (k - 1)] ^ωm. Due to |T ∩ T′| = (1 - ω) n, we know that the number of clauses matched by this part of the literal is (1 - ω) n · (m/n) = (1 - ω) m. Since this part of the literal is the same in T and T′, the number of permutations corresponding to this part of the literal is k^[(1-ω)m] · [(1 - ω) m] !. After the above matches, the number of complete permutations corresponding to the remaining empty positions of the position matrix is [m (k - 1 - ω)] !. From the definition of realization, the realization containing T′ is denoted as R _T′ ( V ^*). For different parts of the assignment pair (T, T′), the realization R _T-T′ ( V ^*) of the assignment pair (T, T′) has

(C_{4 s - 1}^{3 s - 1})^{ω n} + (C_{4 s - 1}^{s - 1})^{ω n}

possibilities if the positive literal in the formula F_3s+s,k occurs 3s times and the negative literal in the formula F_3s+s,k occurs s times. For the parts which are identical in the assignment pair (T, T′), the realization R _T∩T′ ( V ^*) of the assignment pair (T, T′) has

(C_{4 s - 1}^{3 s - 1})^{(1 - ω) n}

possibilities. Thus, for the given assignments T and T′, the number of formulas satisfied by the assignment pair (T, T′) is

\begin{matrix} C_{m}^{ω m} \cdot [(ω m)!]^{2} \cdot [k (k - 1)]^{ω m} \\ \cdot k^{[(1 - ω) m]} \cdot [(1 - ω) m]! \\ \cdot [m (k - 1 - ω)]! \cdot [(C_{4 s - 1}^{3 s - 1})^{ω n} + (C_{4 s - 1}^{s - 1})^{ω n}] \\ \cdot (C_{4 s - 1}^{3 s - 1})^{(1 - ω) n} \\ = [1 + {(\frac{1}{3})}^{ω n}] \cdot (C_{4 s - 1}^{3 s - 1})^{n} \cdot k^{m} \cdot (k - 1)^{ω m} \\ \cdot m! \cdot (ω m)! \\ \cdot [m (k - 1 - ω)]! . \end{matrix}

To sum up, the number of formulas satisfied by a pair of assignment pairs (T, T′) in the Q_ω block is

\begin{matrix} [1 + {(\frac{1}{3})}^{ω n}] (C_{4 s - 1}^{3 s - 1})^{n} \cdot k^{m} (k - 1)^{ω m} \cdot m! \cdot (ω m)! \\ \cdot [m (k - 1 - ω)]! . \end{matrix}

The number of formulas satisfied by all assignment pairs in the Q_ω block is

\begin{matrix} | Q_{ω} | \cdot [1 + {(\frac{1}{3})}^{ω n}] \cdot (C_{4 s - 1}^{3 s - 1})^{n} \cdot k^{m} \cdot \\ (k - 1)^{ω m} \cdot m! \cdot (ω m)! \\ \cdot [m (k - 1 - ω)]! . \end{matrix}

Let

Z_{ω}^{(2)}

denote the count of randomly drawn formulae being satisfied by assigned pairs in the Q_ω block, then we have

\begin{matrix} E [Z_{ω}^{(2)}] = \frac{2^{n} \cdot C_{n}^{ω n} \cdot [1 + {(\frac{1}{3})}^{ω n}] \cdot {(C_{4 s - 1}^{3 s - 1})}^{n}}{{(C_{4 s}^{3 s})}^{n} \cdot (mk)!} \\ \cdot k^{m} \cdot (k - 1)^{ω m} \cdot m! \cdot (ω m)! \cdot [m (k - 1 - ω)]! . \\ = E [Z] \cdot (k - 1)^{ω n} \cdot C_{n}^{ω n} \cdot \frac{(ω m)! \cdot [m (k - 1) - ω m]!}{[m (k - 1)]!} \\ \cdot \frac{[1 + {(\frac{1}{3})}^{ω n}] \cdot {(\frac{3}{4})}^{n}}{[{(\frac{3}{4})}^{n} + {(\frac{1}{4})}^{n}]} \\ = E [Z] \cdot (k - 1)^{ω n} \cdot \frac{C_{n}^{ω n}}{C_{m (k - 1)}^{ω m}} \cdot \frac{[1 + {(\frac{1}{3})}^{ω n}] \cdot {(\frac{3}{4})}^{n}}{[{(\frac{3}{4})}^{n} + {(\frac{1}{4})}^{n}]} . \end{matrix}

Applying the combined approximation formula

C_{n}^{α n} \approx \frac{1}{\sqrt{2 π n α (1 - α)}} e^{nH (α)}, (0 < α < 1)

, and further simplification has

\begin{matrix} E [Z_{ω}^{(2)}] = E [Z] \cdot \sqrt{\frac{4 s \cdot (1 - \frac{ω}{k - 1})}{k \cdot (1 - ω)}} \cdot \frac{[1 + {(\frac{1}{3})}^{ω n}]}{[1 + {(\frac{1}{3})}^{n}]} \\ \cdot exp [nH (ω) - m (k - 1) H (\frac{ω}{k - 1}) + ω m ln (k - 1)] \\ = E [Z] \cdot f (ω) \cdot exp [n φ_{3} (ω)] \cdot \frac{[1 + {(\frac{1}{3})}^{ω n}]}{[1 + {(\frac{1}{3})}^{n}]} \end{matrix}

Among them, function

f (ω) = \sqrt{\frac{4 s (1 - \frac{ω}{k - 1})}{k (1 - ω)}}

, and

\begin{matrix} φ_{3} (ω) = H (ω) - \frac{4 s}{k} (k - 1) H (\frac{ω}{k - 1}) + \frac{4 s}{k} ω ln (k - 1) \\ = - ω ln ω - (1 - ω) ln (1 - ω) + \frac{4 s}{k} ω ln ω \\ + \frac{4 s}{k} (k - 1 - ω) ln (1 - \frac{ω}{k - 1}) . \end{matrix}

E [Z^{2}] = \sum_{j = 0}^{n} E [Z_{j / n}^{(2)}] = E [Z_{0}^{(2)}] + \sum_{j = 1}^{n} E [Z_{j / n}^{(2)}]

, and substitute j/n with ω_j, when j = 0, ω_j = 0, it corresponds to the set of assignment pairs Q₀ = P₀ = {(T, T) : |T - T|=0}. The set of formulas satisfied by assignment pairs on this set of assignments is exactly the set of formulas satisfied by single assignment. Therefore,

E [Z_{0}^{(2)}] = E [Z]

. Then we have

\begin{matrix} E [Z^{2}] = E [Z] + \sum_{j = 1}^{n} E [Z_{ω_{j}}^{(2)}] \\ = E [Z] \cdot (1 + \sum_{j = 1}^{n} f (ω_{j}) exp [n φ_{3} (ω_{j})] \cdot \frac{[1 + {(\frac{1}{3})}^{ω n}]}{[1 + {(\frac{1}{3})}^{n}]} \\ = E [Z]^{2} \cdot \frac{exp [- n (φ_{1} (s)]}{\sqrt{2 π (1 - \frac{1}{k}) \frac{4 s}{k}} \cdot [1 + {(\frac{1}{3})}^{n}]} \\ \cdot [1 + \frac{\sum_{j = 1}^{n} f (ω_{j})}{[1 + {(\frac{1}{3})}^{n}]} \cdot (\begin{matrix} exp [n (φ_{3} (ω_{j})] + \\ exp {n \cdot [(φ_{3} (ω_{j}) + ω_{j} ln \frac{1}{3}]} \end{matrix})] \end{matrix}

}

\begin{matrix} = E [Z]^{2} \cdot \frac{exp [- n (φ_{1} (s)]}{\sqrt{2 π (1 - \frac{1}{k}) \frac{4 s}{k}} \cdot [1 + {(\frac{1}{3})}^{n}]} \\ \cdot [1 + \frac{n \cdot \int_{0}^{1} f (ω) \cdot (\begin{matrix} exp [n \cdot φ_{3} (ω_{j})] + \\ exp {n \cdot [(φ_{3} (ω_{j}) + ω_{j} ln \frac{1}{3}]} \end{matrix}) d ω}{[1 + {(\frac{1}{3})}^{n}]}] . \end{matrix}

}Set

ψ (ω) = φ_{3} (ω) + ω ln \frac{1}{3}

, we get ψ^′′ (ω) = φ₃^′′ (ω). Among them,

\begin{matrix} {φ_{3}}^{'} (ω) = ln (1 - ω) + \frac{4 s}{k} ln ω - ln ω - \frac{4 s}{k} ln (1 - \frac{ω}{k - 1}), \\ {φ_{3}}^{″} (ω) = (\frac{4 s}{k} - 1) \frac{1}{ω} + \frac{4 s}{k (k - 1 - ω)} - \frac{1}{1 - ω} . \end{matrix}

When k = 4, get s^*= 1.048, when k = 6, get s^*= 1.490, the image of function φ₃ (ω) is shown in Fig. 2. It can be proved that when k≥3 and s < s^*, φ₃″ (ω) <0, the function φ₃ (ω) is smooth, and in the interval ω ∈ [0, 1] has unique maximum point. Set the maximum points of function φ₃ (ω) and function ψ (ω) to be ω_{φ
₃
max} and ω_ψmax, respectively.

Fig. 2

Image of function φ₃ (ω).

By using the Laplace method [12] to asymptotically estimate an integral to approximate the second moment. If there exists unique maximum value ω_max ∈ [0, 1] of the function φ (ω), and φ^′′ (ω) <0 for 0 < ω_max < 1, then

\begin{matrix} E [Z (n)^{2}] = \sum_{ω = 0, k / n, 2 k / n, \dots} E [Z_{ω}^{(2)}] \\ \sim \frac{1}{k} \sqrt{\frac{n}{2 π}} \int_{0}^{1} f (ω) exp [n φ (x)] d ω \\ \sim \frac{1}{k} \frac{f (ω_{\max})}{\sqrt{- φ^{″} (} ω_{\max})} exp [n φ (ω_{\max})] . \end{matrix}

(5)

It is obtained that when n→ ∞,

\sqrt{\frac{n}{2 π}} \int_{0}^{1} f (ω) exp [n φ (x)] d ω \sim \frac{f (ω_{\max}) exp [n φ (ω_{\max})]}{\sqrt{- φ^{″} (ω_{\max})}} .

\begin{matrix} E [Z^{2}] = E [Z]^{2} \cdot \frac{exp [- n (φ_{1} (s)]}{\sqrt{2 π (1 - \frac{1}{k}) \frac{4 s}{k}} \cdot [1 + {(\frac{1}{3})}^{n}]} \\ + E [Z]^{2} \cdot \frac{n \cdot exp [- n (φ_{1} (s)]}{\sqrt{2 π (1 - \frac{1}{k}) \frac{4 s}{k}} \cdot {[1 + {(\frac{1}{3})}^{n}]}^{2}} \\ \cdot [\sqrt{\frac{2 π}{n}} \cdot \frac{f (ω_{φ_{3} \max})}{\sqrt{- {φ_{3}}^{″} (ω_{φ_{3} \max})}} exp [n φ_{3} (ω_{φ_{3} \max}) \\ + \sqrt{\frac{2 π}{n}} \cdot \frac{f (ω_{ψ \max})}{\sqrt{- ψ^{″} (ω_{ψ \max})}} exp [n ψ (ω_{ψ \max})]] \\ = E [Z]^{2} \cdot \frac{exp [- n (φ_{1} (s)]}{\sqrt{2 π (1 - \frac{1}{k}) \frac{4 s}{k}} \cdot [1 + {(\frac{1}{3})}^{n}]} + E [Z]^{2} \\ \cdot \frac{\sqrt{n}}{{[1 + {(\frac{1}{3})}^{n}]}^{2}} \cdot [\frac{f_{1} (ω_{φ_{3} \max}) exp [n φ_{3} (ω_{φ_{3} \max}) - n φ_{1} (s)]}{\sqrt{- {φ_{3}}^{″} (ω_{φ_{3} \max})}} \\ + \frac{f_{1} (ω_{ψ \max})}{\sqrt{- ψ^{″} (ω_{ψ \max})}} {(\frac{1}{3})}^{n ω_{ψ \max}} exp [n φ_{3} (ω_{ψ \max}) - n φ_{1} (s)]] . \end{matrix}

}Among them,

\begin{matrix} f_{1} (ω) = f (ω) \cdot {[(1 - \frac{1}{k}) \frac{4 s}{k}]}^{- \frac{1}{2}} \cdot \sqrt{\frac{1}{[- {φ_{3}}^{″} (ω)]}} \\ = \sqrt{\frac{(k - 1 - ω) \cdot k}{{(k - 1)}^{2} (1 - ω)}} \cdot \sqrt{\frac{1}{[- {φ_{3}}^{″} (ω)]}} . \end{matrix}

Due to

lim_{n \to \infty} [1 + {(\frac{1}{3})}^{n}] = 1

and

lim_{n \to \infty, 0 < ω < 1} {(\frac{1}{3})}^{n ω_{ψ \max}} = 0

, we have

\begin{matrix} E [Z^{2}] \approx E [Z]^{2} \cdot {[2 π (1 - \frac{1}{k}) \cdot \frac{4 s}{k}]}^{- \frac{1}{2}} \cdot exp [- n (φ_{1} (s)] \\ + E [Z]^{2} \sqrt{n} f_{1} (ω_{φ_{3} \max}) \cdot exp [n φ_{3} (ω_{φ_{3} \max}) - n φ_{1} (s)] . \end{matrix}

Set ψ₁ (s) = φ₃ (ω_{φ
_3max}) - φ₁ (s), when 0 < ω < 1, Fig. 3 shows the image of the function ψ₁ (s) for k= 4 and k= 6. It can be verified that when k ≥ 3 and s < s^*, we get

lim_{n \to \infty} {[2 π (1 - \frac{1}{k}) \frac{4 s}{k}]}^{- \frac{1}{2}} \cdot exp [- n (φ_{1} (s)] = 0

. The function ψ₁ (s) is smooth and has unique maximum point on the interval (0, 1). Thus, when s < s^*, n→ ∞, we have E [Z²] = E [Z] ² · [1 + o (1)]. So, we can get

\underset{n \to \infty}{Pr} [Z = 0] = 0

\underset{n \to \infty}{Pr} [Z > 0] = 1

. From Chebyshev inequality and the second moment method, when s < s^*, the random regular exact (3s + s, k)-SAT instance is satisfied with high probability.

Fig. 3

Image of function ψ₁ (s).

4.2.2 Proof and analysis by the small subgraph conditioning method

When there is strong correlation between events that are satisfied by a pair of assignments, this results in variance D[Z] that is constant multiple of the expectation E²[Z]. However, in special case, the variance is shown to be much smaller by small subgraph conditioning method, counting the number of small cycles of fixed length in the formula. Therefore, when s < s*, using the small subgraph conditioning method to proof that the random regular exact (3s + s, k)-SAT instance can be satisfied with high probability is more precise than proof by the second moment method. Let X_i denote the number of perfect matches corresponding to factor graphs with cycle length 2i, and the small subgraph conditioning method mainly calculates the correlation between X_i and Z and their high moment. Denote by (x) _r the descending factor, and (x) _r = x (x - 1) ⋯ (x - r + 1).According to Wormald [10], the random variable X_i obeys the Poisson distribution with parameter λ_i approximately independently. By the nature of the Poisson distribution, E [X_i] = λ_i, and the approximate expected value λ_i is calculated by estimating E [X_i]. Under the condition that the nodes are not repeated, an ordered sequence of nodes is formed by alternately selecting from the set of variable nodes and the set of clause nodes in the factor graph, respectively. Each sequence of nodes forms a cycle, and there are (n) _i (m) _i such sequences of nodes. Since such selection is related to the starting point and direction, there are 2i kinds of node sequences corresponding to the same cycle, so that the total number of node sequences of different cycles formed by alternating variables and clauses is (n) _i (m) _i/2i. Each variable is selected twice, so there are 3s (3s - 1)+3s · s+s (s - 1) choices from each row of the matrix R ( V ^*). Similarly, each clause C is selected twice, so there are k(k-1) choices from each row of the position matrix F ^*. Thus, for a given sequence of cycle nodes there are [4s (13s/4 -1)] ⁱ · [k (k - 1)] ⁱ perfect matches. After the above matching, the number of complete permutations corresponding to the remaining empty positions of the position matrix is (km - 2i) !. Therefore, the mathematical expectation of the random variable X_i is

\begin{matrix} E [X_{i}] = \frac{{(n)}_{i} {(m)}_{i}}{2 i} \cdot \frac{{(C_{4 s}^{3 s})}^{n} \cdot {[4 s (\frac{13}{4} s - 1)]}^{i}}{{(C_{4 s}^{3 s})}^{n} \cdot (mk)!} \\ \cdot [k (k - 1)]^{i} \cdot (km - 2 i) \sim \frac{{(\frac{13}{4} s - 1)}^{i} \cdot {(k - 1)}^{i}}{2 i} = λ_{i} . \end{matrix}

Let ZX_i be the number of perfect matches corresponding to factor graphs with cycle length 2i and exact satisfying solution, the analytical method of E [X_i] is useful in estimating E[ZX_i]. Let T be an exact satisfied solution, in the form of an n variable set. Let C be a cycle of length 2i, formally consisting of an i variable set C_v and an i clauses set C_c. Consider t = |T ∩ C_v| to classify the set of triples (T, C_v, C_c) such that at most one of the two neighboring variables of a clause on a cycle C occurs in the solution T, and thus we have 0≤ t ≤ ⌊ i/2 ⌋. Let N_i,t denote the number of all even pairs (T, C) of solutions T and cycles C satisfying the condition t = |T ∩ C_v|, e.g., N_6,0 = 1, N_6,1 = 6, N_6,2 = 9, and N_6,3 = 2, with N_i,⌊i/2⌋ = 2 in general. By the relationship and restriction t = |T ∩ C_v| between the exact solutions T and the cycles C, t variables in the sequence of cycle nodes are selected from T, and i-t variables are complemented by the remaining elements of the T. Considering that such selections are related to the starting point and the direction, it should be divided by a 2i factor, thus leaving [(n) _t (n - t) _i-t (m) _i]/2i possibilities. And there are [4s (13s/4 -1)] ⁱ · [k (k - 1)] ⁱ perfect matches for given sequence of cycle nodes.In the above process 2t clauses in cycle C have been satisfied, so there are m-2t remaining clauses waiting to be satisfied, and there are n-2t mismatched exact solutions satisfying these clauses.Since the m-i clauses outside the cycle C have k positions, the i-2t clauses in the cycle C that have not yet been satisfied have k-2 positions, thus there are (m - 2t) ! k^m-i (k - 2) ^i-2t matches. The number of perfect matches corresponding to the empty positions remaining after passing the matching is [(k - 1) m - 2 (i - t)] !. There are

(C_{4 s - 1}^{3 s - 1})^{n} + (C_{4 s - 1}^{s - 1})^{n}

possibilities for the realization R ( V ^*) that contains the satisfiable solution T. So, the mathematical expectation of ZX_i is obtained as

\begin{matrix} E [Z X_{i}] = 2^{n} \cdot \sum_{t = 0}^{⌊ i / 2 ⌋} [\frac{{(n)}_{t} {(n - t)}_{i - t} {(m)}_{i}}{2 i} \cdot N_{i, t} \\ \cdot {[4 s (\frac{13}{4} s - 1)]}^{i} \cdot [k (k - 1)]^{i} \cdot [(C_{4 s - 1}^{3 s - 1})^{n} + (C_{4 s - 1}^{s - 1})^{n}] \\ \cdot \frac{(m - 2 t)! k^{m - i} {(k - 2)}^{i - 2 t} \cdot [(k - 1) m - 2 (i - t)]!}{{(C_{4 s}^{3 s})}^{n} \cdot (mk)!}] . \end{matrix}

0 \leq t \leq ⌊ \frac{i}{2} ⌋ \leq ⌊ \frac{n}{2} ⌋

, and when k ≥ 3, we have

0 < \frac{n}{k} \leq \frac{n}{3}

. To facilitate the simplification of the calculation to do some approximations, have n→ ∞, (n - t) _i-t ∼ (n - n/k) _i-t ∼ n^i-t · [(k - 1) ^i-t/kⁱ]. Taking E[Z] into, and (m) _i ∼ mⁱ, m !/(m - 2t) ! ∼ m^2t, we further simplify to obtain:

\begin{matrix} \frac{E [Z X_{i}]}{E [Z]} = \frac{1}{m! k^{m} \cdot (mk - m)!} \cdot \sum_{t = 0}^{⌊ i / 2 ⌋} {\frac{{(n)}_{t} {(n - t)}_{i - t} {(m)}_{i}}{2 i} \\ \cdot N_{i, t} \cdot k^{m - i} (k - 2)^{i - 2 t} [(k - 1) m - 2 (i - t)]! \\ \cdot {[4 s (\frac{13}{4} s - 1)]}^{i} {[k (k - 1)]}^{i} \cdot (m - 2 t)!} \\ \sim \frac{1}{2 i} {(\frac{13}{4} s - 1)}^{i} {(k - 2)}^{i} \sum_{t = 0}^{⌊ i / 2 ⌋} N_{i, t} {(\frac{\sqrt{k - 1}}{k - 2})}^{2 t} \\ = μ_{i} = λ_{i} (1 + δ_{i}) . \end{matrix}

where

δ_{i} = {(\frac{k - 2}{k - 1})}^{i} \sum_{t = 0}^{⌊ i / 2 ⌋} N_{i, t} {(\frac{\sqrt{k - 1}}{k - 2})}^{2 t} - 1

.Evaluate this sum using the generate function

\begin{matrix} h (z), h (z) = \sum_{t = 0}^{⌊ i / 2 ⌋} N_{i, t} \cdot z^{2 t} \\ = tr {(\begin{matrix} 0 & z \\ z & 1 \end{matrix})}^{i} = {(\frac{1 + \sqrt{1 + 4 z^{2}}}{2})}^{i} + {(\frac{1 - \sqrt{1 + 4 z^{2}}}{2})}^{i} . \end{matrix}

Thus,

δ_{i} = {(\frac{k - 2}{k - 1})}^{i} h (\frac{\sqrt{k - 1}}{k - 2}) - 1 = {(- \frac{1}{k - 1})}^{i} > - 1

.Set

c = \sum_{p = 1}^{j} m_{i}

, according to the principle of the small graph conditioning method, for any non-negative integer series m₁, m₂, ⋯ , m_j, get

\begin{matrix} \frac{E [Z \prod_{i = 1}^{j} {[X_{i}]}_{m_{i}}]}{E [Z]} = \sum_{t_{1} = 0}^{⌊ i_{1} / 2 ⌋} \sum_{t_{2} = 0}^{⌊ i_{2} / 2 ⌋} \dots \sum_{t_{c} = 0}^{⌊ i_{c} / 2 ⌋} [\prod_{p = 1}^{c} \frac{N_{i_{p}, t_{p}}}{2 i_{p}} \\ \cdot {(n)}_{\sum_{p} t_{p}} {(n - \sum_{p} t_{p})}_{\sum_{p} i_{p} - t_{p}} \\ \cdot {(m)}_{\sum_{p} i_{p}} [4 s (\frac{13}{4} s - 1)]^{\sum_{p} i_{p}} \\ \cdot [k (k - 1)]^{\sum_{p} i_{p}} \cdot (m - 2 \sum_{p} t_{p})! \\ \cdot k^{m - \sum_{p} i_{p}} (k - 2)^{\sum_{p} (i_{p} - 2 t_{p})} \\ \cdot \frac{[(k - 1) m - 2 \sum_{p} (i_{p} - t_{p})]!}{m! k^{m} \cdot (mk - m)!}] . \\ \sim \prod_{p = 1}^{c} \frac{1}{2 i_{p}} {(\frac{13}{4} s - 1)}^{i_{p}} {(\frac{k - 2}{k - 1})}^{i_{p}} \sum_{t_{p} = 0}^{⌊ i_{p} / 2 ⌋} N_{i_{p}, t_{p}} {(\frac{\sqrt{k - 1}}{k - 2})}^{2 t_{p}} \\ = \prod_{p = 1}^{c} μ_{i_{p}} = \prod_{i = 1}^{j} μ_{i}^{m_{i}} . \end{matrix}

Then,

\begin{matrix} \sum_{i = 1}^{\infty} λ^{i} {δ_{i}}^{2} = \sum_{i = 1}^{\infty} \\ \frac{1}{2 i} {[\frac{13 s - 4}{4 (k - 1)}]}^{i} = \frac{1}{2} ln \frac{4 (k - 1)}{13 s - 4 k} < \infty, \end{matrix}

and

\frac{E [Z^{2}]}{E^{2} [Z]} \sim exp (\sum_{i = 1}^{\infty} λ^{i} {δ_{i}}^{2})

.By the small subgraph conditioning method, we obtain

\underset{n \to \infty}{Pr} [Z > 0] = 1 - o (1)

. i.e., when s < s^*, the random regular exact (3s + s, k)-SAT instance can be satisfied with high probability. Lemma 2 is proved.

5 Numerical experiments and analysis

In order to verify the theoretical results, take n = 10, two data sets with k = 4 and k = 6 are selected for the experiments. According to Theorem 1, when k = 4, s*=1.048, when k = 6, s*=1.490. The experimental environment is configured as computer with Intel(R) Core (TM) i5-8265U CPU and 8GB RAM. The phase transition of the random regular exact (3s + s, k)-SAT problem is shown in Fig. 4, and each data point consists of the statistics of 100 random F_3s+s,k formulas generated by the random regular exact (3s + s, k)-SAT instance model. Among them, the horizontal coordinate is the phase transition control parameter s and the vertical coordinate is the statistical probability Pr that the random F_3s+s,k formula can be satisfied.

Fig. 4

Phase transition of the random regular exact (3s + s, k)-SAT problem (k = 4 or k = 6, n = 10).

The results of the experiment are shown in Fig. 4, where the value of k is 4 in Fig. 4(a) and 6 in Fig. 4(b). Observing the phase transition phenomenon in Fig. 4, we can see from Fig. 4(a) that the phase transition phenomenon occurs about 1.05< s<1.3, and Fig. 4(b) that the phase transition phenomenon occurs about 1.2< s<1.5, the experimental results are almost in accordance with the theoretical proofs. Due to the approximation of the assigned values of m and s in the experiment and the small problem scale, the obtained experimental results have some errors with the theoretical results. However, as the problem scale increases, the experimental errors caused by this approximation will be reduced, and the experimental results will gradually become more accurate. At the same time, since the experiment uses the exhaustive assignment method (2 ⁿ assignments in total) to determine whether the random F_3s+s,k formula is exact and satisfiable, the solution time increases exponentially as the problem scale becomes larger.

6 Conclusions

In this paper, we analyze the phase transition phenomenon of the random regular exact (3s + s, k)-SAT problem, and give the phase transition point s* of the random regular exact (3s + s, k)-SAT problem in which each variable occurs 4s times, of which the positive occurrences are 3s times and the negative occurrences are s times. The upper and lower bounds of the satisfiability phase transition threshold are proved by using the first moment method, the second moment method, and the small subgraph conditioning method, in which the small subgraph conditioning method provides a new feasibility of proving the lower bound of the phase transition threshold. Subsequently, numerical experiments are carried out to verify the experimental results, and the results show that the experimental results are consistent with the theoretical ones. Since the phase transition threshold for the regular (d,k)-SAT problem is not available at present, and the random regular exact (3s + s, k)-SAT problem is a special case of this problem, it provides reference value for the study of satisfiable phase transitions of the regular (d,k)-SAT problem. Future work is to further use these phase transition analysis methods to give the phase transition for the random regular exact (s + d,k)-SAT problem with positive variable occurrences s times and negative variable occurrences d times, as well as other similarly intractable problems.

Footnotes

Acknowledgments

This work was supported by the National Natural Science Foundation of China (62062001) and the Ningxia Youth Top Talent Project (2021).

References

Achlioptas

Chtcherba

Istrate

Moore

, The phase transition in 1-in-k SAT and NAE 3-SAT[J], ACM Symposium on Discrete Algorithms (2001), 721–722.

Achlioptas

Moore

, Two moments suffice to cross a sharp threshold[J], SIAM Journal of Computing36 (2006), 740–762.

Coja-Oglan

Panagiotou

, Catching the k-NAESAT threshold[C]// Proceedings of the fortyfourth annual ACM symposium on Theory of computing, ACM (2012), 899–908.

Ding

Sly

Sun

, Satisfiability threshold for random regular NAE-SAT, Communications in Mathematical Physics[J]341(2) (2016), 435–489.

Knysh

Smelyanskiy

V.N.

Morris

R.D.

, Approximating satisfiability transition by suppressing fluctuations[J], arXiv preprint cond-mat/0403416, 2004

Kalapala

Moore

, The phase transition in exact cover[J], Chicago Journal of Theoretical Computer Science (2008), 5.

Moore

, The phase transition in random regular exact cover[J], Ann. Inst.3(3) (2016), 349–362

Panagiotou

Pasch

, Satisfiability thresholds for regular occupation problems[J], arXiv preprint arXiv:1811.00991, 2018.

Wang

X.F.

Zhou

J.C.

, et al. Phase transition of in random balance regular exact (2s,k)-SAT problem [J], Journal of Huazhong University of Science and Technology (Natural Science Edition)50(02) (2022), 105–111.

10.

Wormald

N.C.

, Models of random regular graphs[J], London Mathematical Society Lecture Note Series (1999), 239–298.

11.

Z.F.

D.Y.

, NP-completeness of d-regular (k,s)-SAT problem, Ruan Jian Xue Bao/Journal of Software31(4) (2020), 1113–1123.

12.

Achlioptas

Moore

, Random k-SAT: Two moments suffice to cross a sharp threshold[J], SIAM Journal on Computing36(3) (2006), 740–762.

13.

Marino

Parisi

Ricci-Tersenghi

, The backtracking survey propagation algorithm for solving random K-SAT problems[J], Nature Communications7(1) (2016), 12996

14.

Rassmann

, On the number of solutions in random graph k-colouring[J], Combinatorics, Probability and Computing28(1) (2019), 130–158.

15.

Coja-Oghlan

Efthymiou

Jaafari

, et al. Charting the replica symmetric phase[J], Communications in Mathematical Physics359 (2018), 603–698.

16.

Robinson

R.W.

Wormald

N.C.

, Almost all cubic graphs are Hamiltonian[J], Random Structures & Algorithms3(2) (1992), 117–125.

17.

Wang

Y.P.

D.Y.

, Satisfiability threshold of strictly d-regular random (3,2s)-SAT problem for fixed s, Ruan Jian Xue Bao/Journal of Software32(9) (2021), 2629–2641.

18.

Nam

Sly

Sohn

, One-step replica symmetry breaking of random regular NAE-SAT[C]//2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS), IEEE (2022), 310–318.

19.

Nie

Wang

, , et al.The Phase Transition Analysis for the Random Regular Exact 2-(d,k)-SAT Problem[J], Symmetry, 2021, https://doi.org/10.3390/sym13071231.

20.

Mo Xiao-ling Xu Dao-yun ,Probabilistic Properties of Satisfiable Solutions on Space of Assignments for CNF Formula[J], Journal of Frontiers of Computer Science & Technology12(11) (2018), 1852–1861.