Generating hard SAT/CSP instances using expander graphs

Loading...
Thumbnail Image
Date
2008
Authors
Ansótegui Gil, Carlos JoséAnsótegui Gil, Carlos José - ORCID ID
Béjar Torres, RamónBéjar Torres, Ramón - ORCID ID
Fernàndez Camon, CésarFernàndez Camon, César - ORCID ID
Mateu Piñol, CarlesMateu Piñol, Carles - ORCID ID
Other authors
Impact
Export
Share
Journal Title
Journal ISSN
Volume Title
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.
Citation
DOI
Journal or Serie
Proceedings of the twenty-third National Conference on Artificial Intelligence, 2008, p. 1442-1443