{'fraction_non_alphanumeric': 0.034346614368290666, 'fraction_numerical': 0.00944467382328654, 'mean_word_length': 4.264637956799348, 'pattern_counts': {'":': 0, '<': 19, '<?xml version=': 0, '>': 11, 'https://': 0, 'lorem ipsum': 0, 'www.': 1, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 5, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Many Hard Examples in Exact Phase Transitions with Application to Generating Hard Satisfiable Instances

This paper first analyzes the resolution complexity of two random CSP models (i.e. Model RB/RD) for which we can establish the existence of phase transitions and identify the threshold points exactly. By encoding CSPs into CNF formulas, it is proved that almost all instances of Model RB/RD have no tree-like resolution proofs of less than exponential size. Thus, we not only introduce new families of CNF formulas hard for resolution, which is a central task of Proof-Complexity theory, but also propose models with both many hard instances and exact phase transitions. Then, the implications of such models are addressed. It is shown both theoretically and experimentally that an application of Model RB/RD might be in the generation of hard satisfiable instances, which is not only of practical importance but also related to some open problems in cryptography such as generating one-way functions. Subsequently, a further theoretical support for the generation method is shown by establishing exponential lower bounds on the complexity of solving random satisfiable and forced satisfiable instances of RB/RD near the threshold. Finally, conclusions are presented, as well as a detailed comparison of Model RB/RD with the Hamiltonian cycle problem and random 3-SAT, which, respectively, exhibit three different kinds of phase transition behavior in NP-complete problems.


Introduction
Over the past ten years, the study of phase transition phenomena has been one of the most exciting areas in computer science and artificial intelligence. Numerous empirical studies suggest that for many NP-complete problems, as a parameter is varied, there is a sharp transition from 1 to 0 at a threshold point with respect to the probability of a random instance being soluble. More interestingly, the hardest instances to solve are concentrated in the sharp transition region. As well known, finding ways to generate hard instances for a problem is important both for understanding the complexity of the problem and for providing challenging benchmarks for experimental evaluation of algorithms [12]. So the finding of phase transition phenomena in computer science not only gives a new method to generate hard instances but also provides useful insights into the study of computational complexity from a new perspective.
Although tremendous progress has been made in the study of phase transitions, there is still some lack of research about the connections between the threshold phenomena and the generation of hard instances, especially from a theoretical point of view. For example, some problems can be used to generate hard instances but the existence of phase transitions in such problems has not been proved. One such an example is the well-studied random 3-SAT. A theoretical result by we not only introduce new families of CNF formulas hard for resolution, which is a central task of Proof-Complexity theory, but also propose models with both many hard instances and exact phase transitions. More importantly, it will be shown that an application of RB/RD might be in the generation of hard satisfiable instances, which is not only of significance for experimental studies, but also of interest to the theoretical computer science community. Finally, exponential lower bounds will be established for random satisfiable and forced satisfiable instances of RB/RD near the threshold.

Model RB and Model RD
A Constraint Satisfaction Problem, or CSP for short, consists of a set of variables, a set of possible values for each variable (its domain) and a set of constraints defining the allowed tuples of values for the variables (a well-studied special case of it is SAT). The CSP is a fundamental problem in Artificial Intelligence, with a distinguished history and many applications, such as in knowledge representation, scheduling and pattern recognition. To compare the efficiency of different CSP algorithms, some standard random CSP models have been widely used experimentally to generate benchmark instances in the past decade. For the most widely used CSP model (i.e. standard Model B), Achlioptas et al. [2] proved that except for a small range of values of the constraint tightness, almost all instances generated are unsatisfiable as the number of variables approaches infinity. This result, as shown in [19], implies that most previous experimental results about random CSPs are asymptotically uninteresting. However, it should be noted that Achlioptas et al.'s result holds under the condition of fixed domain size and so is applicable only when the number of variables is overwhelmingly larger than the domain size. But in fact, it can be observed that the domain size, compared to the number of variables, is not very small in most experimental CSP studies. This, in turn, explains why there is a big gap between Achlioptas et al.'s theoretical result and the experimental findings about the phase transition behavior in random CSPs. Motivated by the observation above, and to overcome the trivial asymptotic insolubility of the previous random CSP models, Xu and Li [33] proposed an alternative CSP model as follows.
Model RB: First, we select with repetition m = rn ln n random constraints. Each random constraint is formed by selecting without repetition k of n variables, where k ≥ 2 is an integer. Next, for each constraint we uniformly select without repetition q = p · d k incompatible tuples of values, i.e., each constraint contains exactly (1 − p) · d k allowed tuples of values, where d = n α is the domain size of each variable and α > 0 is a constant.
Note that the way of generating random instances for Model RB is almost the same as that for Model B. However, like the N-queens problem and Latin square, the domain size of Model RB is not fixed but polynomial in the number of variables. It is proved that Model RB not only avoids the trivial asymptotic behavior but also has exact phase transitions. More precisely, the following theorems hold for Model RB, where Pr(Sat) denotes the probability that a random CSP instance generated by Model RB is satisfiable.
As shown in [33], many instances generated following Model B in previous experiments can also be viewed as instances of Model RB, and more importantly, the experimental results for these instances agree well with the theoretical predictions for Model RB. Therefore, in this sense, we can say that Model B can still be used experimentally to produce benchmark instances. However, to guarantee an asymptotic phase transition behavior and to generate random hard instances, a natural and convenient way is to vary the values of CSP parameters under the framework of Model RB. Note that another standard CSP Model, i.e. Model D, is almost the same as Model B except that for every constraint, each tuple of values is selected to be incompatible with probability p. Similarly, we can make a revision to Model D and then get a new Model as follows.
Model RD: First, we select with repetition m = rn ln n random constraints. Each random constraint is formed by selecting without repetition k of n variables, where k ≥ 2 is an integer. Next, for each constraint, from d k possible tuples of values, each tuple is selected to be incompatible with probability p, where d = n α is the domain size of each variable and α > 0 is a constant.
Along the same line as in the proof for Model RB [33], we can easily prove that exact phase transitions also exist for Mode RD. More precisely, Theorem 1 and Theorem 2 hold for Model RD too. In fact, it is exactly because the differences between Model RB and Model RD are very small that many properties hold for both of them and the proof techniques are also almost the same. So in this paper, we will discuss both models, denoted by Model RB/RD.
Recently, there has been a growing theoretical interest in random CSPs, especially with respect to their phase transition behaviors [13,16,17,27,31,35] and resolution complexity [18,26,28]. To discuss the resolution complexity of CSPs, we first need to encode a CSP instance into a CNF formula. In this paper we will adopt the encoding method used in [24]. For convenience, we give the outline of this method here. For each CSP variable u, we introduce d propositional variables, called domain variables, to represent assignments of values to u. There are three sets of clauses needed in the encoding, i.e. the domain clauses asserting that each variable must be assigned a value from its domain, the conflict clauses excluding assignments violating constraints and clauses asserting that each variable is assigned at most one value from its domain.

Resolution Lower Bounds for Model RB/RD
In this section, we will analyze the resolution complexity of unsatisfiability proofs for Model RB/RD and get the following result.
Theorem 3 Let P be a random CSP instance generated following Model RB/RD. Then, almost surely, P has no tree-like resolutions of length less than 2 Ω(n) .
When we say that a property holds almost surely it means that this property holds with probability tending to 1 as the number of variables approaches infinity.
The core of the proof for Theorem 3 is to show that almost surely there exists a clause with large width in every refutation. The width of a clause C, denoted by w(C), is the number of variables appearing in it. The width of a set of clauses is the maximal width of a clause in the set. The width of deriving a clause C from the formula F, denoted by w(F ⊢ C) is defined as the minimum of the widths of all derivations of C from F. So, the width of refutations for F can be denoted by w(F ⊢ 0). Ben-Sasson and Wigderson [8] gave the following theorem on size-width relations and proposed a general strategy for proving width lower bounds for CNF formulas.
Theorem 4 (Ben-Sasson and Wigderson [8]) Let F be a CNF formula and S T (F ) be the minimal size of a tree-like refutation. Then we have By extending Ben-Sasson and Wigderson's strategy, Mitchell [26] proved exponential resolution lower bounds for some random CSPs of fixed domain size. In what follows, to obtain lower bounds on width for RB/RD, we will basically use the same strategy as in [26], but adapt it to handle random CSPs with growing domains. First, we prove the following local sparse property for RB/RD. Lemma 1 Let P be a random CSP instance generated by Model RB/RD. There is constant c > 0 such that almost surely every sub-problem of P with size s ≤ cn has at most b = βs ln n constraints, where β = α 6k ln 1 1−p .
Proof: As mentioned in [27], this is a standard type of argument in random graph theory. Similarly, we consider the number of sub-problems on s variables with b = βs ln n constraints for 0 < s ≤ cn. There are n s possible choices for the variables and m b for the constraints. Given such choices, the probability that all the b constraints are in the s variables is not greater than s n kb .
So, the number of such sub-problems is at most This finishes the proof.
The following two definitions will be of use later.
Definition 1 Consider a variable u and i constraints associated with u. In these i constraints, all the variables except u have already been assigned values from their domains. We call this an i-constraint assignment tuple, denoted by T i,u .
Definition 2 Given a variable u and an i-constraint assignment tuple T i,u . We assign a value v to u from its domain. So, all the variables in the i constraints of T i,u have been assigned values. If at least one constraint in T i,u is violated by these values, then we say that the value v of u is flawed by T i,u . If all the values of u in its domain are flawed by T i,u , then we say that the variable u is flawed by T i,u , and T i,u is called a flawed i-constraint assignment tuple.
Lemma 2 Let P be a random CSP instance generated by Model RB/RD. Almost surely, there does not exist a flawed i-constraint assignment tuple T i,u in P with i ≤ 3kβ ln n.
Proof: Now consider an i-constraint assignment tuple T i,u with i ≤ 3kβ ln n. It is easy to see that the probability that T i,u is flawed increases the number of constraints i. Recall that in Model RD, for every constraint, each tuple of values is selected to be incompatible with probability p. So, given a value v of u, the probability that v is flawed by T i,u is Thus the probability that all the d = n α values of u are flawed by T i,u , i.e. the probability of T i,u being flawed is The above analysis only applies to Model RD. For Model RB, such an analysis is much more complicated, and so we leave it in the appendix. Recall that there are n variables and m = rn ln n constraints. So the number of possible choices for i-constraint assignment tuples is at most For i ≤ 3kβ ln n, when n is sufficiently large, there exists a constant c 2 > 0 such that Thus the expected number of flawed i-constraint assignment tuples with i ≤ 3kβ ln n is at most This implies that almost surely, there does not exist a variable u and an i-constraint assignment tuple T i,u with i ≤ 3kβ ln n such that u is flawed by T i,u . This is exactly what we need and so we are done.
Lemma 3 Let P be a random CSP instance generated by Model RB/RD. Almost surely, every sub-problem of P with size at most cn is satisfiable.
Proof: Here by the size of a problem we mean the number of variables in this problem. We will prove this lemma by contradiction. Assume that we have an unsatisfiable sub-problem of size at most cn. Thus we can get a minimum sized unsatisfiable sub-problem with size s ≤ cn, denoted by P 1 . From Lemma 1 we know that almost surely P 1 has at most βs ln n constraints. Thus there exists a variable u in P 1 with degree at most kβ ln n, i.e. the number of constraints in P 1 associated with u is not greater than kβ ln n. Removing u and the constraints associated with u from P 1 , we get a sub-problem P 2 . By minimality of P 1 , we know that P 2 is satisfiable, and so there exists an assignment satisfying P 2 . Suppose that the variables in P 2 have been assigned values by such an assignment. Now consider the variable u and the i constraints associated with u, where i ≤ kβ ln n. By Definition 2 this constitutes an i-constraint assignment tuple for u, denoted by T i,u . Recall that P 1 is unsatisfiable. This means that no value of u can satisfy all the i constraints. That is to say, the variable u is flawed by T i,u . Therefore, if a sub-problem of size at most cn is unsatisfiable, then, almost surely, there is a variable u and an i-constraint assignment tuple T i,u such that u is flawed by T i,u , where i ≤ kβ ln n. This is in contradiction with Lemma 2 and so finishes the proof. Now we will prove that there almost surely exist a complex clause in the refutation proofs of Model RB/RD. The complexity of a clause was defined in [26] by Mitchell, i.e. for any refutation π, the complexity of a clause C in π, denoted by µ(C), is the size of the smallest sub-problem Π such that C can be derived by resolution from φ(Π). Along the same line as in the proof of [26], we have the following lemma.
Lemma 4 Let P be a random CSP instance generated by Model RB/RD. Almost surely, every refutation π of φ(P ) has a clause C of complexity cn 2 ≤ µ(C) ≤ cn. Proof: For this proof, please refer to [26].
Lemma 5. Let C be a clause of complexity cn 2 ≤ µ(C) ≤ cn. Then, almost surely, C has at least c 6 n literals, i.e. w(C) ≥ c 6 n. Proof: We will prove this by contradiction. For a CSP instance P, its CNF encoding is denoted by φ(P ). Let C be a clause of complexity cn 2 ≤ µ(C) ≤ cn and P 1 be the smallest problem such that φ(P 1 ) |= C. Hence, the size of P 1 is at least c 2 n and at most cn. By Lemma 1, there are at most βcn ln n constraints in P 1 . So, there are at most c 3 n variables with degree greater than 3kβ ln n. Then, there are at least c 2 n − c 3 n = c 6 n variables in P 1 with degree at most 3kβ ln n. We will prove that for these variables, almost surely, there does not exist a variable such that no domain variable of it appears in C. Now assume that we have a variable u in P 1 with degree i ≤ 3kβ ln n and no domain variable of it appears in C. Removing u and the constraints associated with it from P 1 , we get a sub-problem P 2 . By minimality of P 1 , we know that φ(P 2 ) |= C. So we can find an assignment satisfying P 2 but not satisfying C. Suppose that the propositional variables in P 2 and C have been assigned values by such an assignment. Now consider the variable u and the constraints associated with it. By Definition 2, this constitutes an i-constraint assignment tuple for u, denoted by T i,u . By assumption, no domain variable of u appears in C. So, assigning any value to u will not affect the truth value of C. Recall that φ(P 1 ) |= C and C is false under the current assignment. Therefore, no value of u can satisfy φ(P 1 ), i.e. setting any value to u will violate at least one constraint associated with it. It follows that u is flawed by T i,u , i.e. there exists a flawed i-constraint assignment tuple with i ≤ 3kβ ln n. This is in contradiction with Lemma 2 and so we are done.
Combining Lemma 4 and Lemma 5, we have that, for a random CSP instance P generated by Model RB/RD, almost surely, w(φ(P ) ⊢ 0) ≥ c 6 n. Now, by use of Theorem 4, we finish the proof. One point worth mentioning is that when α ≥ 1, the initial width of clauses is greater than or equal to the number of variables. In such a case, to make Theorem 4 applicable, we only need to introduce some new variables and reduce the widths of domain clauses, which has no effect on our results.

Generating Hard Satisfiable Instances
As mentioned before, the finding of phase transitions in NP-complete problems provides a good method for generating random hard instances which are very useful in the evaluation of algorithms. In recent years, a remarkable progress in Artificial Intelligence has been the development of incomplete algorithms for various kinds of problems. To evaluate the efficiency of such incomplete algorithms, we need a source to generate only hard satisfiable instances [3]. However, since the probability of being satisfiable is about 0.5 at the threshold point where the hardest instances are concentrated, the generator based on phase transitions will usually produce a mixture of satisfiable and unsatisfiable instances. So, it is interesting to study how the phase transition phenomenon can be used to generate hard satisfiable instances. Besides practical importance, more interestingly, the problem of generating random hard satisfiable instances is related to some open problems in cryptography, e.g. computing a one-way function, generating pseudo-random numbers and private key cryptography [12,21,23].
In fact, for constraint satisfaction and Boolean satisfiability problems, there is a natural strategy to generate instances that are guaranteed to have at least one satisfying assignment. The strategy is as follows [3]: first generate a random truth assignment t, and then generate a certain number of random constraints or clauses one by one to form a random instance, where any clause or constraint violating t will be rejected. The above strategy is very simple and can be easily implemented. But unfortunately, this strategy was proved to be unsuitable for random 3-SAT because it in fact produces a biased sampling of instances with many satisfying assignments (clustered around t), and experiments also show that these instances are much easier to solve than random satisfiable instances [3]. In the following, for convenience, we will call the satisfiable instances generated using the strategy as forced satisfiable instances. Now let us look further into the problem why the strategy fails for random 3-SAT. As defined in [33,34], an assignment pair < t 1 , t 2 > is an ordered pair of two assignments t 1 and t 2 . We say that < t 1 , t 2 > satisfies a CSP if and only if both t 1 and t 2 satisfy this CSP. Suppose that the number of variables is n and the domain size is d. Then we have totally d n possible assignments, denoted by t 1 , t 2 , · · · , t d n , and d 2n possible assignment pairs. Let t i be a forced satisfying assignment. Then the expected number of solutions for forced satisfiable instances satisfying t i , denoted by E f [N ], is where Pr[< t i , t j >] denotes the probability that < t i , t j > satisfies a random instance.
Note that E f [N ] should be independent of the choice of the forced satisfying assignment t i . So we have where E[N 2 ] and E[N ] are, respectively, the second moment and the first moment of the number of solutions for instances generated randomly. For random 3-SAT, it follows from the result on satisfying assignment pairs in [34] that asymptotically, E[N 2 ] is exponentially greater than E 2 [N ]. This conclusion can also be found in [4]. Thus, the expected number of solutions for forced satisfiable instances is exponentially larger than that for random satisfiable instances, which gives a good theoretical explanation of why, for random 3-SAT, the strategy is highly biased towards generating instances with many solutions. We now consider the problem of generating satisfiable instances for Model RB/RD using the same strategy. Recall that when we established the exact phase transitions for RB/RD [33], it was proved that E[N 2 ]/E 2 [N ] is asymptotically equal to 1 below the threshold, where almost all instances are satisfiable, i.e. E[N 2 ]/E 2 [N ] ≈ 1 for r < r cr or p < p cr . So, we have that for RB/RD, the expected number of solutions for forced satisfiable instances below the threshold is asymptotically equal to that for random satisfiable instances, i.e.
In other words, the strategy has almost no effect on the number of solutions for RB/RD and thus will not lead to a biased sampling of instances with many solutions.
In addition to the analysis above, we can also study the influence of the strategy on the distribution of solutions with respect to the forced satisfying assignment. Based on the definition of similarity number in [33], we first define a distance on the assignments as d f (t 1 , t 2 ) = 1− S f ( t 1 , t 2 )/n, where t 1 , t 2 are two assignments, n is the total number of variables and S f ( t 1 , t 2 ) is equal to the number of variables at which the two assignments take the identical values. It is easy to see that and E[X] respectively denote, for forced satisfiable instances and random satisfiable instances, the expected number of solutions with a fixed distance d t from the forced satisfying assignment. By an analysis similar to that in [33] (pp.96-97), we have Indeed, it can be shown, from the results in [33] (pp.97-98), that E f [X], for r < r cr or p < p cr , will be asymptotically maximized when d t takes the largest possible value, i.e. d t = 1. For random satisfiable instances of RB/RD, we have It is straightforward to see that the same pattern holds for this case, i.e. E[X] will be asymptotically maximized when d t = 1. So, intuitively speaking, for RB/RD, given an assignment t, for both forced satisfiable instances satisfying t and random satisfiable instances, most solutions distribute in a place far from t. This further indicates that the strategy has little effect on the distribution of solutions for RB/RD, and so it will not be be biased towards generating instances with many solutions around the forced satisfying assignment. For random 3-SAT, similarly, we have and where f 1 (n) and f 2 (n) are two polynomial functions. It follows from the results in [34] that as r (the ratio of clauses to variables) approaches 4.25, E f [X] and E[X] will be asymptotically maximized when d t ≈ 0.24 and d t = 0.5 respectively. This means, in contrast to RB/RD, that compared with random satisfiable instances, most solutions of forced satisfiable instances distribute in a place much closer to the forced satisfying assignment when r is near the threshold. Note that the number and the distribution of solutions are the two most important factors determining the cost of solving satisfiable instances. So, we can expect, from the above analysis, that for RB/RD, the hardness of solving forced satisfiable instances should be similar to that of solving random satisfiable instances. More interestingly, it therefore seems that we can, based on the hardness of RB/RD, propose a new method to generate hard satisfiable instances, i.e. generating forced satisfiable instances of RB/RD with a large number of variables near the threshold identified exactly by Theorem 1 or Theorem 2. Experimental results have further confirmed this idea 2 . It is shown, in one experiment for RB with k = 2, n = 30, d = 15 and m = 250, that the mean time of solving forced satisfiable instances near the threshold is only slightly smaller (11 percent) than that of solving random satisfiable instances with the same parameters 3 . More importantly, experiments for RB also indicate that the hardness of solving forced satisfiable instances grows exponentially with the number of variables 4 near the threshold, and we can, in fact, generate forced satisfiable instances appearing to be very hard to solve (for both complete and incomplete algorithms) even when the number of variables is only moderately large (e.g. k = 2, n = 59, α = 0.8 and r = 0.8/ ln 4 3 with constraint tightness p = p cr = 0.25 computed by Theorem 2, or equivalently expressed as k = 2, n = 59, d = 26 and m = 669 with the same tightness 5 ) 6 . Although there have been some other ways to generate hard satisfiable instances empirically, e.g. the quasigroup method [3], we think that the simple and natural method presented in this paper, based on models (i.e. Model RB/RD) with exact phase transitions and many hard instances, should be well worth further investigation. 2 We thank Dr. Christophe Lecoutre and Liu Yang very much for performing the experiments. 3 As specified by the conditions of Theorem 2, to make exact phase transitions hold, the values of α and r should not be small. So, we should choose dense CSPs with a large domain. 4 According to the definitions of RB/RD and Theorems 1 and 2, the parameters α, r and p should be fixed when n increases. The values of the threshold points can also be obtained from these two theorems. 5 If non-integer values occur in the computation of d and m from n, α and r, then we round them to the nearest integers. 6 Benchmarks of Model RB (in both SAT and CSP format) are available at www.nlsde.buaa.edu.cn/˜kexu/ benchmarks/benchmarks.htm.

Exponential Lower Bounds for Satisfiable Instances of Model RB/RD
For random CSP instances of RB/RD, we know from Theorems 1 and 2 that almost surely, they are satisfiable below the threshold and unsatisfiable above the threshold. For satisfiable instances, there are no resolution proofs, or, if any, the resolution proofs are of infinite length. Therefore, the exponential resolution lower bounds, established in Theorem 4, are of interest only for instances above the threshold. Also, in many other cases, exponential lower bounds have been shown only for unsatisfiable instances, and it seems quite difficult to derive such lower bounds for satisfiable instances. A recent progress in this direction, made by Achlioptas et. al. [5], is that exponential lower bounds have been established for certain natural DPLL algorithms on some provably satisfiable instances of random k-SAT for k ≥ 4. In this section, we will analyze the complexity of solving RB/RD below the threshold and obtain the following results.
Theorem 5 Given a random CSP instance of RB/RD with r cr − ǫ r < r ≤ r cr or are two positive constants, we uniformly select without repetition c 12 n variables, and assign each of these variables a value from its domain at random. If such values does not violate any constraint, then, almost surely, the residual formula is unsatisfiable and has no tree-like resolution proofs of less than exponential size.
Proof: Let E[X] denote the expected number of assignments satisfying the residual formula. By assumption, the partial assignment to the c 12 n variables does not violate any constraint. Then For r cr − ǫ r < r ≤ r cr , we have By Markov's inequality, we know that the residual formula will be almost surely unsatisfiable. For the phase transition with respect to p, the proof can be done similarly. Now we prove that for the residual formula, any sub-problem of size at most cn is almost surely satisfiable. Based on the proofs of Lemmas 2 and 3, we only need to show that for any sub-problem with size 1 ≤ s ≤ cn containing unassigned variables, there almost surely exists an unassigned variable with degree at most 3kβ ln n. Thus, it is sufficient to prove that for any sub-problem with size 1 + c 12 n ≤ s ≤ cn + c 12 n containing the c 12 n assigned variables, there almost surely exists an unassigned variable with degree at most 3kβ ln n. For such a sub-problem, the probability that an unassigned variable has a degree at least 3kβ ln n is not greater than as required. Now for the residual formula, Lemmas 3 and 4 follow immediately. Recall that in Lemma 5, we prove that there are at least c 6 n variables in P 1 with degree at most 3kβ ln n. For the residual formula where c 12 n variables have been assigned values, there are at least c 12 n variables in P 1 with degree at most 3kβ ln n. Similarly, we can prove that almost surely, there is a clause with at least c 12 n literals for the residual formula. By Theorem 4, we finish the proof. Note that the constant c can be chosen to monotonically decrease with r or p. Here we can, therefore, take the value of c as that for r = r cr or p = p cr and try to make it as small as possible (in order to guarantee that ǫ r and ǫ p are two positive constants).
Generally speaking, different search algorithms use different strategies to search for solutions. Rather than focusing on some specific algorithms, we relate the hardness of solving satisfiable instances to that of solving unsatisfiable sub-problems, because if it takes a long time to solve the sub-problems generated in the search process, then the original problem can not be solved quickly [24]. Theorem 5 indicates that for satisfiable instances of RB/RD below and close to the threshold, if a resolution-based algorithm can not detect any contradiction in the early stage of a search branch, then the algorithm will, very likely, generate a large-sized unsatisfiable sub-problem. As a result, it will, then, almost surely take exponential time to explore large subtrees to prove the unsatisfiability of the sub-problem. Indeed, there are exponentially many large-sized unsatisfiable sub-problems. More precisely, it can be computed that the total number of residual formulas with = exp (Ω(n ln n)) .
So, intuitively speaking, when solving satisfiable instances of RB/RD near the threshold, backtrackstyle algorithms will very easily fall into pitfalls with no solutions, and then, worse still, take a long time to escape from these pitfalls. To our best knowledge, this is the first result on the complexity of solving satisfiable instances near the proved threshold, which can help us to gain a better understanding of the extreme hardness of instances in the phase transition region.
For random forced satisfiable instances near the proved threshold, similarly, we have the following result.
Theorem 6 Given a random forced satisfiable instance of RB/RD with r cr − ǫ r < r ≤ r cr or r are two positive constants, we uniformly select without repetition c 12 n variables, and assign each of these variables a value from its domain at random. If such values does not violate any constraint, then, almost surely, the residual formula is unsatisfiable and has no tree-like resolution proofs of less than exponential size.
Proof: Due to limited space, we only give the proof for the case of the phase transition with respect to r in Model RD with 1 k < α < 1. The other cases can be handled similarly. Assume that we have two assignments t 1 and t 2 and the similarity number [33] between t 1 and t 2 is S f (< t 1 , t 2 >) = S. Let P be a random instance of Model RD. Based on the analysis in [33] (p.96), the probability that both t 1 and t 2 satisfy P is Now we suppose that t 0 is a random forced satisfying assignment and t is an assignment with S f (< t 0 , t >) = S. Let P sat be a random forced satisfiable formula of Model RD with t 0 as the forced satisfying assignment. Then the probability that t satisfies P sat is Pr[t satisfies P sat ] = Pr[t 0 and t satisfy P ] Pr[t 0 satisfy P ] where g(s) = k(k−1) 2 (s k − s k−1 ). Now, for the random forced satisfiable formula P sat , we uniformly select without repetition c 12 n variables and then assign each of these variables a value from its domain at random. By the standard Chernoff bound, it is easy to show that the similarity number between the forced satisfying assignment t 0 and the random partial assignment to the c 12 n variables is almost surely less than c 6 n 1−α . For the residual formula, we have totally d n− c 12 n possible assignments. Let t ′ be an assignment to the n − c 12 n variables of the residual formula with S f (< t 0 , t ′ >) = S ′ . By assumption, the partial assignment to the c 12 n variables does not violate any constraint. Thus, almost surely, the probability that t ′ satisfies the residual formula is at most Let E[X] be the expected number of assignments satisfying the residual formula. Similar to the asymptotic analysis in [33] (p.99), for r cr − ǫ r < r ≤ r cr , we have Note that the forced satisfying assignment has no effect on the structure of constraint graphs. The rest of the proof is identical to that in Theorem 5 and so we are done. The above theorem, as far as we know, is the first complexity result of resolution-based algorithms on forced satisfiable instances, which further provides, from another aspect, a strong theoretical support for the method of generating hard satisfiable instances proposed in the last section.

Conclusions
In this paper, by encoding CSPs into CNF formulas, we proved exponential lower bounds for tree-like resolution proofs of two random CSP models with exact phase transitions, i.e. Model RB/RD. This result suggests that we not only introduce new families of CNF formulas hard for resolution, which is a central task of Proof-Complexity theory, but also propose models with both many hard instances and exact phase transitions. More interestingly, it is shown both theoretically and experimentally that an application of RB/RD might be in the generation of hard satisfiable instances, which is further supported by the exponential lower bounds established in Section 6.
As mentioned before, there are some other NP-complete problems with proved exact phase transitions, e.g. Hamiltonian cycle problem and random 2+p-SAT (0 < p ≤ 0.4). However, it has been shown either experimentally or theoretically that the instances produced by these problems are generally easy to solve. So one would naturally ask what the main difference between these "easy" NP-complete problems and RB/RD is. It seems that for these "easy" NP-complete problems with exact phase transitions, they usually have some kind of local property which can be used to design polynomial time algorithms working with high probability, and the exact phase transitions are, in fact, obtained by probabilistic analysis of such algorithms. So, it appears that if a problem has exact phase transitions obtained by algorithm analysis, then it also means that the problem is not hard to solve. For RB/RD, the situation is, however, completely different. More specifically, the exact phase transitions of RB/RD are obtained, not by analysis of algorithms, but by use of the first and the second moment methods which say nothing about the local property of the problem and are, therefore, unlikely to be useful for designing more efficient algorithms. Thus, it seems that RB/RD, unlike the "easy" NP-complete problems, can indeed provide a reliable source to generate random benchmark instances, as many and as hard as we need.
Note that more recently, Frieze and Wormald [15] studied random k-SAT for moderately growing k, i.e. k = k(n) satisfies k − log 2 n → ∞ where n is the number of variables. For this model, they established similarly, by use of the first and the second moment methods, that there exists a satisfiability threshold at which the number of clauses is m = 2 k n ln 2. From Beame et al's earlier work on the complexity of unsatisfiability proofs for random k-SAT formulas [6,7], we know that the size of resolution refutations for this model is exponential with high probability. So, the variant of random k-SAT studied by Frieze and Wormald is also a model with both proved phase transitions and many hard instances.
To gain a better understanding of Model RB/RD, we now make a comparison of them with the well-studied random 3-SAT of similar proof complexity. First, we think that the exact phase transitions should be one advantage of RB/RD, which can help us to locate the hardest instances more precisely and conveniently when implementing large-scale computational experiments. As for the theoretical aspect, it seems that RB/RD, intrinsically, are much mathematically easier to analyze than random 3-SAT, such as in the derivation of thresholds. From a personal perspective, we think that such mathematical tractability should be another advantage of RB/RD, making it possible to obtain some interesting results which do not hold or can not be easily obtained for random 3-SAT, just as shown on forced satisfiable instances.
In summary, the Hamiltonian cycle problem, random 3-SAT and Model RB/RD, respectively, exhibit three different kinds of phase transition behavior in NP-complete problems. Compared with the former two that have been extensively explored in the past decade, the third one (i.e. the phase transition behavior with both exact thresholds and many hard instances), due to various reasons, has not received much attention so far. From this point, the main contribution of this paper, we can say, is not in the mathematical techniques used, nor the concrete models studied (although such models are useful for CSP research in their own right), but pointing out an interesting behavior for study. Finally, we hope that more investigations, either experimental or theoretical, will be carried out on this behavior, and we also believe that such studies will lead to deep insights and new discoveries in this active area of research (i.e. on phase transitions and computational complexity). The remaining part of the proof is identical to that of Lemma 2 for Model RD, and so we are done.