# Scale-Free Random SAT Instances
###### Abstract  
We focus on the random generation of SAT instances that have properties similar to real-world instances. It is known that many industrial instances, even with a great number of variables, can be solved by a clever solver in a reasonable amount of time. This is not possible, in general, with classical randomly generated instances. We provide a different generation model of SAT instances, called _scale-free random SAT instances_. This is based on the use of a non-uniform probability distribution \(P(i)\sim i^{-\beta}\) to select variable \(i\), where \(\beta\) is a parameter of the model. This results in formulas where the number of occurrences \(k\) of variables follows a power-law distribution \(P(k)\sim k^{-\beta}\), where \(\delta=1+1/\beta\). This property has been observed in most real-world SAT instances. For \(\beta=0\), our model extends classical random SAT instances. We prove the existence of a SAT-UNSAT phase transition phenomenon for scale-free random 2-SAT instances with \(\beta<1/2\) when the clause/variable ratio is \(m/n=\frac{1-2\beta}{(1-\beta)^{2}}\). We also prove that scale-free random k-SAT instances are unsatisfiable with a high probability when the number of clauses exceeds \(\omega(n^{(1-\beta)k})\). The proof of this result suggests that, when \(\beta>1-1/k\), the unsatisfiability of most formulas may be due to small cores of clauses. Finally, we show how this model will allow us to generate random instances similar to industrial instances, of interest for testing purposes. os +
Footnote †: journal: _Algorithms_  
1
Footnote 1: email: [PERSON]; [PERSON], [PERSON]. ;  
[PERSON] [PERSON]; S.: E.: F.: L.: L.  
have a scale-free structure. This kind of structure has also been observed in other real-world networks like the World Wide Web, Internet, some social networks like papers co-authorship or citation, protein interaction network, etc. [PERSON] et al. [6] show that these graph representations of industrial instances exhibit very high modularity. Modularity has been shown to be correlated with the runtime of CDCL SAT solvers [7] and has been used to improve the performance of some solvers [6; 8; 9]. It is also known that eigenvector centrality is correlated with the significance of variables [10]. Defining a model that captures all the properties observed in industrial instances is a hard task. Here, we focus on the scale-free structure. We will define a model and propose a random generator for _scale-free SAT formulas_, extending our work presented in the IJCAI'09 [11] conference. This model is parametric in terms of the size \(k\) of clauses and an exponent \(\beta\). Formulas are sets of \(m\) independently sampled clauses of size \(k\) with possible repetitions. Clauses are sets of \(k\) independently sampled variables, without repetitions, where each variable \(x_{i}\) is chosen with probability \(P(x_{i})\sim i^{-\beta}\), and negated with probability \(1/2\). In this paper, we also study the SAT-UNSAT phase transition phenomena in this new model using percolation techniques of statistical mechanics. We prove that a random scale-free formula over \(n\) variables, exponent \(\beta\) and \(\mathcal{O}(n^{(1-\beta)k})\) clauses of size \(k\) are unsatisfiable with a high probability (see Theorem 5). This means that, for big enough values of \(\beta\), the number of clauses needed to make a formula unsatisfiable is sub-linear on the number of variables, contrary to the standard random SAT model. We also prove that scale-free random 2-SAT formulas with exponent \(\beta<1/2\) and a ratio of clause/variables \(m/n>\frac{1-2\beta}{(1-\beta)^{2}}\) are also unsatisfiable with high probability (see Theorem 4). This last result, together with a coincident lower bound found by [PERSON] et al. [12], allows us to conclude that scale-free random 2 SAT formulas show a SAT-UNSAT phase transition threshold. More recently, many new results related to the phase transition on scale-free random formulas have been found. [PERSON] et al.