Exact Phase Transitions in Random Constraint Satisfaction Problems


K. Xu and W. Li. Exact Phase Transitions in Random Constraint Satisfaction Problems. Journal of Artificial Intelligence Research, 12(2000):93-103.

Abstract: The Constraint Satisfaction Problem (CSP) is a generalization of the satisfiability problem (SAT) and has a rich history in AI.  In recent years, random constraint satisfaction problems have received more and more attention from both an experimental and a theoretical perspective. In this paper we propose a new type of random CSP model, called Model RB, which is a revision to the standard Model B. It is proved that phase transitions from a region where almost all problems are satisfiable to a region where almost all problems are unsatisfiable do exist for Model RB as the number of variables approaches infinity. Moreover, the critical values at which the phase transitions occur are also known exactly. By relating the hardness of Model RB to Model B, it is shown that there exist a lot of hard instances in Model RB.
Keywords: phase transition, constraint satisfaction problems, NP-complete problems, CSP model, threshold phenomena, sharp thresholds, computational complexity, hard instances.

Remark: Model RB provides a framework for generating asymptotically hard random constraint satisfaction problems (Click the first benchmark link below for more information and to see an illustrative example). Such a framework is very useful for evaluating the asymptotic behavior of CSP algorithms. Another point worth attention is that unlike some other NP-complete problems with hard instances in the phase transition region, e.g. 3-SAT, the existence of phase transitions in Model RB has been established and the phase transition points are also known exactly. Also different from some other NP-complete problems with the exact phase transition, e.g. 1-in-k SAT and Hamiltonian Cycle problem, the exact phase transition points of Model RB are obtained not by analysis of algorithms but by asymptotic analysis of the first and the second moment of the number of solutions. It appears that if a problem has the exact phase transition obtained by analysis of algorithms, then it also means that the problem is easy to solve or easy on average. From a perspective of computational complexity, such problems are not so interesting for study as those with many hard instances. Recently, we have obtained some theoretical results about the hardness of Model RB. By encoding CSPs into CNF formulas we proved that almost all instances of Model RB have no tree-like resolution proofs of less than exponential size. This means that we not only introduce new families of CNF formulas hard for resolution, which is a central task of Proof-Complexity theory, but also associate the generation of such hard formulas with the well-studied phase transition phenomenon theoretically. More interestingly, it was shown that unlike random 3-SAT, for Model RB, the method of generating formulas in the phase transition region that are forced to have a planted satisfying assignment will not cause a biased sampling towards formulas with many satisfying assignments around this planted assignment. This result indicates that by generating forced satisfiable constraint satisfaction problems of Model RB in the phase transition region and by encoding such CSPs into CNF formulas, we might get a new method to generate random hard satisfiable CSP and SAT instances. Following this method, we generated some forced satisfiable CSP and SAT benchmarks (Click the first benchmark link below for more information which includes a summary of the results for the SAT benchmarks used in SAT'04 competition). Anyone interested can have a test on these benchmarks (in both SAT and CSP format) or do further studies (either experimental or theoretical) on Model RB.

Related Papers:
Many Hard Examples in Exact Phase Transitions with Application to Generating Hard Satisfiable Instances.
A Simple Model to Generate Hard Satisfiable Instances, Proc. IJCAI-2005.

Benchmarks:
Forced Satisfiable CSP and SAT benchmarks of Model RB
Benchmarks with Hidden Optimum Solutions for Independent Set, Vertex Cover, Clique and Vertex Coloring
Pseudo-Boolean (0-1 Integer Programming) Benchmarks with Hidden Optimum Solutions

An incomplete list of publications citing the above paper (If you know any other paper that should be listed here, please contact me)

Back to Ke Xu's homepage.