检索结果-内蒙古大学图书馆

作者：毕舜阳西安电子科技大学

学位级别：硕士

可满足性问题(Boolean Satisfiability Problem),又称SAT问题,是指对于一个给定的合取范式(Conjunctive Normal Form),能否找到一组变量的赋值使得该式成立。该问题因在集成电路设计自动化的形式验证和自动测试模式生成(ATPG)问题中被... 详细信息

可满足性问题(Boolean Satisfiability Problem),又称SAT问题,是指对于一个给定的合取范式(Conjunctive Normal Form),能否找到一组变量的赋值使得该式成立。该问题因在集成电路设计自动化的形式验证和自动测试模式生成(ATPG)问题中被广泛应用,而成为近年来的研究热点。求解SAT问题的算法分为两种:完备算法和不完备算法,完备算法因为具有可证明结果不满足的特性,因此适合应用在形式验证和ATPG问题中。cdcl算法(Conflict-Driven Clause Learning)是目前完备算法中最高效的算法框架。cdcl算法框架的主要原理是利用分支启发策略选择一个变量赋值,赋值的变量进行布尔约束传播,产生冲突后得到学习子句,之后的传播会通过学习子句避免相同的冲突,进而完成所有变量的赋值。cdcl算法成功的原因之一在于其采用了学习子句策略,可以有效地缩小算法的搜索空间,实现高效的求解。因此本文的研究工作集中在学习子句的优化策略上,主要包括以下四方面: 1、本文通过实验测试观测到,传统的学习子句评价标准——LBD标准,在近几年提出的分支启发(LRB策略)下产生了评价误差。在具体的实验结果中,出现评价误差的测试例子占到总测试例子的48.9%。对此,分析其误差产生的原因可能是LRB分支启发下更频繁的变量更新导致的; 2、针对LBD标准出现的评价误差和导致其误差的潜在原因,本文提出了一种新的学习子句评价标准——基于冲突频率和LBD值的混合标准(HEC标准)。HEC标准采用指数加权平均的处理方式巧妙地将冲突频率和LBD值结合起来,可以动态地反映学习子句的质量。在给出HEC标准的算法实现后,本文对其进行了初步的验证,结果显示,采用该标准的学习子句使用率要比LBD标准高32.8%;在应用到求解器上时,除了在LRB分支启发下有较好的提升之外(比原算法多解决5个例子),在传统的VSIDS分支启发下也有高效的表现(比原算法多解决5个例子); 3、基于BCP传播的次数远大于冲突分析的次数的事实,本文通过一组实验观测到,学习子句在BCP传播的速度是冲突分析中的20倍以上,因此考虑将学习子句的更新添加到BCP传播中,其目的是为了加快学习子句的更新速度,更有利于筛选出高质量的学习子句。在经过测试对比后结果显示,基于BCP传播的更新方式可以加快学习子句的更新速度,应用在求解器上比冲突分析中的更新多解决9个测试例子; 4、本文提出了一种新的学习子句删除算法框架,并将前两部分的工作——BCP传播的更新方式和HEC标准结合起来,整合在学习子句删除的框架中,实现了一种新的学习子句删除算法。两组不同分支启发下的测试和一组ATPG电路中的测试都显示,应用该算法的求解器求解提升率都在约15%以上。

关键词： cdcl算法学习子句 LBD标准 HEC标准分支启发策略

来源：评论

学校读者我要写书评

暂无评论

基于变量特征的cdcl算法中分支策略优化研究

基于变量特征的CDCL算法中分支策略优化研究

引用

作者：艾森阳西南交通大学

学位级别：硕士

可满足性问题(Satisfiability Problem,SAT问题)是数理逻辑中的一个经典问题,也是自动推理的一个重要研究方向。在理论应用方面,许多的NPC(Non-deterministic Polynomial Complete)问题如图着色问题、欧拉回路问题和旅行商问题等,都可... 详细信息

可满足性问题(Satisfiability Problem,SAT问题)是数理逻辑中的一个经典问题,也是自动推理的一个重要研究方向。在理论应用方面,许多的NPC(Non-deterministic Polynomial Complete)问题如图着色问题、欧拉回路问题和旅行商问题等,都可以转化成SAT问题进行求解。在实际应用方面,如计算机辅助设计与制造领域和人工智能领域中的一些现实问题,通过逻辑形式化方法可以转化为SAT问题进行求解。另外,形式化验证中的一个不可缺少环节就是逻辑公式可满足性的判定。因此,研究SAT问题不仅具有重要的理论价值而且具有广泛的应用前景。目前,求解SAT问题的算法主要分为完备算法和不完备算法两种。完备性算法主要基于穷举和回溯思想,不完备算法主要基于局部搜索思想。基于DPLL(Davis Putnam Logemann Loveland)算法发展而来的cdcl(Conflict driven clause learning)算法是具有代表性的完备算法,也是目前求解SAT问题的一种主流算法。它的求解结构主要包括预处理、子句学习、分支决策和重启等模块。在cdcl算法求解框架中,随着搜索的进行求解器会不断地记录产生冲突的原因,能够避免后续搜索过程进入相同的冲突空间。研究结果表明,基于冲突学习的能力是cdcl算法求解高效的关键因素。在cdcl算法框架下,针对基于冲突分析的分支决策环节,本文主要做了以下两方面的工作:1.为减少求解器在分支决策环节出现过多随机赋值的现象,本文在VSIDS(Variable State Independent Decaying Sum)分支策略的基础上,融入了冲突次数和变量所在子句的LBD值两种特征,提出了一种基于变量特征的分支策略,称为BVA(Breaking the Balance of Variable Activity)分支策略。BVA分支策略在分支决策过程中不改变变量活性值的整体增长趋势,只是小幅度地提升了部分变量的活性值。这样不仅保留了VSIDS分支策略的原有优势,而且更有利于减少VSIDS分支策略的随机性,使分支变量的选择更准确。2.基于上面的工作,将BVA分支策略形成算法,嵌入到著名的求解器Glocose4.1和2018年国际竞赛冠军求解器Maple＿LCM＿Dist＿Chrono BT中,分别形成了Glocose4.1+BVA求解器和Maple＿LCM＿Dist＿Chrono BT+BVA求解器。在实验部分,实验选择2017-2019年的竞赛例作为测试例。通过实验对比分析表明改进的两个求解器在求解效率和求解能力方面均优于原版求解器,尤其在求解不可满足性问题上表现出明显的优势。

关键词： SAT问题 DPLL算法 cdcl算法分支策略

来源：评论

学校读者我要写书评

暂无评论

基于启发式策略的恰当可满足性问题算法优化及应用研究

基于启发式策略的恰当可满足性问题算法优化及应用研究

引用

作者：赵星宇北方民族大学

学位级别：硕士

约束可满足问题(Constraint Satisfaction Problem,CSP)是理论计算机科学中重要的问题,可满足性问题(Satisfiability Problem,SAT)是典型的CSP问题。作为SAT问题的子类,恰当可满足性问题(Exact Satisfiability Problem,XSAT)是指存在一组赋值,使公式中每个子句中仅有一个文字为真的SAT问题。现实中许多实际应用问题都可以归纳为XSAT问题进行求解。目前针对该问题的研究多集中在相变、精确算法的上下界等理论研究层面,而对其问题的求解算法研究较少。因此相应的求解算法值得探索。在求解SAT问题的算法中,优秀的启发式策略能够提升算法的性能。为此,本文将不同的启发式策略分别引入到随机局部搜索算法和完备性算法中求解XSAT问题,并提出了一种大规模XSAT问题实例的转化方法。具体地讲,本文的主要工作如下: (1)针对目前随机局部搜索算法求解XSAT问题的研究空缺,将一种恰当不可满足计分值与防重复选择翻转变元的启发式策略引入到随机局部搜索算法中,提出了一种能在多项式时间内生成较好初始赋值的预处理方法,探究了基于概率的随机局部搜索算法在不同参数取值时对求解性能的影响。实验结果表明,在随机生成的实例中,加入启发式策略的算法,较其它求解SAT问题的算法,能有效减少翻转次数与求解时间;加入预处理方法的算法,能够进一步提升随机局部搜索算法的求解效率。 (2)针对随机局部搜索算法在求解超大规模实例容易不收敛的特点,改进了一种完备性算法,提升了求解大规模XSAT的能力。首先提出了一种大规模XSAT问题实例的规约转化方法,通过对实例性质的分析,改进了完备性算法中的动态启发式变元决策策略,将一种防止选择决策变元陷入局部最优的权重策略引入到冲突驱动子句学习(Conflict-Driven Clause Learning,cdcl)算法中。实验结果表明,在转化后产生的实例集上,较基于其它启发式策略的cdcl算法,改进后的启发式策略能降低大部分实例的求解时间,提升了算法的求解效率。 (3)基于改进后的随机局部搜索算法和cdcl算法,设计开发了求解XSAT问题的可视化求解器。

关键词：恰当可满足性问题启发式策略随机局部搜索算法 cdcl算法规约转化

来源：评论

学校读者我要写书评

暂无评论

基于图注意力网络的SAT问题求解算法研究

基于图注意力网络的SAT问题求解算法研究

引用

作者：张桁恺河南理工大学

学位级别：硕士

命题可满足性问题,即SAT问题是计算机科学中最基本的问题之一。库克在1971年的研究中表明该问题是NP完全问题,这意味着其它所有NP问题都可以在多项式时间内转化为SAT问题。在实际生活中,SAT问题有着广泛的应用,如硬件和软件验证、测试... 详细信息

命题可满足性问题,即SAT问题是计算机科学中最基本的问题之一。库克在1971年的研究中表明该问题是NP完全问题,这意味着其它所有NP问题都可以在多项式时间内转化为SAT问题。在实际生活中,SAT问题有着广泛的应用,如硬件和软件验证、测试模式生成、计划、调度和组合优化问题,都是通过构建一个适当的SAT问题,然后调用一个SAT求解器来解决的。 SAT问题实例具有非常丰富的泛型和特定的结构特征,这些结构通常在大多数经典的特征提取技术过程中丢失。由于表征学习领域的新进展,特别是几何深度学习,使用图神经网络在可满足性判定方面取得了不错的进展。目前图神经网络在SAT问题上的应用可以归为两类。一种是建立一个端到端的模型,输入一个问题实例并直接预测可满足性或获得解决方案。另一类是将神经网络与传统求解器相结合,试图提高一些关键启发式方法的有效性。本文针对这两类应用分别进行研究,主要工作内容如下: (1)首次使用图注意力网络来解决命题逻辑问题,并提出了GAT-SAT,一个预测随机SAT问题满足性的新模型。该模型在随机SAT问题和随机3-SAT问题数据集上的预测准确性一直优于现有的方法。GAT-SAT在同样没有人工特征的条件下,仅用别的方法一半的迭代次数就可以达到更高的精度,而且只需要类似的监督条件。本文还分析了GAT-SAT是如何做到这一点的,在图形注意力网络学习了注意力分数之后,对文字和子句节点的特征向量给予不同的权重。在预测可满足性时,GAT-SAT专注于重要节点的特征特征向量。实验结果表明,图注意力网络可以学习和捕捉命题逻辑问题的关键节点的不变结构特征,预测准确性始终领先其他图神经网络的方法。 (2)训练了一个简化的GAT-SAT架构,SGAT-SAT,通过直接预测真实世界SAT问题所有变量的注意力分数,从而指导现代求解器的决策变量启发式策略。本文改进了两个高性能的SAT求解器,定期对SAT问题查询修改后的GAT-SAT,并根据其预测结果,即该变量对于这个SAT问题的重要性,一次性设置所有变量的注意力分数,并让两个现代求解器根据每个变量的注意力分数和活动分数综合选择决策变量。修改后的现代求解器在SATCOMP-2018的标准时间5000秒内解决的问题数量均超过了原版。当针对特定类别的问题进行专门训练时,结果提升更大。实验结果表明,GAT-SAT可以对高性能求解器解决实际问题提供有效的指导。本文有图13幅,表4个,参考文献89篇。

关键词：命题逻辑可满足性问题 cdcl算法深度学习图注意力网络

来源：评论

学校读者我要写书评

暂无评论

基于SAT的逻辑综合优化及映射后的性能分析

基于SAT的逻辑综合优化及映射后的性能分析

引用

作者：汤占玺济南大学

学位级别：硕士

现阶段针对逻辑综合算法的研究已经从启发式算法转向到了精确综合算法的研究,这一转变的本质在于将逻辑综合中的优化问题转化成布尔逻辑问题,然后利用SAT求解器对其进行求解。然而,在精确综合领域仍然存在一些问题,例如,在Vivado和原始Y... 详细信息

现阶段针对逻辑综合算法的研究已经从启发式算法转向到了精确综合算法的研究,这一转变的本质在于将逻辑综合中的优化问题转化成布尔逻辑问题,然后利用SAT求解器对其进行求解。然而,在精确综合领域仍然存在一些问题,例如,在Vivado和原始Yosys对相同案例进行综合对比的实验中,发现LUT、FDRE、CARRY、LDCE等资源利用方面,Yosys明显超过Vivado,这表明现阶段的精确综合算法在资源优化方面还存在改进空间。基于上述背景,本文开始对逻辑优化算法和工艺映射规则进行研究,并且做了以下三个方面的研究工作: 1.通过对VSIDS策略及其扩展策略EVSIDS策略的深入研究,本文在VSIDS策略的基础上引入了变量活跃度参数。在计算变量得分的过程中,本文进一步考虑了当前变量的决策层、冲突次数以及总冲突次数等因素,确保了相同冲突中不同变量的得分能够有所区分。结合这些改进,本文提出了一种基于活跃度及变量决策层的启发式变量选择策略,为cdcl算法加载新的启发式分支策略,将这一改进后的cdcl算法集成到ABC综合工具的Glucose2求解器中。通过Yosys命令,用户可以轻松调用ABC综合工具,并对测试案例进行测试。在对比分析Vivado、原始Yosys以及Yosys+AVSIDS对相同测试案例的综合结果后,改进后Yosys在LUT资源上平均减少了23.4%,在FDRE资源上平均减少了5.0%,在CARRY4资源上平均减少了7.2%。这一优化不仅大大降低了FPGA资源的消耗,还为后续布局布线阶段减少了面积和时间的消耗,从而提升了整体的综合效率。 2.根据对FPGA工艺映射概念和流程的系统研究,本文对Yosys中的工艺映射规则和部分映射库文件进行了优化。特别是针对Yosys的映射命令synth＿xilinx中涉及到的关于DSP、BRAM、BUFG等资源的工艺映射规则进行改进。同时,对Yosys映射库文件进行了优化,在映射库文件中添加了LDCE原语并修正了部分寄存器原语的格式。通过对VTR-benchmarks测试集的20个测试案例进行测试,测试结果显示BUFG资源成功映射,并且相对于Vivado的资源利用降低了15.5%。改进后Yosys相对于原始Yosys在LDCE资源利用方面平均减少了0.586%。 3.在对Yosys综合工具的使用过程中,发现对不同的测试案例进行综合需要重新构建新的包含Yosys命令的综合脚本,而且综合后的资源利用情况也无法直观的看到,所以本文认为设计一个基于Yosys的综合系统是有必要的。首先可以通过界面的形式对Verilog文件、约束文件进行添加,还可以通过本系统对不同的案例进行综合并且不需要重新构建Yosys脚本文件,可以清楚的看到源文件的各个模块并且可以设置顶层模块,另外在界面上也可以显示出综合后的资源使用情况,方便用户对测试案例进行对比分析。基于Yosys的综合系统的开发让使用者可以缩减学习Yosys命令的时间,也能减少使用过程中因为对Yosys命令不熟悉所导致综合出错次数,大大提高使用者的工作效率。

关键词： SAT 逻辑综合 cdcl算法工艺映射

来源：评论

学校读者我要写书评

暂无评论

基于分支策略与距离比删除策略的SAT问题求解算法研究

基于分支策略与距离比删除策略的SAT问题求解算法研究

引用

作者：王萌西南交通大学

学位级别：硕士

自然科学与社会科学中的许多问题均可转化成布尔可满足问题(Satisfiability Problem,SAT),并且SAT问题也是计算机以及人工智能等科学领域的核心问题之一。因此,随着计算机科学、智能信息的快速发展,为解决各种实际问题,研究SAT问题以及... 详细信息

自然科学与社会科学中的许多问题均可转化成布尔可满足问题(Satisfiability Problem,SAT),并且SAT问题也是计算机以及人工智能等科学领域的核心问题之一。因此,随着计算机科学、智能信息的快速发展,为解决各种实际问题,研究SAT问题以及其求解具有深刻意义。SAT问题中的算法主要分为完备算法和不完备算法,本文主要研究的是完备算法中的cdcl(Conflict Drive Clause Learning)算法。在cdcl算法基本求解过程中,分支过程以及子句学习过程是非常重要的两个阶段,对求解效率和求解速度都有很大的影响。而现在多数的改进算法在分支过程均未考虑整个算法过程中的其他阶段,所以求解结果未能达到最优。基于此,本文考虑冲突分析阶段对分支过程影响的同时,结合回溯以及重启两个阶段产生的影响,提出加权决策变量决策层的改进分支策略。新策略设计了新的变量得分函数,使其具有在分支过程能够更快的挑选出决策变量的优势,因此能减少后续冲突和重启次数,最终减少求解时间。对由新策略形成新的求解器进行试验测试,实验结果表明新分支策略具有优化的效果。另外,现在多数算法在子句学习过程评估学习子句质量均是将学习子句的长度、活跃度或者文字块距离(literal block distance,LBD)值作为评价标准,但少有考虑制定新的删除标准,基于此,本文考虑平衡LBD的值,提出文字块紧密度(literal block close,LBC)的概念,并将其与学习子句活跃度结合,形成基于距离比的学习子句删除策略。新策略能更有效地删除利用率低的学习子句,由此加强求解器的求解能力,增加求解例子个数,减少求解时间。对此策略形成新的求解器进行实验测试,结果表明新策略的求解能力更强。本文的主要研究工作如下:1、通过分析冲突、回溯和重启过程,根据变量作为决策变量的次数以及对其决策层加权,提出了新的变量得分计算函数方法,并提出了加权决策变量决策层(DVT)的策略,将DVT策略嵌入cdcl算法中并形成Glucose4.1+DVT求解器。采用SATLIB中的基准例以及2019年、2018年和2017年国际SAT竞赛Main Track组中的测试例进行实验测试,结果表明新求解器成功求解的平均总时长比原求解器缩短10%,成功求解出的测试例总个数相比原版求解器增加6个。2、由于冲突子句学习过程中会产生大量的学习子句,基于平衡子句LBD值的思想,提出文字块紧密度的概念以及距离比的学习子句删除(LBDR)策略,将此策略加入cdcl算法中,形成Glucose4.1+LBDR求解器。采用SATLIB中的基准例以及2019年、2018年和2017年国际SAT竞赛Main Track组中的测试例进行实验测试,结果表明新求解器成功求解时间比原求解器缩短12.5%,成功求解出测试例的总个数相比原版求解器增加14个。

关键词： SAT问题求解 cdcl算法决策变量决策层文字块密集度距离比的删除策略

来源：评论

学校读者我要写书评

暂无评论

SAT算法中基于回溯的分支和子句删除策略的研究

SAT算法中基于回溯的分支和子句删除策略的研究

引用

作者：沈雪西南交通大学

学位级别：硕士

布尔可满足性问题(Satisfiability Problem,SAT问题)是逻辑学中经典的判定问题,也被证明是一个NPC(Non-deterministic Polynomial Complete)问题。由于NPC问题能在多项式时间内相互转化,因此所有的NPC问题都能转换为SAT问题进行求解。此... 详细信息

布尔可满足性问题(Satisfiability Problem,SAT问题)是逻辑学中经典的判定问题,也被证明是一个NPC(Non-deterministic Polynomial Complete)问题。由于NPC问题能在多项式时间内相互转化,因此所有的NPC问题都能转换为SAT问题进行求解。此外,在实际应用中,如计算机辅助设计与制造、生物信息、人工智能等领域的许多问题都可转化为SAT问题进行求解。因此,快速求解SAT问题具有重要的研究价值。近几十年来,对SAT问题的研究已经取得了重大进展,特别是cdcl(Conflict Driven Clause Learning)算法的提出,使得求解器可以在几分钟内解决数十万变量和数百万个子句的工业实例。因此,本文的研究工作主要是以cdcl算法为算法框架,围绕分支变量决策和学习子句删除两方面进行了系统研究,在已有方法基础上提出了一些改进策略和新方法,并通过理论分析和实验进行了有效性验证。本文主要的研究工作如下:1.为解决求解SAT问题过程中分支决策效率不高的问题,本文在EVSIDS(Exponential Variable State Independent Decay Sum)分支策略的基础上,提出了基于二次奖励的分支启发式(Two Rewards Based Branching Heuristic,TRBH)策略。考虑到分支决策变量是在未赋值变量集中选取,针对在回溯期间转化为未赋值状态的变量,TRBH分支策略结合变量最近一次参与冲突分析的情况,再次给予这些变量一次奖励。通过二次奖励的方式可以增大最近一次参与冲突分析且未赋值的变量被选择为决策变量的可能性,以此改变决策变量的选择规则。2.为解决单一地利用LBD(Literals Blocks Distance)值来评估子句而导致子句利用率不高的问题。本文在LBD评估方法的基础上,增加了回跳层数(Back-Jump levels,BJL)的学习子句删除策略。该删除策略利用学习子句的回跳层数来评估学习子句的质量,因为学习子句回跳层数越大,在搜索过程中对二叉树的剪枝能力越强,也就是说可以加大剪枝效率,加快搜索速度,从而减少求解器的求解时间。3.将TRBH分支策略和BJL删除策略分别嵌入到Glucose4.1中,分别形成了求解器Glucose4.1+TRBH和Glucose4.1+BJL,然后实验测试了2017～2019的SAT竞赛实例。在分支策略实验中,对比Glucose4.1+TRBH和Glucose4.1两个求解器的求解个数、平均用时和决策次数,实验结果表明新提出的分支策略能有效减少分支决策次数,提高SAT求解器的求解效率。在删除策略实验中,对比Glucose4.1+BJL和Glucose4.1两个求解器的求解个数以及平均用时,实验结果表明BJL删除策略比单一的LBD删除策略更加科学合理。

关键词：可满足性问题 cdcl算法分支决策学习子句删除

来源：评论

学校读者我要写书评

暂无评论

基于cdcl与遗传算法的SAT求解器算法的研究

基于CDCL与遗传算法的SAT求解器算法的研究

引用

作者：臧婉君西安电子科技大学

学位级别：硕士

可满足性问题(SAT问题)是计算机科学领域中的核心基础问题,是寻找并确定一组真值指派作为以合取范式形式(CNF)表示的给定布尔约束公式的解决方案的问题。解决方案是一组布尔真值指派,可以对原公式进行真值评估。SAT问题具有广泛的应用领... 详细信息

可满足性问题(SAT问题)是计算机科学领域中的核心基础问题,是寻找并确定一组真值指派作为以合取范式形式(CNF)表示的给定布尔约束公式的解决方案的问题。解决方案是一组布尔真值指派,可以对原公式进行真值评估。SAT问题具有广泛的应用领域,包括计算机辅助设计,人工智能,路线规划等。可以将各种电子设计自动化(EDA)应用程序(如等效性检查,模型检查,测试模式生成,布局和路线)定义或转化为SAT问题。至今为止国内外许多研究都致力于开发高度可扩展和高效的SAT求解器。SAT问题是NP完全问题,如果该问题的解是存在的,SAT求解器会尝试为原公式找到解决方案。尽管在许多实际情况下可以通过最先进的SAT求解器在合理的计算资源消耗内去求解很多问题,但由于SAT的NP完全性,在很多情况下求解工作仍然非常困难。本论文提出了一种基于增强型遗传算法(GA)和冲突驱动子句学习算法(cdcl)的SAT完备混合求解器。这个求解器是一个完备求解器,可以在SAT问题的求解工作上得到一个完整的解决方案,或者证明解决方案不存在(即原问题是不可满足(UNSAT)问题),它可以在所有三类SAT实例测试集(应用类,随机类和特制类)上都表现得相对好。这种求解器的主要混合方法是使用结合局部搜索技术的遗传算法作为求解器不完备部分的算法,并且集成了 cdcl算法的求解器作为互补的完备部分。其结合了预处理,布尔约束传播,冲突分析,子句学习,边界点等求解技术,并考虑了 GA求解阶段中问题规模(变量数与子句数的比例)与遗传参数的具体设置方式。这种混合机制是让两个部分相互指导共同求解,从而找到原问题的解决方案,并且能够避免单纯依赖某一部分求解器来独自寻找解决方案的过程的出现。通过与原基于cdcl算法或GA算法的SAT求解器的一系列实验数据进行比较,本文实现的混合求解器是完备求解器,可以高效地解决不同类别的SAT问题,比现存的常用求解器具有更快的求解速度并在运行过程中消耗合理的较多内存,且测试集的问题规模由小到大是十分广泛的。特别是针对基于cdcl算法的求解器Minisat不容易求解或限定时间内无法判定求解结果的某些测试集上,本文提出的求解器求解效率更高,求解时间大幅度减少。与Minisat求解器相比,本文提出的混合求解器在最佳实例上的平均求解时间为0.56倍。当在GA部分中依照问题规模的不同而设置适当的遗传算子组合机制和参数时,实验结果显示出此求解器能够同时减少求解时间并降低内存消耗量。在本研究中问题规模最大的测试例上,此求解器平均求解时间为前者的0.76倍,且平均内存用量减少了 38%。经过大量针对不可满足的UNSAT测试集的对比实验结果得出,此求解器不仅能够在限定求解时间内Minisat无法证明不可满足性的测试集上成功求解,更能够比Minisat在更短的求解时间内得出解决方案,体现出了不可满足性证明方面更为优秀的求解能力,并且展示了应用了 GA而不是单一地应用SLS作为混合求解器不完备算法部分的优势。本文所提出的完备求解器充分地结合了 GA和cdcl两者的优势,展示出在更多的SAT问题上可表现出更佳性能的潜力,更体现了在后续科研方向上优化意义和在实际应用问题上的应用前景。

关键词：可满足性问题遗传算法 cdcl算法 SAT混合求解器

来源：评论

学校读者我要写书评

暂无评论

基于变量混合特征的分支启发式策略

引用

计算机系统应用 2020年第3期29卷 200-205页

作者：艾森阳宋振明沈雪西南交通大学数学学院成都611756 西南交通大学系统可信性自动验证国家地方联合工程实验室成都611756

先进的SAT求解器能够通过有效的分支启发式策略解决大型应用实例.目前VSIDS策略是最具有代表性的基于冲突分析的分支策略,它因其稳健性而被广泛使用,但在每次冲突分析中其判定变量活性的增量方式过于单一.针对此问题,本文提出了一种基... 详细信息

先进的SAT求解器能够通过有效的分支启发式策略解决大型应用实例.目前VSIDS策略是最具有代表性的基于冲突分析的分支策略,它因其稳健性而被广泛使用,但在每次冲突分析中其判定变量活性的增量方式过于单一.针对此问题,本文提出了一种基于变量混合特征的分支启发式算法,目的是充分地利用参与冲突分析的变量所携带的不同信息特征来区分变量,来进一步指导变量活性增长.并将所提出的分支策略算法嵌入到Glucose4.1中形成求解器Glucose4.1+MFBS,通过对比测试,实验结果表明改进的分支算法比原本的VSIDS策略,具有一定的优势,求解明显个数增加.

关键词： SAT问题 cdcl算法分支启发式冲突分析学习子句

来源：评论

学校读者我要写书评

暂无评论

基于cdcl求解SAT问题的启发式策略研究

基于CDCL求解SAT问题的启发式策略研究

引用

作者：陈秀兰西南交通大学

学位级别：硕士

在逻辑问题中,布尔可满足性问题(即SAT问题)一直广受人们的关注。SAT问题是确定以合取范式(CNF)的形式给出的命题逻辑公式是否具有对其变量的一组布尔真值赋值,使得该公式是可满足的,或者证明它不可满足。SAT问题在算法时间复杂度上是... 详细信息

在逻辑问题中,布尔可满足性问题(即SAT问题)一直广受人们的关注。SAT问题是确定以合取范式(CNF)的形式给出的命题逻辑公式是否具有对其变量的一组布尔真值赋值,使得该公式是可满足的,或者证明它不可满足。SAT问题在算法时间复杂度上是首个被证明的NP完全问题。目前,SAT问题是许多领域的研究热点,如定理证明、自动推理、模型检查、电子设计自动化、计算机辅助设计等。因此,有关SAT问题的研究,不仅在理论方面意义重大,而且在实际应用中也有着巨大的价值。不完备算法和完备算法是解决SAT问题的两类主要算法。不完备算法主要基于随机局部搜索的思想,完备算法主要基于回溯搜索的思想。完备算法的优点在于一定能够判定SAT问题的可满足性。目前,最流行的完备算法是cdcl算法,本文则是基于cdcl算法结构展开研究,主要取得了如下研究成果:1.在EVSIDS和ACIDS算法的启发下,提出了一种基于动态奖励的分支启发式算法,也称为DRB算法。每当冲突发生时,DRB算法通过综合考虑变量决策层、冲突层、冲突次数和变量冲突频率进行活性分数更新,从而引导求解器的分支变量决策。2.根据学习子句的LBD值引入了层次差,用于评估LBD值相同的学习子句之间的质量差异。基于此,提出了基于层次差的学习子句删除启发式策略,也称为LDCR策略,从而指导求解器的子句数据库管理。3.将DRB算法和LDCR策略嵌入到Glucose 3.0与MapleLCMDistChronoBT求解器中,得到了6个新的SAT求解器。主要做了两类实验,实验一是基于Glucose 3.0的改进求解器与Glucose 3.0之间的对比实验,选择2015年、2016年和2017年三年的SAT竞赛实例进行测试;实验二是基于2018年冠军求解器MapleLCMDistChronoBT的改进求解器与MapleLCMDistChronoBT之间的对比实验,选择2018年的SAT竞赛实例进行测试。将改进求解器的测试结果与原来的求解器进行对比分析,实验结果表明改进求解器的性能均高于原来的求解器。因此,本文提出的两种新的启发式策略可以有效改进已有的cdcl算法框架,进而提升求解器的性能。

关键词： SAT问题 cdcl算法分支启发式策略学习子句删除启发式策略 DRB算法 LDCR策略 cdcl SAT求解器

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：