Abstract:
Recent years have witnessed rapid progress both in the foun- dations of and in applying state-of-art solvers for the propo- sitional satisfiability problem (SAT). The study of sources for hard SAT instances is motivated by the need for inter- esting benchmarks for solver development and on the other hand by theoretical analysis of different proof systems. In this respect satisfiable instance families are espe- cially interesting. In contrast to unsatis iable instance families, there are few theoretical results for satisfiable formulas; for the successful DPLL method, restricted heuristics need to be considered. While real-world problems serve as best benchmark in- stances in many sense, such instances are typically very large and unavailable in abundance. More artificial empirically hard satisfiable CNF families include regular random k-SAT, encodings of quasi-group completion, XORSAT models inspired by statistical physics, and the regular XORSAT model motivated by expansion properties of random regular bipartite graphs. Experimental comparison with other available generators for notably hard satisfiable 3-CNF formulas shows that the regular XORSAT model gives extremely hard instances for state-of-the art clausal SAT solvers. In this paper we generalize the regular XORSAT model for k > 3, and investigate how this relates to the hardness of the instances. By increasing the degree of the underlying regular constraint graphs, we observe a sharp increase in problem difficulty with respect to the number of variables, motivating further analysis of regular XORSAT.