Generating hard satisfiability problems

被引:156
作者
Selman, B [1 ]
Mitchell, DG [1 ]
Levesque, HJ [1 ]
机构
[1] UNIV TORONTO, DEPT COMP SCI, TORONTO, ON M5S 1A4, CANADA
基金
加拿大自然科学与工程研究理事会;
关键词
satisfiability; random problems; phase transitions; 4.3; benchmarks; empirical study;
D O I
10.1016/0004-3702(95)00045-3
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
We report results from large-scale experiments in satisfiability testing. As has been observed by others, testing the satisfiability of random formulas often appears surprisingly easy. Here we show that by using the right distribution of instances, and appropriate parameter values, it is possible to generate random formulas that are hard, that is, for which satisfiability testing is quite difficult. Our results provide a benchmark for the evaluation of satisfiability testing procedures.
引用
收藏
页码:17 / 29
页数:13
相关论文
共 38 条
[1]  
[Anonymous], 1979, Computers and Intractablity: A Guide to the Theoryof NP-Completeness
[2]  
BECKMAN RJ, 1983, TECHNOMETRICS, V25, P119, DOI 10.2307/1268541
[3]  
Bollobas B, 1985, RANDOM GRAPHS
[4]  
BURO M, 1992, 110 U PAD DEP MATH I
[5]  
CHAO M, 1990, INFORM SCI, V51, P23
[6]  
CHEESEMAN P, 1991, P IJCAI 91, P163
[7]  
Chvatal V., 1992, Proceedings 33rd Annual Symposium on Foundations of Computer Science (Cat. No.92CH3188-0), P620, DOI 10.1109/SFCS.1992.267789
[8]   MANY HARD EXAMPLES FOR RESOLUTION [J].
CHVATAL, V ;
SZEMEREDI, E .
JOURNAL OF THE ACM, 1988, 35 (04) :759-768
[9]  
Cook S.A., 1971, P 3 ANN ACM S THEOR, P151, DOI DOI 10.1145/800157.805047
[10]  
CRAWFORD JM, 1993, P AAAI 93 WASH DC