The purpose of this project is to identify the properties of industrial SAT instances that makes them tractable. Two properties have been observed in industrial SAT instances. The first property is that the degrees of the variables in an industrial SAT instance follow a scale-free distribution, where the degree of a variable of a SAT formula is the number of clauses thatcontain this variable. The second property is that the variables of an industrial SAT instance tend to cluster in communities, that is sets of variables tend to appear in the same clauses. The standard model for generating random SAT instances does not produce formulae that have these two properties. Random SAT models have been proposed that encompass either scale-free degree distribution or a high clustering coefficient, but none of these models seems provides insight on why SAT solversperform so well on real world instances. Inspired by recent models designed to approximate real world networks, we propose to study a new model for generating random SAT instances that potentially addresses both of these properties. Our model uses geometry to address the community structure and a measure of importance, in the form of variable weights, to address the power-law degree distribution.
