|
Title:
|
From High Girth Graphs to Hard Instances
|
|
Author:
|
Ansótegui Gil, Carlos José; Béjar Torres, Ramón; Fernàndez Camon, César; Mateu Piñol, Carles
|
|
Notes:
|
In this paper we provide a new method to generate hard
k-SAT instances. Basically, we construct the bipartite incidence graph of
a k-SAT instance where the left side represents the clauses and the right
side represents the literals of our Boolean formula. Then, the clauses are
filled by incrementally connecting both sides while keeping the girth of
the graph as high as possible. That assures that the expansion of the
graph is also high. It has been shown that high expansion implies high
resolution width w. The resolution width characterizes the hardness of
an instance F of n variables since if every resolution refutation of F has
width w then every resolution refutation requires size 2Ω(w2/n)
. We have
extended this approach to generate hard n-ary CSP instances. Finally,
we have also adapted this idea to increase the expansion of the system
of linear equations used to generate XOR-SAT instances, being able to
produce harder satisfiable instances than former generators.
Research partially supported by projects TIN2006-15662-C02-02, TIN2007-68005-C04-02 and José Castillejo 2007 program funded by the Ministerio de Educación y Ciencia |
|
Rights:
|
(c) Springer-Verlag Berlin Heidelberg, 2008
info:eu-repo/semantics/restrictedAccess |
|
Document type:
|
article
publishedVersion |
|
Published by:
|
Springer Verlag
|
|
Share:
|
|
