available, as it can be supported by a number of experiments. 

Conjecture 1. For every integer k ≥ 3*, given the number of variables n and a target language L that* is a subset of DNNF, there exists a positive real number rc such that For each pair (r1,r2), if r1<r2<rc, then 1 2 ( ( )) ( ( )) nr nr EX P EX P Lk Lk < . 

For each pair (r1,r2), if rc<r1<r2<rp, then 1 2 ( ( )) ( ( )) nr nr EX P EX P Lk Lk > . 

where rp is the soluble-to-insoluble phase transition point of k-SAT. The conjecture describes that when r ranges from 0 to rp, the sizes of compilation results increase until r reaches rc and then decrease. 

## Experimental Results On Random K**-Sat**

In this section, we analyze phase transitions in random k-SAT compilation using OBDD and d-DNNF as target languages. The compilers we choose for the target languages are the state-of-the-art compilers, where d-DNNF compiler was made by Darwiche (It is available at: http://reasoning.cs.ucla.edu/c2d/) and the OBDD compiler based on CUDD package was developed by Narodytska and Walsh for their work of constraint and variable ordering heuristics for compiling configuration problems [14]. According to the knowledge compilation map, all the languages in the map are subsets of NNFs. Because NNFs can be described by directed acyclic graphs, we can represent OBDD and d-DNNF using directed acyclic graphs, of which the sizes are measured by the number of its nodes and edges. However, it can be observed that the number of nodes and the number of edges change in the same manner when we compile k-SAT instances ranging r from 0 to rp, and the peak points are also in the same position. Since we only care about the changing manner and the points of maximum sizes, with the fact discussed above, we count the number of nodes as the size of d-DNNF (OBDD), though the number of edges is usually used to evaluate the size of d-DNNF. In the following experiments, we generate SAT instances using random k-SAT model and compile them into OBDDs and d-DNNFs respectively. For each combination of k and n, we vary r from 0 to the corresponding rp (relative to k). To obtain more exact results, we produce 1000 instances for each r, and calculate average nodes of the compilation results. Because of runtime limitations, we only take k ranging from 2 to 6 and n ranging from 20 to 60. 

## Experiments On Random 3-Sat

The first set of experimental results concerns random 3-SAT instances. Fig. 1 depicts the easy-hard-easy pattern when compiling instances into d-DNNFs. We also locate the phase transition point in random 3-SAT compilations. There are 3 curves in Fig. 1, each of which corresponding to a different n ranging from 40 to 60. The peak points of those curves are with same value of the ratio r, which is 1.8. This point is far from the soluble-to-insoluble transition point where r is about 4.3. Fig. 2 describes the experimental results of OBDDs. Three groups of instances have been generated for the OBDD experiments too. But there is a small difference in the generation parameters with n varying from 20 to 40, since the OBDD compiler needs more time to finish the experiments. Note that the curves of OBDDs have the same behaviors as curves in Fig. 1. Especially, the peak sizes occur at the same point where r is 1.8. However, as we mentioned in pervious section, the critical point of PIs is 