K. Xu and W. Li. Many Hard Examples in Exact Phase Transitions with Application to Generating Hard Satisfiable Instances. CoRR Report cs.CC/0302001, 2003. Last updated on Nov. 12, 2003.
Abstract: This paper first 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 CNF formulas hard for resolution, which is a central task of Proof-Complexity theory, but also propose models with both many hard instances and exact phase transitions. Then, the implications of such models are addressed. It is shown both theoretically and experimentally that an application of Model RB/RD might be in the generation of hard satisfiable instances, which is not only of practical importance but also related to some open problems in cryptography such as generating one-way functions. Subsequently, a further theoretical support for the generation method is shown by establishing exponential lower bounds on the complexity of solving random satisfiable and forced satisfiable instances of RB/RD near the threshold. 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, hard satisfiable instances, satisfiable problems generation.Related Paper:
Exact Phase Transitions in Random Constraint Satisfaction Problems
A Simple Model to Generate Hard Satisfiable InstancesBenchmarks:
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)
L. Christophe, B. Frederic and H. Fred. Implicit Random CSPs. Proceedings of the 15th International IEEE Conference on Tools with Artificial Intelligence (ICTAI'03), pp.482-486, Sacramento, California, November, 2003.
Y. Gao and J. Culberson. Resolution Complexity of Random Constraint Satisfaction Problems: Another Half of the Story. Proceedings of LICS'03, Workshop on Typical Case Complexity and Phase Transitions, Ottawa, Canada, June, 2003.
L. Christophe, B. Frederic and H. Fred. Exploiting Multidirectionality in Coarse-grained Arc Consistency Algorithms. Proceedings of the 9th International Conference one Principles and Practice of Constraint Programming (CP'03), pp.480-494, LNCS-2833, Ireland, 2003.