ML Anthology

Locality in Random SAT Instances

Jesús Giráldez-Cru, Jordi Levy
IJCAI 2017 pp. 638-644
doi:10.24963/IJCAI.2017/89 /ijcai/2017/giraldezcru2017ijcai-locality/

Abstract

Despite the success of CDCL SAT solvers solving industrial problems, there are still many open questions to explain such success. In this context, the generation of random SAT instances having computational properties more similar to real-world problems becomes crucial. Such generators are possibly the best tool to analyze families of instances and solvers behaviors on them. In this paper, we present a random SAT instances generator based on the notion of locality. We show that this is a decisive dimension of attractiveness among the variables of a formula, and how CDCL SAT solvers take advantage of it. To the best of our knowledge, this is the first random SAT model that generates both scale-free structure and community structure at once.

PDF IJCAI Semantic Scholar

Cite

Text

Giráldez-Cru and Levy. "Locality in Random SAT Instances." International Joint Conference on Artificial Intelligence, 2017. doi:10.24963/IJCAI.2017/89

Markdown

[Giráldez-Cru and Levy. "Locality in Random SAT Instances." International Joint Conference on Artificial Intelligence, 2017.](https://mlanthology.org/ijcai/2017/giraldezcru2017ijcai-locality/) doi:10.24963/IJCAI.2017/89

BibTeX

@inproceedings{giraldezcru2017ijcai-locality,
  title     = {{Locality in Random SAT Instances}},
  author    = {Giráldez-Cru, Jesús and Levy, Jordi},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2017},
  pages     = {638-644},
  doi       = {10.24963/IJCAI.2017/89},
  url       = {https://mlanthology.org/ijcai/2017/giraldezcru2017ijcai-locality/}
}