Abstract
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.
Research partially supported by the projects TIN2007-68005-C04-{01,03,04} and TIN2006-15662-C02-02 funded by the MEC.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Ansótegui, C., Bonet, M.L., Levy, J.: Towards industrial-like random SAT instances. In: Proc. of the 21st Int. Joint Conf. on Artificial Intelligence, IJCAI 2009 (2009)
Albert, R., Jeong, H., Barabási, A.-L.: The diameter of the www. Nature 401, 130–131 (1999)
Albert, R., Jeong, H., Barabási, A.-L.: Error and attack tolerance of complex networks. Nature 406, 378–482 (2000)
Barabási, A.-L., Albert, R.: Emergence of scaling in random networks. Science 286, 509–512 (1999)
Boufkhad, Y., Dubois, O., Interian, Y., Selman, B.: Regular random k-sat: Properties of balanced formulas. J. of Automated Reasoning 35, 181–200 (2005)
Clauset, A., Shalizi, C.R., Newman, M.E.J.: Power-law distributions in empirical data. Arxiv, 0706.1062 (2007)
Erdós, P., Rényi, A.: On random graphs. Publicationes Mathematicae 6, 290–297 (1959)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Gomes, C.P., Fernández, C., Selman, B., Bessière, C.: Statistical regimes across constrainedness regions. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 32–46. Springer, Heidelberg (2004)
Gent, I.P., Hoos, H.H., Prosser, P., Walsh, T.: Morphing: Combining structure and randomness. In: Proc. of the 16th Nat. Conf. on Artificial Intelligence, AAAI 1999, pp. 654–660 (1999)
Jeroslow, R.G., Wang, J.: Solving propositional satisfiability problems. Annals of Mathematics and Artificial Intelligence 1, 167–187 (1990)
Kautz, H.A., Selman, B.: Ten challenges redux: Recent progress in propositional reasoning and search. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 1–18. Springer, Heidelberg (2003)
Kautz, H.A., Selman, B.: The state of SAT. Discrete Applied Mathematics 155(12), 1514–1524 (2007)
Li, C.M., Anbulagan: Look-ahead versus look-back for satisfiability problems. In: Smolka, G. (ed.) CP 1997. LNCS, vol. 1330, pp. 341–355. Springer, Heidelberg (1997)
Li, L., Alderson, D., Doyle, J.C., Willinger, W.: Towards a theory of scale-free graphs: Definition, properties, and implications. Internet Mathematics 2(4), 431–523 (2005)
Selman, B.: Satisfiability testing: Recent developments and challenge problems. In: Proc. of the 15th Annual IEEE Symposium on Logic in Computer Science, LICS 2000, p. 178 (2000)
Selman, B., Kautz, H.A., McAllester, D.A.: Ten challenges in propositional reasoning and search. In: Proc. of the 15th Int. Joint Conf. on Artificial Intelligence, IJCAI 1997, pp. 50–54 (1997)
Walsh, T.: Search on high degree graphs. In: Proc. of the 17th Int. Joint Conf. on Artificial Intelligence, IJCAI 2001, pp. 266–274 (2001)
Watts, D.J., Strogatz, S.H.: Collective dynamics of ’small-world’ networks. Nature 393, 440–442 (1998)
Xu, L., Hutter, F., Hoos, H., Leyton-Brown, K.: SATzilla: Portfolio-based algorithm selection for SAT. J. of Artificial Intelligence Research 32, 565–606 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ansótegui, C., Bonet, M.L., Levy, J. (2009). On the Structure of Industrial SAT Instances. In: Gent, I.P. (eds) Principles and Practice of Constraint Programming - CP 2009. CP 2009. Lecture Notes in Computer Science, vol 5732. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04244-7_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-04244-7_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04243-0
Online ISBN: 978-3-642-04244-7
eBook Packages: Computer ScienceComputer Science (R0)