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
2W(w2/n)2^{\Omega(w^2/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.