ML Anthology

Generating Hard SAT/CSP Instances Using Expander Graphs

Carlos Ansótegui, Ramón Béjar, Cèsar Fernández, Carles Mateu
AAAI 2008 pp. 1442-1443
/aaai/2008/ansotegui2008aaai-generating/

Abstract

In this paper we provide a new method to generate hard k-SAT instances. We incrementally construct a high girth bipartite incidence graph of the k-SAT instance. Having high girth assures high expansion for the graph, and high expansion implies high resolution width. We have extended this approach to generate hard n-ary CSP instances and we have also adapted this idea to increase the expansion of the system of linear equations used to generate XORSAT instances, being able to produce harder satisfiable instances than former generators.

PDF AAAI Semantic Scholar

Cite

Text

Ansótegui et al. "Generating Hard SAT/CSP Instances Using Expander Graphs." AAAI Conference on Artificial Intelligence, 2008.

Markdown

[Ansótegui et al. "Generating Hard SAT/CSP Instances Using Expander Graphs." AAAI Conference on Artificial Intelligence, 2008.](https://mlanthology.org/aaai/2008/ansotegui2008aaai-generating/)

BibTeX

@inproceedings{ansotegui2008aaai-generating,
  title     = {{Generating Hard SAT/CSP Instances Using Expander Graphs}},
  author    = {Ansótegui, Carlos and Béjar, Ramón and Fernández, Cèsar and Mateu, Carles},
  booktitle = {AAAI Conference on Artificial Intelligence},
  year      = {2008},
  pages     = {1442-1443},
  url       = {https://mlanthology.org/aaai/2008/ansotegui2008aaai-generating/}
}