On different models for generating random sat problems

Abstract

In the last decade a lot of effort has been invested into both theoretical and experimental analysis of SAT phase transition. However, a deep theoretical understanding of this phenomenon is still lacking. Besides, many of experimental results are based on some assumptions that are not supported theoretically. In this paper we introduce the notion of SAT-equivalence and we prove that some restrictions often used in SAT experiments don't make an impact on location of a crossover point. We consider several fixed and random clause length SAT models and relations between them. We also discuss one new SAT model and report on a detected phase transition for it.