检索结果-南通市图书馆

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

学位级别：硕士

可满足性问题(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算法中分支策略优化研究

基于变量特征的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年的竞赛例作为测试例。通过实验对比分析表明改进的两个求解器在求解效率和求解能力方面均优于原版求解器,尤其在求解不可满足性问题上表现出明显的优势。

来源：

同方学位论文库评论

基于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问题上可表现出更佳性能的潜力,更体现了在后续科研方向上优化意义和在实际应用问题上的应用前景。

来源：

同方学位论文库评论

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

引用

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

学位级别：硕士

约束可满足问题(Constraint Satisfaction Problem,CSP)是理论计算机科学中重要的问题,可满足性问题(Satisfiability Problem,SAT)是典型的CSP问题。作为SAT问题的子类,恰当可满足性问题(Exact Satisfiability Problem,XSAT)是指存在一... 详细信息

约束可满足问题(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问题的启发式策略研究

基于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问题算法的研究

引用

作者：吴小瑞西南交通大学

学位级别：硕士

SAT问题是判断命题逻辑公式可满足性,也是NP完全问题之首,在计算机科学和人工智能等领域有重要的理论和应用价值,成为了这些领域的一个热点研究问题。长期以来,人们对SAT问题的求解进行了深入研究,提出了很多求解SAT问题的算法,其中最... 详细信息

SAT问题是判断命题逻辑公式可满足性,也是NP完全问题之首,在计算机科学和人工智能等领域有重要的理论和应用价值,成为了这些领域的一个热点研究问题。长期以来,人们对SAT问题的求解进行了深入研究,提出了很多求解SAT问题的算法,其中最流行的要数cdcl算法。基于cdcl算法,有许多的求解器被开发出来,如Chaff、zChaff、Minisat、Glucose、Lingeling等著名求解器。这些求解器都是通过对cdcl算法的变量决策、冲突分析、子句学习、回溯回退等主要部分进行不断地替换和调整而来。本文着重研究了 cdcl算法的决策过程,也对变量决策过程进行改进。在决策过程中考虑了子句长短不一的问题,采用优先满足短子句的思想,利用单子句的蕴含原理和满足较多的短子句方法,尽可能早的产生冲突或减少冲突的产生,提高算法求解SAT问题的效率。基于cdcl算法结构框架,对算法做了相应部分的替换,主要的研究工作如下:1.基于优先满足短子句的思想,依据子句固有的结构信息,满足较多的子句,尽可能减少一些冲突的产生,提高算法求解SAT问题的效率,首先以在子句集中出现频率较多且大多出现在短子句中的变量作为选择前提,结合子句的长度,给出变量在子句中的平均长度的概念及一些相关的性质;然后将变量在子句中的平均长度,与变量出现的次数相联系,设计变量权重的计算函数;最后提出一种初始变量决策策略。2.依据子句长度在决策过程中的影响,以短子句为出发点,为了能够发现较多的单子句,采用单子句的蕴含原理,尽可能早地发现冲突或避免一些冲突的产生,提高算法求解SAT问题的时间效率,首先以生成单子句为目的,结合子句的长度,构造子句权重的计算函数;然后提出一种新的分支变量选择策略。3.基于初始变量选择策略和分支变量选择策略形成两种新算法,在cdcl算法结构框架上分别做了一些相应部分的改进,集成VW-SAT求解器和CW-SAT求解器,并进一步通过2015年SAT竞赛中的竞赛例和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个。

来源：

同方学位论文库评论

基于cdcl求解器的分支策略和删除策略的研究

基于CDCL求解器的分支策略和删除策略的研究

引用

作者：刘姚西南交通大学

学位级别：硕士

SAT问题是计算机科学理论和人工智能中的著名问题。NP完全问题(NP-complete,NPC)排在千禧年七大难数学问题之首,许多NP完全问题都可以在多项式时间内转换为SAT问题进行求解。SAT问题广泛应用于数学定理证明、计算机软件与理论、工程技... 详细信息

SAT问题是计算机科学理论和人工智能中的著名问题。NP完全问题(NP-complete,NPC)排在千禧年七大难数学问题之首,许多NP完全问题都可以在多项式时间内转换为SAT问题进行求解。SAT问题广泛应用于数学定理证明、计算机软件与理论、工程技术、软件验证以及逻辑电路等价性验证等多个领域。因而SAT问题一直是国内外学者关注的热点问题,设计并实现求解SAT问题的高效算法具有重要的钻研意义和应用远景。DPLL求解器开创了求解SAT问题的先河,但其算法自身的回溯机制对大规模问题的求解有一定程度的制约性。为了提升DPLL算法的求解效率,国内外学者们进行了大量的研究,添加了一些关键技术。例如启发式分支策略、基于冲突分析和子句学习、非时序回溯、学习子句的删除和周期性重启等,形成了当前最流行的cdcl(Conflict-Driven-Clause-Learning,cdcl)求解器。基于cdcl算法结构,本文做了以下研究工作:一、借鉴VSIDS策略及其延伸策略的思想,研究变量的决策层和变量参与冲突的冲突次数对分支决策阶段的影响,在此基础上提出一种改进的启发式分支策略——基于变量决策层的启发式变量选择策略(HSVDL),为分支决策提供依据,从而引导求解器的搜索进程。二、在充分考虑学习子句的子句长度和变量的决策层对子句删除的影响后,为了充分发挥短子句在演绎过程中的优势,因此给出平均子句长度的定义,在删除策略中用于删除较长的学习子句。然后提出了一种新的学习子句删除策略——基于学习子句长度和LBD的删除策略(LLBD)。三、分别将所提出的HSVDL策略和LLBD策略形成相应算法,嵌入到著名求解器Glucose4.1中,得到新的求解器Glucose4.1+HSVDL和Glucose4.1+LLBD;将所提出的HSVDL策略和LLBD策略同时嵌入求解器Glucose4.1中,得到新的求解器Glucose4.1+HSVDL+LLBD。选择2017年和2018年SAT国际竞赛Main Track组的竞赛例进行测试,测试结果从成功求解个数、平均决策次数、平均冲突次数、平均重启次数、平均用时等多项指标与求解器Glucose4.1的测试结果进行对比分析,显示出了新的求解器的有效性及优势。

来源：

同方学位论文库评论

基于cdcl的SAT问题的分支启发式策略研究

基于CDCL的SAT问题的分支启发式策略研究

引用

作者：胡容西南交通大学

学位级别：硕士

命题逻辑公式的可满足性问题(SAT问题)是指给出一个合取范式,判断是否存在一组赋值使得这个合取范式可满足。SAT问题是计算机科学与工程、人工智能、计算机视觉和计算机辅助设计等领域的一个核心问题,它也是第一个被证明的NP完全(Non-De... 详细信息

命题逻辑公式的可满足性问题(SAT问题)是指给出一个合取范式,判断是否存在一组赋值使得这个合取范式可满足。SAT问题是计算机科学与工程、人工智能、计算机视觉和计算机辅助设计等领域的一个核心问题,它也是第一个被证明的NP完全(Non-Deterministic Polynomial-Complete,NPC)问题。正因为如此,研究SAT问题并提高求解器的效率是很有价值的。求解SAT问题的算法分为完备算法和不完备算法。完备算法的特点是在问题可满足时,给出一个模型;不可满足时,给出证明。基于完备算法的优点,本文以cdcl(Conflict Driven Clause Learning,cdcl)算法为框架,研究cdcl算法的以下主要流程:决策、冲突分析、学习子句和回溯之间的关系。SAT求解器的成功绝大多数归因于从错误赋值中学习的能力、快速地删除搜索空间以及首先集中在那些“重要”变量中。故本文集中在cdcl算法中的决策和冲突分析上,取得的主要研究结果如下:1.当一个命题逻辑中的逻辑公式以CNF的形式输入到数据库时,从中选择“重要”变量的依据是变量出现的次数和包含该变量子句的长度。因为越短的子句越难满足,故优先考虑短子句,相应地,短子句中的变量就“重要”。由这些信息,给出变量的初始计分和排序方法。2.当发生冲突时,即当前赋值使得某些子句为不可满足子句,参与冲突的那些子句中对应的变量的价值高于没有参与冲突的,因而在这个阶段考虑由这些子句或者变量所携带的信息刻画变量的贡献值。根据参考文献中的实验数据分析看出指数级的增长效果较好,因此,根据学习子句长度的不同,进行分段,在每个段,给出一个常数加上一个指数函数的方法进行计分排序。3.根据以上研究结果提出一种新的分支启发式策略并运用在glucose4.0算法上,用2016和2017年SAT竞赛例子和SATLIB例子测试,根据效果修改参数。结果表明在一定程度上比原始求解器glucose4.0有所提高。

来源：

同方学位论文库评论

基于cdcl结构的SAT问题优化策略的研究

基于CDCL结构的SAT问题优化策略的研究

引用

作者：杜忠和西南交通大学

学位级别：硕士

可满足性问题（即SAT问题）是当代理论计算机科学的重要研究方向之一,也是第一个被证明的NP完全问题,SAT问题的求解有助于解决其他NP问题。其快速求解算法不仅具有重要的理论意义,也具有重要的实际价值。SAT问题广泛应用于社会生产和人... 详细信息

可满足性问题（即SAT问题）是当代理论计算机科学的重要研究方向之一,也是第一个被证明的NP完全问题,SAT问题的求解有助于解决其他NP问题。其快速求解算法不仅具有重要的理论意义,也具有重要的实际价值。SAT问题广泛应用于社会生产和人类生活中的各个领域,如人工智能、自动推理、软件自动验证等。因此,设计并实现求解SAT问题的高效算法具有重要研究意义。目前,求解SAT问题的算法主要分为完备算法和不完备算法两类。不完备算法主要是基于随机搜索策略的局部搜索算法。完备算法主要基于1962年由Martin Davis,Hilary Putnam,George Logemann和Donald ***提出的DPLL算法,现在大多数完备算法都是基于DPLL算法发展而来,包括现在主流的cdcl算法。随着社会科学的进步,许多基于cdcl算法的求解器应运而生,用于解决日益复杂的大规模SAT问题,如z Chaff、Mini SAT、Glucose、Lingeling、PicoSAT等。本文基于cdcl算法结构,做了如下几个方面的研究工作:1.根据变量决策层和冲突次数,引入了分支决策阶段变量得分的增量函数,用于动态衡量不同搜索阶段下变量的得分,在此基础上,提出了基于变量决策层的分支策略（DLBH）,为分支决策提供依据,引导求解器搜索过程;2.根据学习子句中不同变量的决策层,引入了子句深度,用于评估求解过程中所产生学习子句的质量,以删除低质量学习子句而保证高效率求解为目的,提出了基于子句深度的学习子句删除策略（DBCD）;3.分别将所提出的DLBH策略和DBCD策略形成相应算法,嵌入到著名求解器Glucose3.0中,得到新的求解器glucose3.0+dlbh和glucose3.0+dbcd;将DLBH策略和DBCD策略对应的算法同时嵌入到著名求解器Glucose3.0中,得到新的求解器glucose3.0+dlbh+dbcd。选择2015年和2017年SAT国际竞赛中的问题进行测试,从测试结果在成功求解个数、平均决策次数、平均冲突次数、平均重启次数、平均用时等多项指标进行对比分析,显现出了新的求解器的有效性及优势。

来源：

同方学位论文库评论

欢迎您,

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

在线全文

在线全文

在线全文

在线全文

在线全文

在线全文

在线全文

在线全文

在线全文

在线全文

请选择保存的检索档案：

请选择收藏分类：

通借通还

欢迎您,

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

在线全文

在线全文

在线全文

在线全文

在线全文

在线全文

在线全文

在线全文

在线全文

在线全文

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：