可满足性问题的结构特征进展综述.pdf

2023 年11月郑 州 大 学 学 报(工 学 版)Nov.2023第 44 卷第 6 期Journal of Zhengzhou University(Engineering Science)Vol.44No.6收稿日期:2022-11-01;修订日期:2022-12-03基金项目:国家自然科学基金资助项目(62062001);宁夏自然科学基金资助项目(2020AAC03214);宁夏青年拔尖人才项目(2021)作者简介:王晓峰(1980),男,甘肃会宁人,北方民族大学副教授,博士,主要从事算法分析与设计、人工智能等研究,E-mail:xfwang 。引用本文:王晓峰,庞立超,莫淳惠,等.可满足性问题的结构特征进展综述J.郑州大学学报(工学版),2023,44(6):40-47.(WANG X F,PANG L C,MO C H,et al.A review of structural characteristics of satisfiability problemsJ.Journal of Zhengzhou University(Engineering Science),2023,44(6):40-47.)文章编号:1671-6833(2023)06-0040-08可满足性问题的结构特征进展综述王晓峰1,2,庞立超1,莫淳惠1,杨易1,赵星宇1,杨澜1(1.北方民族大学 计算机科学与工程学院,宁夏 银川 750021;2.北方民族大学 图像图形智能处理国家民委重点实验室 宁夏,银川 750021)摘要:可满足性(SAT)问题是人工智能的基础问题,也是 NP 难问题,在机器学习、模式识别和自然语言处理等领域有着实际应用。然而,随着人工智能发展,越来越多的问题呈现出更为复杂的形态,原有的算法不再适用,需进一步优化或者改进,这对基础研究提出了更高要求。为了研究 SAT 问题难解的内在本质,需要研究其结构特征,进而找出求解 SAT 问题的高效算法。近年来备受研究人员关注的相变、树宽、结构熵、DNA 折纸术是 SAT 问题结构特征的 4 种常用度量模型。为了理清关于 SAT 问题结构特征的研究进展,基于上述 4 种度量模型,对 SAT 问题的结构特征进行了综述,指出了 SAT 问题结构特征研究所面临的挑战及未来的方向。在 SAT 问题求解中相变分析、树分解算法、结构熵及 DNA 折纸术等方面虽已取得一定的研究成果,但在相变点精确上界的求解、结构度量模型指导 SAT 求解器设计,以及树分解算法效率的提高等方面仍待突破,这将成为未来关于 SAT 问题结构特征研究的重点。关键词:SAT 问题;相变;树分解;结构熵;DNA 折纸术中图分类号:TP301文献标志码:Adoi:10.13705/j.issn.1671-6833.2023.03.013约束满足问题(constraint satisfaction problem,CSP)1又称约束网络,在计算机科学、数学和物理学等学科中占据重要地位。CSP 在许多领域(如模式识别、交通规划和人机交互等领域)中发挥着重要的作用。从旅行商、图着色等经典问题到神经网络、图像识别等大型应用问题,都可以转化为 CSP问题进行求解。布尔可满足性问题(boolean satisfiability prob-lem,SAT)是 CSP 问题的子问题,同时也是一个 NP完全(NP-complete)问题2。现阶段,解决 SAT 问题的算法有完备算法、非完备算法及组合算法。近年来这 3 类算法都取得了一些研究成果,如 DPLL(da-vis putnam logemann loveland)算法3、消息传送算法4、演化计算算法5等。然而,针对大规模问题实例、难满足问题实例等,多数求解器无能为力。研究发现,SAT 问题的求解难度与其结构特征紧密联系。因此,研究 SAT 问题的结构特征对设计求解SAT 问题的高效算法具有十分重要的意义。其中,相变、树宽、结构熵、DNA 折纸术是研究 SAT 问题结构特征的 4 种常用度量模型。本文也将对上述 4 种度量模型的概念及其相关应用展开综述。首先,对相关知识进行介绍;其次,对 4 种度量模型的基本概念、相关原理及其在 SAT 问题的应用进行介绍;再次,指出研究 SAT 问题结构特征面临的挑战及研究方向;最后,总结全文。1相关知识1.1SAT 问题若干个文字的析取构成一个子句6,记为 C=L1L2Ln,若干子句的合取构成一个合取范式(conjunctive normal form,CNF)公 式,记 为 F=C1C2Cm,SAT 判定问题指是否存在一组指派能够使 CNF 公式为真。1.2因子图给定 CNF 公式 F=C1C2Cm,其中,子句为 C1,C2,Cm,变元为 x1,x2,xn,为方便表第 6 期王晓峰,等:可满足性问题的结构特征进展综述 41 示,将 xi简记为 i。公式 F 能够表示为一个二部网络 G=(CX,E),G 称为因子图,如图 1 所示。图 1中的一侧以布尔变元集为变元节点(图 1 中用圆形表示),而另一侧以子句集为子句节点(图 1 中用矩形表示)。因子图中的实边和虚边包含 CNF 公式的2 种不同的信息。实边:(Ci,j)E变元 xi在子句 Ci中正出现。虚边:(Ci,j)E变元 xi在子句 xi中负出现。例:对于一个 CNF 公式,F=(x1 x2 x3)(x1 x2x3)(x2x3x4)=a1,a2,a3 的因子图 G=(CX,E)。图 1因子图Figure 1Factor graph2解空间聚类是指将数据空间实体划分,把相似实体划分为一个簇。同一类簇的任意 2 个点的距离小于不同簇的任意 2 个点间的距离7。目前已有部分研究者用 聚 类 研 究 SAT 问 题 解 空 间 的 性 质。Mezard等8证明 XOR-SAT 问题中存在解聚类成簇的现象;Maneva 等9引入覆盖的概念,进一步证明随机k-SAT 问题(子句长度为 k)解空间的聚类现象。接着,Achlioptas 等7证 明了聚类的 存在性;莫孝 玲等6分析研究了 CNF 公式赋值空间的可满足解的聚类现象。CNF 公式赋值空间中存在可满足解聚类现象,并且随着约束密度的变化可满足解聚类的个数也发生变化。k-SAT 问题是研究较多的一类 SAT 问题。自从统计物理学家利用复本对称破缺平均场理论预测出k-SAT 问题的解空间在临界约束密度结构上发生定性改变后,各个领域的研究人员开始通过概率分析、算法分析、数理统计等方法对 k-SAT 问题的结构特征进行大量研究,尝试找出 k-SAT 问题的难解本质。解空间被划分为许多子空间,这种突变现象被称为簇集相变。相变研究 SAT 问题解空间的分布情况,观察满足与不可满足之间的变化规律,即解的临界特征。随机 k-SAT 问题是 SAT 问题的子问题。对于随机k-SAT 问题的实例产生模型 G(n,k,m),统计结果表明,子句约束密度 =m/n(m 为子句数,n 为变元数)是一个关键的参数,该参数刻画了随机 k-SAT问题解的临界特征和实例的难解程度。然而,对于正则 SAT 问题,子句约束密度恒为常数,该参数已无法反映正则 SAT 问题的相变现象。近年来,研究人员利用一阶矩和二阶矩证明了 SAT 相变问题。一阶矩方法的理论依据是马尔可夫不等式10,通过一阶矩方法可得到随机 CNF 公式高概率不可满足判定条件。一阶矩引理如下。引理 1设 X 为随机变量且为非负整数值,对任意的 a0,都有p(X a)EXa。(1)使用方差估计特定随机事件发生概率的方法称为二阶矩方法,该方法的理论依据是切比雪夫不等式11。二阶矩引理如下。引理 2如果 X 为随机变量且为非负整数值,那么p(X=0)p(|X-EX|EX)Var(X)(EX)2。(2)当前,对相变性质的研究主要集中于 k-NAE-SAT12、Regular 2-SAT13以及 Regular NAE-SAT14等具有特殊结构的 SAT 问题的确切相变点。张明明等15发现在规模较小的情况下,正则 3-SAT 问题的相变点有偏移现象,并从变元自由度的角度给出定性解释。周锦程等16不但证明严格随机正则(3,s)-SAT 问题可满足临界点的上界,而且给出的严格随机正则(3,s)-SAT 实例产生模型可以构造在相变点 s=11 处的随机 3-SAT 难解实例。王永平等17使用一阶矩方法,研究出取定 s 的严格 d-正则随机(3,2s)-SAT 问题的可满足临界值的一个下界。进一步,周锦程等18又以覆盖总数作为一阶矩方法的随机变量,获得随机正则(k,r)-SAT 问题可满足临界值点的一个最紧致界。Ding 等14研究了随机(d,k)-NAE-SAT 问题的相变,并给出一个关于变元出现次数 d 的相变控制参数。综述至此发现,关于规则问题相变的证明技术主要基于一阶矩和二阶矩。然而,使用二阶矩时需要处理一个高阶无穷小量,这是困难的,因此,还有大量的开放问题未获得严格的相变点。3树宽随着 SAT 问题研究的不断深入,基于图论的方法成为重要的研究方法之一,图结构的特殊性质和表达能力在 SAT 问题研究中得到应用。这些图结构的性质逐渐成为探索 SAT 问题难解本质和设计42 郑 州 大 学 学 报(工 学 版)2023 年SAT 问题求解算法的重要方法之一。聂国霞等19将 CNF 公式转化成因子图,通过研究因子图的结构和性质,进而研究 CNF 公式的可满足性。因为子句和变元之间的复杂联系,所以 SAT 实例存在潜在的结构特征。刘纯20也将 SAT 实例表示为图模型,利用数据挖掘技术分析子句和子句之间以及变元之间的潜在结构信息。1972 年,Bertele 等21首 次 引 入 树 宽(tree width),后来,Arnborg 等22确定任意图的树宽本身就是一个 NP 难问题。20 世纪 80 年代发展起来的图子式理论是重要的图理论分支。Fellows 等23在1988 年就研究了图子式理论在算法分析与设计中的应用。树分解是将给定图 G 的节点集合 V 划分,使图 G 尽可能地划分为树形结构,通过研究树的结构信息来刻画原图的一些性质。树宽是衡量图树分解程度好坏的指标。正如 Enright 等24的研究表明,如果随机组合 2 个非常简单的层,每个层由 n 个顶点的路径组成,那么所生成的网络的树宽将以高概率随 n 增长。无向图的树宽是 G 的所有树分解中的宽度最小值。图的树宽和弦图关系密切,借助弦图可给出树宽的等价定义,即图 G 的树宽为其所有超弦图 H中最小的一个最大团减 1。虽然树分解的结构是树宽的经典表现形式,但如果树分解的形式是受限制的,则许多问题可以用动态规划来描述和解决。路径分解是树分解的另一个版本,它应用了一些动态规划算法的定义,换言之,图的路径分解是动态规划算法的重要组成部分。因此,图 G 的路径分解是 G 的树分解,其中底层的树 T 是一条路径。人工智能、数据库和逻辑电路设计等领域的诸多实际应用通常采用启发式算法构造树分解。在以往的研究中,构造树分解的启发式方法一般有 2 类。一类是基于消点序的启发式搜索算法。所谓消点(也可以称为消元)是指删除无向图 G 中的某个节点 v 以及与 v 相连的边,同时在剩下的图中添加一些边,使得 v 原来的邻节点构成一个三角剖分。通过在初始的图 G 中逐个消元的方法可以生成 G 的一个消点序,根据这个消点序便能构造出图 G 的一个树分解。由于消点序的选择存在一定的随机性,因此,不同的消元顺序可以得到不同的树分解。此外,由于求解最优消元顺序是一个 NP 难问题,研究者常采用启发式方法求解图的消点序。如最小度搜索算法(minimum degree search)25、最大势搜索算法(maximum cardinality search)及其改进算法26、最小缺边搜索算法(minimum deficiency search)27等。另一类是基于割集的启发式搜索算法,即通过在初始图中找到某些割集来构造树分解。所谓割集是指在无向图 G=(V,E)中,若存在 E E 使得p(G-E)p(G),且 对 于 任 意 的 E E,均 有p(G-E)p(G),则称 E为 G 的边割集,简称为割集。基于割集的方法来构造图 G 的树分解的过程相较于利用消点序的方法更复杂,但 Amir28验证了基于割集的方法在一些问题研究中更为有效。事实上,树分解在众多研究领域一直都有着重要的用途。Arnborg 等29利用树分解来求解组合优化问题;Koster 等30讨论了利用树分解解决计算生物学的问题;Zhao 等31探讨了利用树分解来解决社交网络问题。随着研究的不断深入,Adcock 等32引入特殊的树形结构,将正则 CNF 公式的因子图转换为树形结构,并证明随机正则(3,r)-SAT 问题的可能相变点。莫孝玲等6通过引入树分解技术,将 CNF 公式的因子图分解为一棵树。谢志新等33提出一种度量命题公式结构特征的树宽算法,并给出不同规模随机实例算法收敛时的树宽充分条件。4结构熵信息传播算法34是否收敛取决于因子图的结构。近年来,随着实例集不断增大,因子图的结构也变得复杂。由于信息熵可以度量不确定性,是概率分布的静态度量方法。在信息论中,根据概率分布选择节点,则熵值反映了确定节点代码所需的平均信息量。所以,在通信领域中,信息熵只测量点与点之间的单个信息。在此基础上,Li 等35首次提出结构熵。结构熵被定义为节点编码所需的最小总位数,该节点可通过随机游走来访问。与信息熵不同,结构熵是一种能够反映网络复杂性的动态度量方法,因此,结构熵弥补了信息熵的缺陷。不确定信息最小化是实现网络结构熵度量过程中遵循的基本原则。为保证因子图不确定信息最小化,对因子图进行精确的社区结构划分。Newman 等36于 2004 年首次提出模块度,模块度能定量地评估不同社区划分算法结果的准确度以及评价网络中社区结构的质量。虽然模块度有着清晰的定义,但无法识别小规模的社区结构,即存在分辨率37的问题。基于模块度的社区发现算法有 GN算法、Louvain 算法、FN 算法36等。其实最初设计模块度的目的是用来对 GN 算法进行质量评估。随着研究的不断深入,该模型得到研究人员的普遍认第 6 期王晓峰,等:可满足性问题的结构特征进展综述 43 可,于是,衍生出大量与模块度相关的算法。Rotta等38对 Louvain 算法加入更多层次的细化阶 段。Blondel 等39提出图 折叠算法(gragh folding algo-rithm),该算法也称为模块性优化算法,因为该算法具有时间复杂度低的特点,所以相关研究人员认为它是目前性能最佳的社区划分算法。4.1二维结构熵若一个具有 n 个节点、m 个变量的图 G=(V,E)是带权无向连通图,V 为图 G 中的顶点集,E 为图G 中的边集。设 P=X1,X2,XL 为节点集合 V的划分。定义划分 P 的结构熵如下:Hp(G)=Lj=1VjVol(G)Hd(j)1Vj,d(j)2Vj,d(j)njVj()-Lj=1gjVol(G)log2VjVol(G)=-Lj=1VjVol(G)nji=1d(j)iVjlog2d(j)iVj-Lj=1gjVol(G)log2VjVol(G)。(3)式中:L 为划分 P 中的划分个数;nj为 Xj中的顶点数;d(j)i为社区 Xj中第 i 个节点的度数;Vj=Vol(Xj);gj为社区 Xj与其他社区相连的边数。二维结构熵定义为H2(G)=minHp(G)。(4)4.2K 维结构熵对于无向连通图 G=(V,E),假设 T 为社区模块树,定义编码树的结构熵如下:HT(G)=T,HT(G,);HT(G,)=-g2mlog2VV-。(5)式中:m=|E|;V为 T中所有节点的度数之和,即集合 T的体积;g为从 T内的节点到 T外的节点的边数。连通图 G 的 K 维结构熵定义:HK(G)=minT:h(T)KHT(G)。(6)其中 T 在 G 的所有编码树高度不高于维度 K。对于非连通图 G 的 K 维结构熵定义如下:HK(G)=1Vol(G)Lj=1Vol(Gj)HK(Gj)。(7)式中:Vol(Gj)为 Gj的体积;G1,G2,GL为图 G 的所有连通分支。K 维结构信息是网络动态复杂性的一个指标,衡量网络交互、通信、操作等的复杂性。指标满足可加性、局部性、稳健性、局部和增量可计算性等基本属性。Brooks40将结构信息的量化问题列为计算机科学面临的三大挑战之首。Liu 等41证明,结构信息是冯诺依曼图熵的一个很好的近似,同时实现了可证明的精度、可扩展性和可解释性。熵测度起源于量子信息论,用于描述密度矩阵表示的量子系统的混合性。Braunstein 等42首次使用冯诺依曼图熵通过将缩放拉普拉斯矩阵视为密度矩阵来衡量图的复杂性。众所周知,拉普拉斯谱包含图的多尺度结构的丰富信息,因此,熵在复杂网络分析和模式识别的下游任务中得到广泛应用。当前对结构熵的应用研究已经取得了一些成果。网络中各种行为的不确定性是网络复杂性的本质。Li 等35的研究表明,最小化二维结构熵是检测网络自然社区结构的原则,并用 K 维结构熵度量 K维网络的动态复杂性。Zhang 等43发现解决命题公式的困难程度与 d 公式的结构熵大小有关,公式的压缩信息越小,求解公式就越困难。其次,提出了一种-近似策略来近似大型公式的结构熵。牛进等44提出了 WPLPA 算法,并基于二维结构熵提出命题公式的结构熵度量模型,给出 BP 算法收敛的充分条件,之后又利用结构熵表示命题公式的结构信息,给出 WP 算法收敛的充分条件。限于篇幅,不再一一赘述。5DNA 折纸术DNA 折纸术是利用碱基互补配对原则和 DNA分子所具有的结构特征,将一条较长的 DNA 单链(通常称为脚手架链)的特定区域进行折叠,并用较短的 DNA 片段(通常称为订书钉链)加以固定,构造出预期的纳米图案或结构。最终得到的结构大小、形状取决于特殊的订书钉链。与传统 DNA 自组装技术相比,DNA 折纸术更容易组合出结构稳定、精密度高及可控性高的纳米结构,并且具有组装速度快、生物毒性较低、易于操作、纳米可寻址性和可编程性等优点。随着分子生物学、热力学及电子学技术的不断发展,DNA 自组装的形式从一维到二维再到三维,在 NP 问题中起到不可或缺的作用。1994 年,Adleman 教授45首次利用 DNA 分子实验解决了有向图的哈密顿问题。次年,Lipton46在 Adleman 的实验基础上,给出一种解决可满足性问题的 DNA 计算模型。2000 年,Sakamoto 等47利用 DNA 分子自组装,为可满足性问题的求解提供一种新方法。2002 年,Braich 等48利用 DNA 折纸术成功地解决了变量 n=20 的 3-SAT 问题。次年,张凤月等49首次提出了一种利用荧光标记的策略,解决了可满足问题。周康等50在 2009 年提出了解决可满足性问题的闭环 DNA 算法;Xiao 等51在 201344 郑 州 大 学 学 报(工 学 版)2023 年年给出了可满足性问题的 DNA 计算模型。2017年,马莹等52利用微流路芯片高压凝胶电泳,给出了可满足性问题的生物芯片 DNA 计算模型。2020年,陈哲53给出了一个利用动态 DNA 计算模型去解决 3-SAT 问题的方法。2021 年,麻晶晶等54提出了一种利用 DNA 折纸术解决可满足性问题的DNA 计算模型。上述利用 DNA 求解的可满足性问题,几乎都不是大规模可满足性问题。然而,随着人工智能的发展,可满足性问题的规模越来越大,因此,找出基于DNA 折纸术求解大规模可满足性问题的算法是值得研究的。6讨论与展望首先,对各种 SAT 问题结构度量模型的优缺点进行总结和分析;其次,对各种模型在 SAT 问题上未来可能的应用进行讨论。表 1 总结了研究 SAT问题结构的各种度量模型的优缺点。相变、树宽、结构熵和 DNA 折纸术等结构度量模型使可满足性问题的求解有了长足的发展,但仍存在许多值得深入研究的问题,主要包括以下方面。(1)相变分析方面。深入研究一阶矩和局部最大值方法,探索相变点的精确上界。在运用二阶矩方法得到可满足性问题相变点的下界时,往往需要刻画组合解的空间结构,并且要处理一个关于常数1 的高阶无穷小量问题,这是困难的。因此,探寻新方法(小子图条件)能够得到更优的下界。(2)结构熵度量模型方面。计算模块度和结构熵本质上就是对图节点进行划分,现有结构熵的计算算法时间复杂度较高,可以利用性能较好的社区划分算法思想改进现有的结构熵计算方法。结构熵是度量图结构信息的有效方法,设计一种高效的基于结构熵指导的 SAT 求解器具有非凡意义。(3)树分解算法方面。针对 CNF 公式实例的因子图,分析及比较现有树分解算法,提高 SAT 问题实例的因子图的树分解算法求解效率。表 1研究 SAT 结构特征的各种度量模型的优缺点Table 1The advantages and disadvantages of various measurement models for studying the structural characteristics of SAT应用领域度量模型代表性文献优点缺点解空间相变文献7-9,12-18可测试算法的性能;有助于理清相变控制参数与 SAT 问题难解之间的变化规律相变分析方法比较单一,而且烦琐;二阶矩求得的相变点下界精确度较差图论树宽文献21-24,29-33为设计求解树宽较小的难解问题提供思路;可度量 SAT 问题的因子图的结构特性现有的树分解算法求解时间较长信息论结构熵文献35,40-44结构熵原理简单,使用范围广,验证条件简单;有效分析 SAT 问题的解空间的结构信息现有的求解结构熵的算法时间复杂度较大分子生物学DNA 折纸术 文献45-51,53-54可视化 SAT 问题;操作简单;效率高;降 低 了 可 满 足 性 问 题 的 复 杂度;具有较大的并行性DNA 折纸基底尺寸有限;不适用于大规模 SAT 问题的求解(4)DNA 折纸术方面。深入研究 DNA 折纸计算模型,探索新的基于 DNA 求解 SAT 问题算法,改善 DNA 折纸术在超大规模的 SAT 问题效果。(5)混合使用结构度量模型方面。深入理解命题公式的结构熵度量模型原理,建立结构熵与相变之间的详细变化规律,并分析基于结构熵的信息传播算法的收敛性。(6)结构度量模型内在联系方面。深入理解相变、树宽、结构熵和 DNA 折纸术度量模型的内部度量原理,找出它们的内在联系,并分析出它们各自度量适用的 SAT 问题类型。(7)信息传播算法的收敛性方面。信息传播算法的性能取决于命题公式的结构特征,因此,建立结构度量模型与信息传播算法收敛性之间的关系有重要意义。(8)结构特征方面。根据可满足性问题的结构特征,优化已有 SAT 求解器,给出求解 SAT 问题的高效算法,并分析算法的收敛性及近似度等性能。7结语自 1991 年以来,SAT 问题受到研究人员的广泛关注,其在人工智能、密码学、数学、计算机科学等领域具有重要实际价值。本文重点研究 SAT 问题的结构特征,将结构度量模型划分为相变、树宽、结构第 6 期王晓峰,等:可满足性问题的结构特征进展综述 45 熵、DNA 折纸术,并概述总结了上述 4 种结构度量模型及其在 SAT 问题上的应用。最后,对未来研究SAT 问题的结构特征可能面临的挑战及研究方向进行了讨论与展望。参考文献:1DYER M,FRIEZE A,MOLLOY M.A probabilistic a-nalysis of randomly generated binary constraint satisfac-tion problemsJ.Theoretical Computer Science,2003,290(3):1815-1828.2VIZEL Y,WEISSENBACHER G,MALIK S.Boolean satisfiability solvers and their applications in model chec-king J.Proceedings of the IEEE,2015,103(11):2021-2035.3DAVIS M,PUTNAM H.A computing procedure for quantification theoryJ.Journal of the ACM,1960,7(3):201-215.4ZHAO C Y,ZHOU H J,ZHENG Z M,et al.A mes-sage-passing approach to random constraint satisfaction problems with growing domainsJ.Journal of Statistical Mechanics:Theory and Experiment,2011,2011(2):P02019.5WANG H F,FAN H,LI F L.Quantum algorithm for sol-ving some discrete mathematical problems by probing their energy spectraJ.Physical Review A,2014,89:012306.6莫孝玲,许道云.CNF 公式赋值空间上可满足解的概率性质J.计算机科学与探索,2018,12(11):1852-1861.MO X L,XU D Y.Probabilistic properties of satisfiable solutions on space of assignments for CNF formula J.Journal of Frontiers of Computer Science and Technology,2018,12(11):1852-1861.7ACHLIOPTAS D,COJA-OGHLAN A,RICCI-TERSEN-GHI F.On the solution-space geometry of random con-straint satisfaction problems J.Random Structures&Algorithms,2011,38(3):251-268.8MEZARD M,RICCI-TERSENGHI F,ZECCHINA R.Two solutions to diluted p-spin models and XORSAT problemsJ.Journal of Statistical Physics,2003,111(3):505-533.9MANEVA E,SINCLAIR A.On the satisfiability thresh-old and clustering of solutions of random 3-SAT formulasJ.Theoretical Computer Science,2008,407(1/2/3):359-369.10 MITZENMACHER M,UPFAL E.概率与计算M.冉启康等译.北京:机械工业出版社,2020.MITZENMACHER M,UPFAL E.Probability and com-putingM.RAN Q K,et al.Translated.Beijing:Chi-na Machine Press,2020.11 HARDY G H,LITTLEWOOD J E,PLYA G.Inequali-ties:a mathematical olympiad approachM.Cambridge:Cambridge University Press,1952.12 COJA-OGLAN A,PANAGIOTOU K.Catching the k-NAESAT threshold CProceedings of the Forty-fourth Annual ACM Symposium on Theory of Computing.New York:ACM,2012:899-908.13 BOUFKHAD Y,DUBOIS O,INTERIAN Y,et al.Regu-lar random k-SAT:properties of balanced formulas J.Journal of Automated Reasoning,2005,35(1):181-200.14 DING J,SLY A,SUN N K.Satisfiability threshold for random regular NAE-SATJ.Communications in Mathe-matical Physics,2016,341(2):435-489.15 张明明,许道云.正则 3-SAT 问题的相变现象J.计算机科学,2016,43(4):33-36.ZHANG M M,XU D Y.Phase transition phenomenon of regular 3-SAT problemJ.Computer Science,2016,43(4):33-36.16 周锦程,许道云,卢友军.随机正则(k,r)-SAT 问题的可满足临界J.软件学报,2016,27(12):2985-2993.ZHOU J C,XU D Y,LU Y J.Satisfiability threshold of the regular random(k,r)-SAT problem J.Journal of Software,2016,27(12):2985-2993.17 王永平,许道云.取定 s 的严格 d-正则随机(3,2s)-SAT 问题的可满足临界J.软件学报,2021,32(9):2629-2641.WANG Y P,XU D Y.Satisfiability threshold of strictly d-regular random(3,2s)-SAT problem for fixed s J.Journal of Software,2021,32(9):2629-2641.18 周锦程,许道云,卢友军.基于 1RSB 的正则(k,r)-SAT 问题可满足临界J.华中科技大学学报(自然科学版),2017,45(12):7-13.ZHOU J C,XU D Y,LU Y J.Satisfiability threshold of regular(k,r)-SAT problem via 1RSB theoryJ.Journal of Huazhong University of Science and Technology(Natu-ral Science Edition),2017,45(12):7-13.19 聂国霞,秦永彬,许道云.基于因子图求解(3,4=)-CNF 公式类下可满足问题J.计算机与数字工程,2013,41(5):686-689.NIE G X,QIN Y B,XU D Y.Based on the factor graph for solving satisfiability problem of(3,4=)-CNF formula class J.Computer&Digital Engineering,2013,41(5):686-689.20 刘纯.基于聚类的 SAT 实例结构分析D.武汉:华中科技大学,2015.LIU C.The structural analysis of SAT instance based on clusteringD.Wuhan:Huazhong University of Science and Technology,2015.21 BERTELE U,BRIOSCHI F.Nonserial dynamic program-46 郑 州 大 学 学 报(工 学 版)2023 年mingM.New York:Academic Press,1972.22 ARNBORG S,CORNEIL D G,PROSKUROWSKI A.Complexity of finding embeddings in a k-treeJ.SIAM Journal on Algebraic Discrete Methods,1987,8(2):277-284.23 FELLOWS M R,LANGSTON M A.Nonconstructive tools for proving polynomial-time decidability J.Journal of the ACM,1988,35(3):727-739.24 ENRIGHT J,MEEKS K.Deleting edges to restrict the size of an epidemic:a new application for treewidthJ.Algorithmica,2018,80(6):1857-1889.25 雷莹.树 分 解 算 法 在 可 满 足 性 问 题 中 的 应 用 研 究D.贵阳:贵州大学,2020.LEI Y.Tree decomposition algorithm and application for the SATD.Guiyang:Guizhou University,2020.26 TARJAN R E,YANNAKAKIS M.Simple linear-time al-gorithms to test chordality of graphs,test acyclicity of hy-pergraphs,and selectively reduce acyclic hypergraphsJ.SIAM Journal on Computing,1984,13(3):566-579.27 HELL P,KIRKPATRICK D G.Algorithms for degree constrained graph factors of minimum deficiency J.Journal of Algorithms,1993,14(1):115-138.28 AMIR E.Approximation algorithms for treewidthJ.Al-gorithmica,2010,56(4):448-479.29 ARNBORG S,PROSKUROWSKI A.Linear time algo-rithms for NP-hard problems restricted to partial k-treesJ.Discrete Applied Mathematics,1989,23(1):11-24.30 KOSTER A M C A,VAN HOESEL S P M,KOLEN A W J.Solving partial constraint satisfaction problems with tree decompositionJ.Networks,2002,40(3):170-180.31 ZHAO J Z,MALMBERG R L,CAI L M.Rapid ab initio prediction of RNA pseudoknots via graph tree decomposi-tionJ.Journal of Mathematical Biology,2008,56(1):145-159.32 ADCOCK A B,SULLIVAN B D,MAHONEY M W.Tree decompositions and social graphsJ.Internet Mathemat-ics,2016,12(5):315-361.33 谢志新,王晓峰,于卓,等.基于树宽的警示传播算法收敛性分析