Random SAT Instances à la Carte
Carlos Ansótegui, Marı́a Luisa Bonet, Jordi Levy · 2008
Many studies focus on the generation of hard SAT instances. The hard-ness is usually measured by the time it takes SAT solvers to solve the instances. In this preliminary study, we focus on the generation of instances that have compu-tational properties that are more similar to real-world instances. In particular, in-stances with the same degree of difficulty, measured in terms of the tree-like res-olution space complexity. It is known that industrial instances, even with a great number of variables, can be solved by a clever solver in a reasonable amount of time. One of the reasons may be their relatively small space complexity, compared with randomly generated instances. We provide two generation methods of k-SAT instances, called geometrical and the geo-regular, as generalizations of the uniform and regular k-CNF generators. Both are based on the use of a geometric probability distribution to select vari-ables. We study the phase transition phenomena and the hardness of the generated instances as a function of the number of variables and the base of the geometric distribution. We prove that, with these two parameters we can adjust the difficulty of the problems in the phase transition point. We conjecture that this will allow us to generate random instances more similar to industrial instances, of interest for testing purposes.