A Simple Model to Generate Hard Satisfiable Instances

TL;DR

This paper demonstrates that the RB and RD models for random CSP instances are easy to generate, exhibit a clear phase transition, and can produce forced satisfiable instances with hardness comparable to unforced ones, supported by theoretical analysis and experiments.

Contribution

It introduces a simple model for generating hard satisfiable CSP instances with a known phase transition and comparable difficulty to unforced instances, supported by formal analysis and experiments.

Findings

Models exhibit a clear phase transition point.

Forced satisfiable instances have similar hardness to unforced ones.

Instances can be generated easily with guaranteed complexity.

Abstract

In this paper, we try to further demonstrate that the models of random CSP instances proposed by [Xu and Li, 2000; 2003] are of theoretical and practical interest. Indeed, these models, called RB and RD, present several nice features. First, it is quite easy to generate random instances of any arity since no particular structure has to be integrated, or property enforced, in such instances. Then, the existence of an asymptotic phase transition can be guaranteed while applying a limited restriction on domain size and on constraint tightness. In that case, a threshold point can be precisely located and all instances have the guarantee to be hard at the threshold, i.e., to have an exponential tree-resolution complexity. Next, a formal analysis shows that it is possible to generate forced satisfiable instances whose hardness is similar to unforced satisfiable ones. This analysis is supported by some representative results taken from an intensive experimentation that we have carried out, using complete and incomplete search methods.