-
摘要:
研究变元和文字出现次数受限制的规则3-SAT问题,提出了一种严格随机正则(3,
s )-SAT问题,并给出了该问题的实例产生模型--SRR模型。结合一阶矩方法和生成函数展开项系数的渐近近似技术,证明了严格随机正则(3,s )-SAT问题相变点的上界,即当变元规模N 较大且变元出现次数s >11时,严格随机正则(3,s )-SAT实例是高概率不可满足的。实验结果表明:由SRR模型所生成的随机实例中,当N >60且s >11时,所有的(3,s )-SAT实例均是不可满足的,而当N >150且s < 11时,所有的(3,s )-SAT实例均是可满足的,即严格随机正则(3,s )-SAT实例的相变点位于s =11处,且在s =11处(子句变元比为11/3)的严格随机正则(3,s )-SAT实例,比在相变点(子句变元比)4.267处同规模的均匀随机3-SAT实例更难求解,因此,SRR模型可以很方便地在s =11处构造难解的随机3-SAT实例。-
关键词:
- 严格正则(3, s)-SAT问题 /
- 相变性质 /
- 计算复杂性 /
- 难解实例产生模型 /
- 生成函数
Abstract:We study the restricted occurrence times for variables and literatures in 3-SAT problem. In particular, we propose a strictly regular random (3,
s )-SAT problem and its instances generating model-SRR model. Using the first moment method and the asymptotic approximation technique to the expansion coefficient in generating function, we derive an upper bound of the phase transformation point for the strictly regular random (3,s )-SAT problem, i.e., when the variable sizeN is large enough and the variable occurrence timess is greater than 11, the strictly regular random (3,s )-SAT instances are unsatisfied with high probability. Furthermore, for the random instances generated by model SRR with different variable size, our experimental results show that whenN is greater than 60 ands is greater than 11, all the (3,s )-SAT instances are unsatisfied, and whenN is greater than 150 ands is less than 11, all the (3,s )-SAT instances are satisfied. Thus, the phase transition point of the strictly regular random (3,s )-SAT instances is located ats =11(i.e., the ratio of clauses to variables is 11/3). We also observe that the strictly regular random (3,s )-SAT instances at the locations =11 are much more difficult to solve than the uniform random 3-SAT instances around its phase transition point, which is about 4.267 (the ratio of clauses to variables). Therefore, it is quite easy to generate hard random 3-SAT instances by our SRR model at the location wheres is 11. -
表 1 各变元规模下,不同s时每100个严格随机正则(3, s)-SAT实例中可满足的实例总数
Table 1. Total number of satisfied instances for each s in every 100 strictly regular random (3, s)-SAT instances with different-sized variables
s 7 8 9 10 11 12 13 14 15 N=60 100 100 100 84 43 0 0 0 0 N=90 100 100 100 94 33 0 0 0 0 N=120 100 100 100 95 30 0 0 0 0 N=150 100 100 100 100 17 0 0 0 0 N=180 100 100 100 100 14 0 0 0 0 N=210 100 100 100 100 13 0 0 0 0 表 2 各变元规模下,不同s时每100个严格随机正则(3, s)-SAT实例中各实例的平均求解时间
Table 2. Average solution time for each s in every 100 strictly regular random (3, s)-SAT instances with different-sized variabless
s 9 10 11 12 13 N=60 0.002 4 0.031 5 0.029 2 0.028 6 0.017 6 N=90 0.004 5 0.206 7 0.438 4 0.167 3 0.107 9 N=120 0.008 8 2.493 7 4.854 1 1.436 4 0.595 1 N=150 0.045 0 10.943 7 109.409 0 15.267 6 5.454 7 N=180 0.090 4 124.586 9 1 760.378 0 219.243 4 30.070 8 N=210 0.150 6 747.547 3 57 679.600 0 4 080.987 0 485.358 0 表 3 各变元规模下,相变点附近每100个均匀随机3-SAT实例中可满足的实例总数
Table 3. Total number of satisfied instances near phase transition point in every 100 uniform random 3-SAT instances with different-sized variables
α 3.95 4.05 4.15 4.20 4.25 4.30 4.35 4.45 4.55 N=60 91 84 68 67 62 55 42 35 19 N=90 94 89 72 61 61 45 40 35 8 N=120 94 90 74 64 61 40 37 21 6 N=150 95 91 78 64 57 52 46 18 8 N=180 100 91 76 64 48 44 33 19 5 N=210 100 93 81 70 50 47 30 12 0 N=240 99 99 78 73 50 35 25 12 2 N=270 100 98 88 69 61 48 23 13 0 表 4 各变元规模下,α≃4.267时每100个均匀随机3-SAT实例中各实例的平均求解时间
Table 4. Average solution time for α≃4.267 in every 100 uniform random 3-SAT instances with different-sized variables
N 150 180 210 240 270 平均求解时间/s 1.341 7 8.293 5 76.859 0 361.543 4 2 548.435 0 -
[1] COOK S A.The complexity of theorem-proving procedures[C]//Proceedings of the 3rd Annual ACM Symposium on Theory of Computing.New York:ACM, 1971:151-158. [2] JOHNSON D S.The NP-completeness column:An ongoing guide[J].Journal of Algorithms, 1984, 5(3):433-447. doi: 10.1016/0196-6774(84)90022-1 [3] COOK S A, MITCHELL D G.Finding hard instances of the satisfiability problem:A survey[C]//Satisfiability Problem:Theory and Applications, DIMACS Series in Discrete Mathematics and Theoretical Computer Science.Piscataway, NJ:American Mathematical Society, 1997:1-17. [4] FRIEDGUT E, BOURGAIN J.Sharp thresholds of graph properties, and the k-SAT problem[J].Journal of the American Mathematical Society, 1999, 12(4):1017-1054. doi: 10.1090/S0894-0347-99-00305-7 [5] ACHLIOPTAS D, RICCI-TERSENGHI F.On the solution-space geometry of random constraint satisfaction problems[C]//Proceedings of the 38th Annual ACM Symposium on Theory of Computing.New York:ACM, 2006:130-139. [6] SEMERJIAN G.On the freezing of variables in random constraint satisfaction problems[J].Journal of Statistical Physics, 2008, 130(2):251-293. [7] ACHLIOPTAS D, RICCI-TERSENGHI F.Random formulas have frozen variables[J].SIAM Journal on Computing, 2009, 39(1):260-280. doi: 10.1137/070680382 [8] MÉZARD M, PARISI G, ZECCHINA R.Analytic and algorithmic solution of random satisfiability problems[J].Science, 2002, 297(5582):812-815. doi: 10.1126/science.1073287 [9] MÉZARD M, ZECCHINA R.Random k-satisfiability problem:From an analytic solution to an efficient algorithm[J].Physical Review E, 2002, 66(5):056126. doi: 10.1103/PhysRevE.66.056126 [10] CHVÁTAL V, REED B.Mick gets some (the odds are on his side)[satisfiability] [C]//Proceedings of 33rd Annual Symposium on Foundations of Computer Science.Piscataway, NJ:IEEE Press, 1992:620-627. [11] COJA-OGLAN A, PANAGIOTOU K.Catching the k-NAESAT threshold[C]//Proceedings of the 44th Annual ACM Symposium on Theory of computing.New York:ACM, 2012:899-908. [12] BOUFKHAD Y, DUBOIS O, INTERIAN Y, et al.Regular random k-SAT:Properties of balanced formulas[J].Journal of Automated Reasoning, 2005, 35(1):181-200. http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.71.9897 [13] DING J, SLY A, SUN N.Satisfiability threshold for random regular NAE-SAT[C]//Proceedings of the 46th Annual ACM Symposium on Theory of Computing.New York:ACM, 2014:814-822. [14] RICCI-TERSENGHI F, WEIGT M, ZECCHINA R.Simplest random k-satisfiability problem[J].Physical Review E, 2001, 63(2):026702. doi: 10.1103/PhysRevE.63.026702 [15] MERTENS S, MÉZARD M, ZECCHINA R.Threshold values of random k-SAT from the cavity method[J].Random Structures & Algorithms, 2006, 28(3):340-373. https://www.researchgate.net/publication/1956729_Threshold_values_of_Random_K-SAT_from_the_cavity_method [16] COJA-OGHLAN A.The asymptotic k-SAT threshold[C]//Proceedings of the 46th Annual ACM Symposium on Theory of Computing.New York:ACM, 2014:804-813. [17] DING J, SLY A, SUN N.Proof of the satisfiability conjecture for large k[C]//Proceedings of the 47th Annual ACM on Symposium on Theory of Computing.New York:ACM, 2015:59-68. [18] HAJIAGHAYI M T, SORKIN G B.The satisfiability threshold of random 3-SAT is at least 3.52[EB/OL].Ithaca, New York:Cornell University Library, 2003(2003-10-22)[2015-12-24].http://arxiv.org/abs/math/0310193v2. [19] KAPORIS A C, KIROUSIS L M, LALAS E G.The probabilistic analysis of a greedy satisfiability algorithm[J].Random Structures & Algorithms, 2006, 28(4):444-480. http://www.docin.com/p-1284908643.html [20] IMPAGLIAZZO R, LEVIN L A, LUBY M.Pseudo-random generation from one-way functions[C]//Proceedings of the 21st Annual ACM Symposium on Theory of Computing.New York:ACM, 1989:12-24. [21] XU K, LI W.Exact phase transitions in random constraint satisfaction problems[J].Journal of Artificial Intelligence Research, 2000, 12(1):93-103. https://www.researchgate.net/publication/220543100_Exact_Phase_Transitions_in_Random_Constraint_Satisfaction_Problems [22] XU K, LI W.Many hard examples in exact phase transitions[J].Theoretical Computer Science, 2006, 355(3):291-302. doi: 10.1016/j.tcs.2006.01.001 [23] XU K, BOUSSEMART F, HEMERY F, et al.Random constraint satisfaction:Easy generation of hard (satisfiable) instances[J].Artificial Intelligence, 2007, 171(8):514-534. https://www.researchgate.net/publication/222836051_Random_constraint_satisfaction_Easy_generation_of_hard_satisfiable_instances [24] TOVEY C A.A simplified NP-complete satisfiability problem[J].Discrete Applied Mathematics, 1984, 8(1):85-89. doi: 10.1016/0166-218X(84)90081-7 [25] DUBOIS O.On the r, s-SAT satisfiability problem and a conjecture of Tovey[J].Discrete Applied Mathematics, 1990, 26(1):51-60. doi: 10.1016/0166-218X(90)90020-D [26] 许道云.极小不可满足公式在多项式归约中的应用[J].软件学报, 2006, 17(5):1204-1212. doi: 10.1360/jos171204XU D Y.Applications of minimal unsatisfiable formulas to polynomially reduction for formulas[J].Journal of Software, 2006, 17(5):1204-1212(in Chinese). doi: 10.1360/jos171204 [27] RATHI V, AURELL E, RASMUSSEN L, et al.Bounds on threshold of regular random k-SAT[C]//13th International Conference on Theory and Applications of Satisfiability Testing.Berlin:Springer, 2010:264-277. [28] CASTELLANA M, ZDEBOROVÁ L.Adversarial satisfiability problem[J].Journal of Statistical Mechanics:Theory and Experiment, 2011, 2011(3):P03023. https://www.researchgate.net/publication/47690852_Adversarial_Satisfiability_Problem?_sg=Y3g-baxTMwJE8kgA06289ds_dXJb9WjNn5JyBUKansJ55pCSNuFsEgDOpmXMxk3gQ2cchxf5Jih6XDpuu3Os7g [29] SUMEDHA S, KRISHNAMURTHY S, SAHOO S.Balanced K-satisfiability and biased random K-satisfiability on trees[J].Physical Review E, 2013, 87(4):042130. doi: 10.1103/PhysRevE.87.042130 [30] KRISHNAMURTHY S.Exact satisfiability threshold for k-satisfiability problems on a Bethe lattice[J].Physical Review E, 2015, 92(4):042144. doi: 10.1103/PhysRevE.92.042144 [31] BAPST V, COJA-OGHLAN A.The condensation phase transition in the regular k-SAT model[EB/OL].Ithaca, New York:Cornell University Library, 2015(2015-10-07)[2015-12-24].http://arxiv.org/pdf/1507.03512v3. [32] KSCHISCHANG F R, FREY B J, LOELIGER H A.Factor graphs and the sum-product algorithm[J].IEEE Transactions on Information Theory, 2001, 47(2):498-519. doi: 10.1109/18.910572 [33] KIRKPATRICK S, SELMAN B.Critical behavior in the satisfiability of random Boolean expressions[J].Science, 1994, 264(5163):1297-1301. doi: 10.1126/science.264.5163.1297 [34] FLAJOLET P, SEDGEWICK R.Analytic combinatorics[M].Oxford:Cambridge University Press, 2009. [35] ROBBINS H.A remark on Stirling's formula[J].The American Mathematical Monthly, 1955, 62(1):26-29. doi: 10.2307/2308012 [36] CHVÁTAL V, SZEMERÉDI E.Many hard examples for resolution[J].Journal of the ACM, 1988, 35(4):759-768. doi: 10.1145/48014.48016 [37] DAVIS M, LOGEMANN G, LOVELAND D.A machine program for theorem-proving[J].Communications of the ACM, 1962, 5(7):394-397. doi: 10.1145/368273.368557 [38] MOSKEWICZ M W, MADIGAN C F, ZHAO Y, et al.Chaff:Engineering an efficient SAT solver[C]//Proceedings of the 38th Annual Design Automation Conference.New York:ACM, 2001:530-535.