From high girth graphs to hard instances

Abstract

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 . 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. © 2008 Springer-Verlag Berlin Heidelberg.