K. Xu and W. Li. Many Hard Examples in Exact Phase Transitions. Theoretical Computer Science, 355(2006):291-302. Earlier version appeared as CoRR Report cs.CC/0302001 in Feb. 2003.
Abstract: This paper analyzes the resolution complexity of two random CSP models (i.e. Model RB/RD) for which we can establish the existence of phase transitions and identify the threshold points exactly. By encoding CSPs into CNF formulas, it is proved that almost all instances of Model RB/RD have no tree-like resolution proofs of less than exponential size. Thus, we not only introduce new families of CSPs and CNF formulas hard to solve, which can be useful in the experimental evaluation of CSP and SAT algorithms, but also propose models with both many hard instances and exact phase transitions. Finally, conclusions are presented, as well as a detailed comparison of Model RB/RD with the Hamiltonian cycle problem and random 3-SAT, which, respectively, exhibit three different kinds of phase transition behavior in NP-complete problems.
Keywords: SAT, CSP, CNF formulas, NP-complete problems, constraint satisfaction, phase transition, sharp thresholds, resolution complexity, computational complexity.
Exact Phase Transitions in Random Constraint Satisfaction Problems, JAIR, 2000.
A Simple Model to Generate Hard Satisfiable Instances, Proc. IJCAI-2005.
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
Back to Ke Xu's homepage.