Hard SAT and CSP instances with Expander Graphs.
Carlos Ansótegui, Ramón Béjar, César C. Fernández, Carles Mateu · 2008
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. The experimental investigation conducted on complete and incomplete solvers confirms that the expansion of the graph is indeed a key factor in order to obtain harder instances than other approaches. 1