Generating hard SAT/CSP instances using expander graphs

Thumbnail
View/Open
Issue date
2008
Author
Ansótegui Gil, Carlos José
Béjar Torres, Ramón
Fernàndez Camon, César
Mateu Piñol, Carles
Impact

Google Scholar logo  Google Scholar
Share
Export to Mendeley
Metadata
Show full item record
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.
URI
http://hdl.handle.net/10459.1/46644
Is part of
Proceedings of the twenty-third National Conference on Artificial Intelligence, 2008, p. 1442-1443
Collections