Abstract
Despite the success of modern SAT solvers on industrial instances, most of the progress relies on intensive experimental testing of improvements or new ideas. In most cases, the behavior of CDCL solvers cannot be predicted and even small changes may have a dramatic positive or negative effect. In this paper, we do not try to improve the performance of SAT solvers, but rather try to improve our understanding of their behavior. More precisely, we identify an essential structural property of industrial instances, based on the Eigenvector centrality of a graphical representation of the formula. We show how this static value, computed only once over the initial formula casts new light on the behavior of CDCL solvers.
We also advocate for a better partitionning of industrial problems. Our experiments clearly suggest deep discrepancies among the families of benchmarks used in the last SAT competitions.
This work was partially funded by the “Agence nationale de la Recherche”, reference ANR-10-BLA-0214.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Ansótegui, C., Giráldez-Cru, J., Levy, J.: The Community Structure of SAT Formulas. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 410–423. Springer, Heidelberg (2012)
Ansótegui, C., Levy, J.: On the modularity of industrial SAT instances. In: CCIA (2011)
Braunstein, A., Mézard, M., Zecchina, R.: Survey propagation: An algorithm for satisfiability. Random Structures & Algorithms 27(2), 201–226 (2005)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Communication of ACM 5(7), 394–397 (1962)
Langville, A., Meyer, C.: Google’s PageRank and Beyond: The Science of Search Engine Rankings. Princeton Unviersity Press (2006)
Shah, D., Zaman, T.: Community detection in networks: The leader-follower algorithm. arXiv:1011.0774v1 (2010)
Silva, J.M., Sakallah, K.: Grasp - a new search algorithm for satisfiability. In: ICCAD, pp. 220–227 (1996)
Walsh, T.: Search in a small world. In: IJCAI 1999: Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, pp. 1172–1177. Morgan Kaufmann Publishers Inc., San Francisco (1999)
Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In: Proceedings of IEEE/ACM International Conference on Computer Design (ICCAD), pp. 279–285 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Katsirelos, G., Simon, L. (2012). Eigenvector Centrality in Industrial SAT Instances. In: Milano, M. (eds) Principles and Practice of Constraint Programming. CP 2012. Lecture Notes in Computer Science, vol 7514. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33558-7_27
Download citation
DOI: https://doi.org/10.1007/978-3-642-33558-7_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33557-0
Online ISBN: 978-3-642-33558-7
eBook Packages: Computer ScienceComputer Science (R0)