Satisfiability and Algorithms for Non-Uniform Random k-SAT

The Random Satisfiability problem has received much attention in the literature. In this paper we tackle a somewhat nonstandard type of Random Satisfiability, the one where instances are not chosen uniformly from a certain class of instances, but rather from a certain nontrivial distribution. More precisely, we use so-called Configuration Model, in which we start with a distribution of degrees (the number of occurrences) of a variable, sample the degree of each variable and then generate a random instance with the prescribed degrees. It has been proposed previously that by properly selecting the starting distribution (to be, say, power law or lognorm) one can approximate at least some aspect of `industrial' instances of SAT.Here we suggest an algorithm that solves such problems for a wide range of degree distributions and obtain necessary and sufficient conditions for the satisfiability of such formulas.