一种求解布尔不可满足子式的局部搜索算法

解释布尔公式不可满足的原因在众多领域都具有非常重要的理论与应用价值,而不可满足子式能够为公式不可满足的原因提供精确的解释,帮助应用领域的自动化工具迅速定位错误,诊断问题失败的本质缘由。近年来涌现了许多基于SAT求解器DPLL回溯搜索过程的完全算法,但关于不完全方法提取不可满足子式的研究相对较少。因此,本文提出一种采用启发式局部搜索过程从公式的不可满足性证明中求解布尔不可满足子式的算法。该算法根据公式的消解规则通过局部搜索过程直接构造证明不可满足性的消解序列,并融合了布尔推理技术以提高搜索效率;而后通过一个递归过程遍历证明序列从而得到不可满足子式。通过实验与贪心遗传算法进行对比,结果表明本文提出的算法优于贪心遗传算法。     

求解极小SMT不可满足子式的宽度优先搜索算法

极小不可满足子式能够为可满足性模理论(SMT)公式的不可满足的原因提供精确的解释,帮助自动化工具迅速定位错误.针对极小SMT不可满足子式的求解问题,提出了SMT公式搜索树及其3类结点的概念,并给出了不可满足子式、极小不可满足子式与3类结点之间的映射关系.基于这种映射关系,采用宽度优先的搜索策略提出了宽度优先搜索的极小SMT不可满足子式求解算法.基于业界公认的SMT Competition 2007测试集进行实验的结果表明,该算法能够有效地求解极小不可满足子式.     

基于否证蕴含的极小一阶不可满足子式求解算法

解释公式不可满足的原因在软件分析与验证等众多领域都具有非常重要的理论与应用价值,而极小不可满足子公式能够为公式不可满足的原因提供精炼的解释,帮助应用领域的自动化工具迅速定位错误,准确地诊断问题失败的本质缘由.文中针对极小一阶不可满足子式的求解问题,引入了否证蕴含图及其正向与逆向可达结点的概念,并证明了不可满足子式与否证蕴含图之间的关系.基于二者的关系,提出了基于冲突分析与否证蕴含的极小一阶不可满足子式求解算法,并融合了蕴含图剪枝技术,以提高算法效率.通过实验与当前最优的深度优先搜索算法进行了比较,结果表明:文中的算法显著优于深度优先搜索算法,并且随着公式复杂度的增加,性能优势更加明显.     

布尔不可满足子式的求解方法研究进展

解释布尔公式不可满足的原因在诸如形式化验证与电子设计自动化等众多领域中都具有非常重要的理论与应用价值.不可满足子式能够为布尔公式不可满足的原因提供精确的解释,帮助应用领域的自动化工具迅速定位错误,诊断问题失败的本质缘由.针对近年来出现的许多求解布尔不可满足子式的研究工作,根据算法的类型归类比较,对各种求解方法进行了概述评论,并简要介绍了在该领域所做的一些研究工作.最后讨论了布尔不可满足子式的求解方法目前面临的主要挑战,并对今后的研究方向进行了展望.     

针对MUS求解问题的加强剪枝策略

极小不可满足子集(minimal unsatisfiable subsets, MUS)的求解是布尔可满足性问题中的一个重要子问题. 对于一个给定的不可满足问题, 其MUS的求解能够反映出问题中导致其不可满足的关键原因. 然而, MUS的求解是一项极其耗时的任务, 不同的剪枝过程将直接影响到搜索空间的大小、算法的迭代次数, 从而影响算法的求解效率. 提出一种针对MUS求解的加强剪枝策略ABC (accelerating by critical MSS), 依据MSS、MCS、MUS这3者之间的对偶性和碰集关系特点, 提出cMSS和subMUS概念, 并总结出4条性质, 即每个MUS必是subMUS的超集, 进而在避免对MCS的碰集进行求解的情况下有效利用MUS和MCS互为碰集的特征, 有效避免求解碰集时的时间开销. 当subMUS不可满足时, 则subMUS是唯一的MUS, 算法将提前结束执行; 当subMUS可满足时, 则剪枝掉此节点, 进而有效避免对求解空间中的冗余空间进行搜索. 同时, 通过理论证明ABC策略的有效性, 并将其应用于目前最高效的单一化模型算法MARCO和双模型算法MARCO-MAM, 在标准测试用例下的实验结果表明, 该策略可以有效地对搜索空间进行进一步剪枝, 从而提高MUS的枚举效率.     

极小布尔不可满足子式的提取算法

研究了极小布尔不可满足子式的提取算法，它分为近似算法和精确算法两种．文中就精确算法提出了局部预先赋值的优化方案，并且在理论上证明了该算法的正确性；通过实验显示了此算法可以获得更高的效率．通过模拟实验观察到，利用完法计算法进行近似提取的一个有趣现象，即随着公式密度的增加，算法的提取误差会趋于下降．     

合取范式3可满足问题的局部搜索近似算法

合取范式最大可满足问题是理论计算机科学的核心问题.局部搜索被许多求解实践证明是解答合取范式最大可满足问题十分有效的方法,但未见关于局部搜索算法解答该问题性能分析的结果.文中讨论最大3可满足问题(Max-(3)-Sat)的局部搜索算法并分析算法性能.证明Max-(3)-Sat问题的一位跳变局部搜索算法的近似性能比为4/3;证明一位跳变局部搜索后跟有条件全体跳变算法,解答Max-(3)-Sat问题的近似性能比为5/4.设计一位跳变加全体跳变的新局部搜索算法,证明新算法解答Max-(3)-Sat问题的近似性能比为8/7.将8/7-近似局部搜索算法推广为解答Max-(k)-Sat问题的局部搜索算法,证明算法的近似性能比为(2k+2)/(2k+1),k≥4.设计解答Max-(k)-Sat问题的两位跳变局部搜索算法,证明两位跳变局部搜索算法的近似性能比为1+1/(2k+1+k(k-1)/(n-k)),k≥4.局部搜索算法经多次运行可进一步提高求解性能.文中结果显示,局部搜索算法在合取范式最大可满足问题求解实践中表现出高性能,有其必然性.     

一个求解结构SAT问题的高效局部搜索算法

逻辑表达式可满足性(SAT)问题是第一个被证明的NP完全问题.它也是解决人工智能和计算理论中许多实际问题的基础.人们发现,对于某些类型的SAT问题,局部搜索算法要比一些传统的算法(例如Davis-Putnam过程)更为有效.在本文中,我们主要讨论如何用局部搜索算法求解结构SAT问题.我们对一个典型的局部搜索算法GSAT+walk做了改进与扩展.首先,我们除去了GSAT+walk中GSAT部分的"平移";其次,我们给每一个子句赋权,并在GSAT+walk的搜索过程中动态地调整子句的权.文中给出的实验结果表明改进后的新算法对于求解结构SAT问题非常有效.     

约束满足问题的局部一致性维护理论与方法

人工智能与计算机科学中的许多问题都可视为约束满足问题,为了简化问题的求解,常采用局部一致性方法减小搜索空间。本文首先介绍与分析了着眼于全局一致性的局部处理的理论与方法,以及尽可能消除回溯因素的局部一致性方法,最后给出了一种在减少局部一致性维护代价上优于已有方法的新算法。     

利用近似解加速求解SAT问题的启发式完全算法

结合DPLL完全算法能够证明可满足性(SAT)问题的不可满足性和局部搜索算法快速的优点,提出利用近似解加速求解SAT问题的启发式完全算法.首先利用局部搜索算法快速地得到一个近似解,并将该近似解作为完全算法的初始输入,用于其中分支变量的相位决策.该算法引导完全算法优先搜索近似解所在的子空间,加速解决器找到可满足解的过程,为SAT问题的求解提供了一种新的有效途径.实验结果表明,该算法有效地提高了决策的精度和SAT解决器的效率,对很多实例非常有效.     

基于父子等价剪枝策略的最大频繁项集挖掘

在传统剪枝策略中,具有相同事务集的父子结点搜索空间没有充分剪枝,效率较低.为此,提出父子等价的剪枝策略.采用深度优先搜索集合枚举树,对于父子结点中具有相同事务集的搜索空间进行剪枝,有效地缩小搜索空间,减少频繁项计算的次数,给出基于该剪枝策略的最大频繁项集挖掘算法.实验结果表明,该算法可缩短同一支持度下的最大频繁项集挖掘时间.     

基于互补概念和搜索图的MUPS求解优化方法

本体调试是人工智能中非标准推理任务之一,对于本体工程具有很重要的意义.本文结合互补概念与基于术语集的搜索图提出极小不可满足子术语集求解的优化方法.首先,通过判断扩展的术语集是否包含互补概念,确定该子术语集是否需要进行概念可满足性检测,可以有效减少推理机的调用次数.接着,根据术语集扩展过程构造一个术语集搜索图,分别采用宽度优先搜索和深度优先搜索策略快速查找不可满足子术语集.该优化方法一方面减少了待测子术语集的规模,另一方面提高了查找不可满足子术语集对应的节点的查找效率.最后,实现了本文给出的各类优化算法并与现有的黑盒优化算法进行了比较.实验效果表明,本文方法从推理机调用次数和待测术语集规模方面均优于现有的MUPS求解方法,能够有效提高求解术语集MUPS的效率.     

基于Grover算法的图着色问题求解

Grover量子搜索算法是针对非结构化搜索问题设计的著名量子算法，可用于解决图着色、最短路径排序等问题，也可以有效破译密码系统。图着色问题是最著名的NP-完全问题之一，文中首先将图着色问题转化为数学上的无向图；然后采用布尔表达式将其转换为布尔可满足性问题，介绍了量子线路图解决布尔表达式的步骤原理以及图着色问题向布尔可满足性问题的转换过程；最后在IBMQ云平台上，对三节点的2-着色问题以及4-着色问题进行模拟仿真。实验结果验证了使用Grover算法求解图着色问题的可行性，在搜索空间为8的2-着色问题和搜索空间为64的4-着色问题中，分别以近82%和97%的成功概率搜索到目标项。文中使用Grover算法解决了4-着色问题，拓展了该算法在此问题领域上的实验规模，且改进了现有实验的量子线路，使量子位成本更低，结果的成功率更高，展示了Grover算法在大型搜索问题中显著的加速效果。     

一类布尔方程组的可满足性阈值研究*

以一类布尔方程组形式的NP问题可满足性阈值估计为研究目的,通过将高斯消去算法与摘叶算法相结合的方法给出了一种求解该问题的完全算法,并通过不同参数条件下对大量随机实例进行数值实验得到了原问题可满足性阈值的算法估计值。所得研究结果不仅首次给出了该问题的可满足性阈值估计,而且可以作为相关启发式完全算法的设计依据。     

具有约束条件的组合测试用例集的构建方法

针对如何为存在约束条件的软件系统生成尽可能小的组合测试用例集问题,提出了基于组合测试算法的约束组合测试法.该方法是对待测系统中的约束条件进行处理,将约柬条件先转化为合取范式再转化为布尔表达式的形式.利用布尔可满足性求解器进行求解,找出满足约束条件的约束组合测试用例.最后运用AETG-SAT算法得到较优的组合测试用例集,并通过实验表明了AETG-SAT算法的优越性.     

非布尔问题系统求解算法的一种新思路

非布尔变量的约束可满足性问题有两种较为普遍的求解方法,系统求解算法就是其中的一种。该算法的基本思想是对变量的值域空间逐个进行搜索,其优点是只要问题有解,算法就一定能给出正确答案。在最不理想的情况下,该算法时间复杂度为变量数目的指数级。该文给出一种新策略,虽然在本质上仍然是在值域空间中进行搜索,但在实现过程中根据启发式思想,有针对性地设置搜索的优先次序。它的目的是尽可能的缩小搜索空间的范围,因为实践证明算法计算过程中许多状态不需要搜索。几个实例证明该策略在许多情况下有较为令人满意的性能。同时该文还给出相应的理论分析。     

一种子句重构的增强Tableau算法

利用非循环定义的概念可展开的特性,提出一个基于子句重构的增强Tableau算法.采用最简洁的概念合取子句代替原来的子概念集对完整树/图上的结点进行标记,并设计一组推理规则以构建这样的完整树/图,从而消除传统Tableau算法中的∩-规则、∪-规则所带来的概念描述重复.因而在非循环定义概念可满足性判定问题上,空间性能有明显提高.此外,虽然文中只提供针对SI语言的规则和证明,可是这种处理思路同样适用于其它描述逻辑语言,因而具有一定的推广价值.     

约束满足混合算法求解并行机Job-Shop调度问题

分析并行机Job-Shop调度问题的特点并建立其约束满足优化模型,结合约束满足与变邻域搜索技术设计了一个求解该问题的混合优化算法。该算法采用变量排序方法和值排序方法选择变量并赋值,利用回溯和约束传播消解资源冲突,生成初始可行调度,然后应用局部搜索技术增强收敛性,并通过结合问题特点设计的邻域结构的多样性提高求解质量。数据实验表明,提出的算法与其他两种算法相比,具有一定的可行性和有效性。     

面向高维连续行动空间的蒙特卡罗树搜索算法

蒙特卡罗树搜索(Monte Carlo Tree Search,MCTS)在低维离散控制任务中取得了巨大的成功.然而,在现实生活中许多任务需要在连续动作空间进行行动规划.由于连续行动空间涉及的行动集过大,蒙特卡罗树搜索很难在有限的时间内从中筛选出最佳的行动.作为蒙特卡罗树搜索的一个变种,KR-UCT(Kernel Regression UCT)算法通过核函数泛化局部信息的方式提高了蒙特卡罗树搜索在低维连续动作空间的模拟效率.但是在与环境交互的过程中,为了找出最佳的行动,KR-UCT在每一步都需要从头进行大量的模拟,这使得KR-UCT算法仅局限于低维连续行动空间,而在高维连续行动空间难以在有限的时间内从行动空间筛选出最佳的行动.在与环境交互的过程中,智能体可以获得环境反馈回来的信息,因此,为了提高KR-UCT算法在高维行动空间的性能,可以使用这些反馈信息剪枝树搜索过程来加快KR-UCT算法在高维连续行动空间的模拟效率.基于此,文中提出了一种基于策略-价值网络的蒙特卡罗树搜索方法(KR-UCT with Policy-Value Network,KRPV).该方法使用策略-价值网络保存智能体与环境之间的交互信息,随后策略网络利用这些信息帮助KR-UCT算法剪枝KR-UCT搜索树的宽度;而价值网络则通过泛化不同状态之间的价值信息对蒙特卡罗树搜索在深度上进行剪枝,从而提高了KR-UCT算法的模拟效率,进而提高了算法在高维连续行动任务中的性能.在OpenAI gym中的4个连续控制任务上对KRPV进行了评估.实验结果表明,该方法在4个连续控制任务上均优于KR-UCT,特别是在6维的HalfCheetah-v2任务中,使用KRPV算法所获得的奖励是KR-UCT的6倍.     

基于多样性SAT求解器和新颖性搜索的软件产品线测试

软件产品线测试是一项非常具有挑战性的工作. 基于相似性的测试方法通过提升测试集的多样性以达到提高测试覆盖率和缺陷检测率的目的. 因其具有良好的可拓展性和较好的测试效果, 目前已成为软件产品线测试的重要手段之一. 在该测试方法中, 如何产生多样化的测试用例和如何维护测试集的多样性是两个关键问题. 针对以上问题, 提出一种基于多样性可满足性(SAT)求解器和新颖性搜索(novelty search, NS)的软件产品线测试算法. 具体地, 所提算法同时采用两类多样性SAT求解器产生多样化的测试用例. 特别地, 为了改善随机局部搜索SAT求解器的多样性, 提出一种基于概率向量的通用策略产生候选解. 此外, 为同时维护测试集的全局和局部多样性, 设计并运用两种基于NS算法思想的归档策略. 在50个真实软件产品线上的消融和对比实验验证多样性SAT求解器和两种归档策略的有效性, 以及所提算法较其他主流算法的优越性.