Títol | On the Structure of Industrial SAT Instances |

Publication Type | Conference Paper |

Year of Publication | 2009 |

Authors | Ansótegui C [1], Bonet MLuisa [2], Levy J [3] |

Editor | Gent I.P [4] |

Conference Name | Proc. of the 15th Int. Conf. on Principles and Practice of Constraint Programming, CP'09 |

Volume | 5732 |

Editor | Springer |

Conference Location | Lisbon, Portugal |

Paginació | 127-141 |

Resum | During this decade, it has been observed that many real-world graphs, like the web and some social and metabolic networks, have a scale-free structure. These graphs are characterized by a big variability in the arity of nodes, that seems to follow a power-law distribution. This came as a big surprise to researchers steeped in the tradition of classical random networks. SAT instances can also be seen as (bi-partite) graphs. In this paper we study many families of industrial SAT instances used in SAT competitions, and show that most of them also present this scale-free structure. On the contrary, random SAT instances, viewed as graphs, are closer to the classical random graph model, where arity of nodes follows a Poisson distribution with small variability. This would explain their distinct nature. We also analyze what happens when we instantiate a fraction of the variables, at random or using some heuristics, and how the scale-free structure is modified by these instantiations. Finally, we study how the structure is modified during the execution of a SAT solver, concluding that the scale-free structure is preserved. |