导读:本文包含了满足性论文开题报告文献综述及选题提纲参考文献，主要关键词:可满足性问题,全解求解器,传统机器学习,深度学习
满足性论文文献综述
任小芹[1]（2019）在《SAT问题的可满足性判定及其全解研究》一文中研究指出可满足性问题(SAT)是数学和计算机科学领域中很重要的问题,是工业自动化等领域的应用基石。目前使用机器学习判定可满足性问题的方法仍在探索阶段,现有方法未尝试求解难度较大、规模较大的问题。因此本文设计出有效的机器学习方法来判定大规模且难以求解的可满足性问题。同时SAT问题的一个重要分支–SAT全解问题(ALLSAT),在工业界实践应用更广泛、需求更高的技术。由于SAT全解问题的计算复杂度高于一般SAT问题,目前相关研究较为匮乏,相应求解器求解能力一般。因此,本文深入研究SAT全解问题,设计出一种有效的求解全解的方法。通过将SAT问题的判定看作有监督的二分类问题,本论文设计出两种方法对SAT问题进行分类判别。一种是基于传统机器学习的求解方法,该方法首先计算SAT的特征,特征总数为141个,然后带入选定的传统机器学习模型进行训练,模型的选取是依据SAT问题的求解特性以及模型的训练效率和精度。第二种是基于深度学习的求解方法,首先将可满足性问题编码成数值矩阵,本论文设计了叁种矩阵转换的方法,并通过分析找出最优的一种转换方案,然后将转换后的数据集放入卷积神经网络中训练模型。实验结果表明,本论文提出的基于LightGBM模型的判定方法是能够快速准确的预测可满足性问题,在agile17数据集上达到了0.966高准确率;本论文提出的卷积神经网络判定模型,在单一类别的数据集上,该模型都可达到0.9以上的准确率。本论文设计的基于机器学习的SAT判定方法已经能够一定程度上求解大规模复杂的SAT问题。针对可满足性问题的全解求解,本论文设计出一种二分求解SAT全解问题的算法。同时提出两种分割策略,包括Jaccard相似度分割以及变量互补分割。实验结果表明,本论文设计的全解算法相对当前最好的全解算法,在2014年SAT竞赛数据集上能够求解更多实例并且求解的解个数更多。(本文来源于《电子科技大学》期刊2019-03-23）
张波,赵榕榕[2]（2018）在《满足性符号意义的消费与设计——创意时代高端设计产业人才培养改革研究》一文中研究指出创意时代的设计提出了更高的要求,国际前端产业链的竞争加剧了设计教育的改革步伐。这种改革不仅要从人文素养、团队合作模式等方面入手,也要从知识体系、企业与设计的协同创新入手,共同展开改革。创意时代的消费,其主要特征是满足消费者对产品的符号意义的需求和渴望为心理特征,而这种符号意义,代表着某一团体、亚文化、族群等方面的共同文化认可。(本文来源于《创意与设计》期刊2018年06期）
翟治年,卢亚辉,万健,王中鹏,吴茗蔚[3]（2018）在《互斥约束工作流可满足性决策的匹配剪枝模式回溯法》一文中研究指出针对用于工作流可满足决策的模式回溯技术如何平衡性能与代价的问题,提出了一种对部分模式解及时进行授权匹配验证的优化方法,牺牲一定验证效率以增强剪枝能力。就仅受互斥约束的问题情形,利用实例难易程度的两极分化现象对总体时间性能进行了分析。随机生成数据集上的实验表明,这一优化极大地降低了模式回溯在难实例上的时间代价,而对易实例执行时间的影响很小,且相对于其他基于动态规划的代表性算法,优化后的算法在时间和空间性能上均有显着优势。(本文来源于《中国机械工程》期刊2018年24期）
赵威亦,陈相锦,董怡雯,周冰滢,王杰[4]（2018）在《感知器神经网络线性可分判断的满足性算法》一文中研究指出感知器神经网络有着广泛的应用前景,是人工神经网络的重要组成部分。同时感知器神经网络对与现代计算机新的硬件设计也有重要研究意义。感知器神经网络的线性可分判断是感知器领域一个重要的研究内容。文章对满足性问题进行研究,把满足性算法应用于感知器神经网络的线性可分判断,提出布尔函数线性可分性判断的逻辑满足性算法。(本文来源于《台州学院学报》期刊2018年06期）
金俊杰,储着飞,王伦耀,夏银水[5]（2018）在《基于可满足性模理论的CMOL电路单元映射》一文中研究指出针对纳米CMOS混合电路(CMOL)单元映射时,传统的精确算法存在编码变量多、文件存储大导致的求解规模受限问题,提出了一种基于可满足性模理论(SMT)的CMOL电路单元映射方法,该方法通过整型编码减小文件存储大小,通过渐进式求解算法兼顾求解规模和速度.实验结果表明,与传统的精确算法相比,本文提出的方法可大幅减少中间处理文件的大小,并以较小的求解速度为代价提高了处理大规模电路的能力.(本文来源于《宁波大学学报(理工版)》期刊2018年06期）
郭贝贝[6]（2018）在《基于融资担保机制的P2P网贷满足性研究》一文中研究指出基于网贷平台信息服务中介的定位,网贷市场"去担保化"趋势不可避免,但网贷平台的"去担保化"切勿"一刀切"。研究发现,在五种担保模式中,融资性担保模式和风险准备金模式,对于网贷融资满足性存在显着的正向相关关系,起到了积极的促进作用。采取不同担保模式的网贷平台的风险性存在巨大差异,平台数据的有效性及参考价值也存在差异。网贷市场引入担保机制,不可避免地强化了网贷投资者的"羊群行为",即非理性行为。但是在借贷经济活动过程中,网贷参与者更偏好于小额借贷,保持资金的流动性及安全性,这也是网贷市场中投资者自觉规避风险的手段。(本文来源于《金融与经济》期刊2018年06期）
张晓[7]（2018）在《面向问题的需求满足性验证和测试方法研究与实现》一文中研究指出随着科学技术的进步,系统实现的功能越来越多,系统的规模变大,复杂性也有所提高。根据美国权威组织Standish Group在2015年的报告中得出的结论,规模越大的项目越容易失败。特别是在工业4.0理念深入人心的时候,信息物理融合系统(CPS)作为工业制造的主要技术,成为了学者和专家的研究目标之一。由于信息物理融合系统中使用到大量的硬件,所以它的开发成本相当昂贵;同时,信息物理融合系统的质量与人们的生活质量、生命和财产安全等相关。而在过去的研究中得知,需求是项目成败的最关键的因素。需求建模是为了系统开发人员从获取到的需求信息中能够在语义上正确地理解其含义,让客户可以正确表达和判断自己的表达的需求信息是否符合自己真实的想法。学术界和企业都比较关注需求建模方法,在多个需求建模方法中,问题框架方法也受了一些大学和学者们的青睐。问题框架方法作为面向问题的需求工程方法,在众多人的不断研究和探索下,在系统开发的过程中越来越发挥了重要作用。问题框架方法描述用户需求,有很多方向值得研究和进一步的探究。问题框架方法由Jackson在20世纪90年代提出来的。该方法充分考虑软件的运行环境,也即问题所在的现实世界。本文先是基于问题框架方法开展了两点研究。一是利用问题图转化成通信顺序进程(CSP)脚本去验证需求满足性。二是制定对象约束语言(OCL)约束附加到建模环境中,以此实现模型的完整性、正确性校检。问题框架是半形化方法,它难对复杂系统模型进行严格的语义分析和正确性验证。问题框架又是一个严谨的建模语言,它规定了相应的完整性和正确性约束。然后,本文借鉴前人的思想,在需求分析阶段引入测试相关工作。在需求分析阶段,如果把测试工作也加入其中,可以使需求更加详尽。在大型的CPS系统的中,物理组件的故障,计算组件的故障,计算组件与物理组件的交互故障等都有可能导致软件的毁坏,甚至是安全事故。而如何短时间有效排除故障,且精准的分析故障原因,这些都需要用到系统仿真建模。因此本文使用问题框架建模方法描述需求,并根据因果关系链为系统生成测试线索和设计一组符合CPS系统的测试用例。最后,本文实现一款软件,该软件将本文研究内容一一实现。同时,软件实现了多个角色用户和多个需求分析师之间的协同建模。一款好的建模软件应该实现多人协同,供叁种以上不同角色的人同时使用,这样有利于需求分析的迭代和指导软件开发,以及对测试工作的帮助。(本文来源于《广西师范大学》期刊2018-06-01）
孙瑞[8]（2018）在《基于可满足性问题的密码体制构造及应用》一文中研究指出随着信息技术的迅猛发展,大数据环境下用户信息在传递过程中的安全性问题成为人们最关注的热点之一。众所周知,公钥加密体制是近代密码学的重要研究内容,同时也是保障大数据环境下用户数据安全的重要工具。然而许多经典的公钥加密体制都不能满足较高的可证明安全性,且现有的许多公钥加密方案常常为了满足某些特殊性质(如同态性、可验证性、可委派性等)而很难达到较高的安全性,因此研究如何构造安全的公钥加密体制显得尤为必要。本文以可满足性问题(SAT)为基础,以SRR模型和可证明安全理论为工具,对基于随机正则可满足性问题的公钥加密方案的安全性进行了具体研究。本文主要研究工作如下:(1)基于可满足性问题的公钥加密方案。首先,对传统的SRR(N,k,s)模型进行改进,使其满足对数据加密的功能;其次,根据现有的对随机正则(k,s)-SAT问题临界值的研究,合理约束所构造的(3,s)-SAT合取范式的约束密度,从而生成难解的(3,s)-SAT实例并加密明文;最后,在可证明安全理论的框架下证明本方案能够满足选择明文攻击安全。(2)基于可满足性问题的混合加密方案。首先,基于随机正则公式在相变点附近的难解性问题,结合并改进SRR模型,用以加密明文;其次,在已有的Damg?rd Elgamal方案的基础上,引入数据封装机制和Hash函数提升其安全性,提出了一个基于SAT与离散对数问题的混合加密方案;最后分析表明,本方案与已有的基于SAT的混合加密方案相比,私钥长度更短,满足密文可验证性,且能够安全抵抗适应性选择密文攻击安全。(3)基于可满足性问题的混合加密方案在快递保密面单中的应用。利用基于SAT的混合加密算法对用户的信息进行加密,在快递运输和派送阶段,由于密文的可验证及算法的安全性,不仅能够保障快递线下运输时用户信息的隐私性,还能保障信息的完整性与可用性,从而减少了用户信息在线下泄露的风险。(本文来源于《贵州大学》期刊2018-06-01）
丁陈陈[9]（2018）在《最大可满足性问题的博弈算法研究》一文中研究指出最大可满足性问题(MaxSAT)是人工智能领域研究的核心问题之一,很多复杂的实际问题都可以通过MaxSAT建模并求解,对于MaxSAT问题的研究具有理论和实际的双重意义。近些年,随着科学研究的进步和工业技术的发展,MaxSAT问题的规模成倍增长。为满足新的MaxSAT问题求解的需求,本文基于布尔博弈模型提出两个适用于不同规模MaxSAT实例求解的博弈算法,包括用于求解一般规模MaxSAT实例的基本博弈算法bgmaxsat和用于求解大规模MaxSAT实例的分组博弈算法bgmaxsat_m。本文的主要工作总结为以下四点。(1)我们提出一种将MaxSAT实例映射为布尔博弈模型的建模方法,通过博弈参与者的策略选择过程来模拟MaxSAT实例中的变量赋值过程。博弈参与者的策略基于重新定义的目标函数和收益计算函数进行选择,并依据其他参与者的策略不断更新。(2)针对MaxSAT问题的特征,我们对经典布尔博弈模型进行改进,提出基于动态收益矩阵的动态博弈模型。在动态博弈模型中,参与者的收益矩阵在博弈过程中实时变化,使得所有参与者都能够按照自身的目标函数快速收敛。基于动态博弈模型,我们提出求解一般规模MaxSAT实例的基本博弈算法bgmaxsat。(3)针对大规模MaxSAT实例产生大量博弈参与者的问题,我们提出一种新的博弈参与者联盟构建方法。我们基于无向图重建博弈参与者间的关系,将相互间无关系的参与者划分为一组来构建联盟,从而有效降低博弈规模。(4)基于博弈参与者联盟,我们提出求解大规模MaxSAT实例的分组博弈算法bgmaxsat_m。在bgmaxsat_m算法中,我们将博弈的基本单位设定为参与者联盟,并将信息共享通道仅设定在联盟之间。在实验部分,我们基于4个测试数据集进行了多组对比实验。首先,我们在846个一般规模MaxSAT实例上评估bgmaxsat算法,并与CCLS2016、Swcca-ms、ahmaxsat1.55叁个最新算法进行对比。实验结果表明,在求解一般规模的MaxSAT实例时,bgmaxsat算法的性能与CCLS2016算法相近,其分别在不同分类的实例上各占优势,同时优于Swcca-ms算法和ahmaxsat1.55算法。其次,我们在100个变量规模超过105的大规模MaxSAT实例上评估bgmaxsat_m算法,并与CCLS2016、wbo、Open-wbo、pwbo、CnC-LS五个最新算法进行对比。实验结果表明,在求解大规模MaxSAT实例时,bmgaxsat_m算法的性能在所有分类的实例上均明显优于CCLS2016算法、wbo算法和pwbo算法,并且在随机分类的实例上优于Open-wbo算法和CnC-LS算法,而仅在部分工业分类的实例上不及Open-wbo算法和CnC-LS算法。(本文来源于《中国科学技术大学》期刊2018-05-21）
唐宇[10]（2018）在《概率时间交替μ-演算的可满足性与模型检测研究》一文中研究指出多智能体系统(Multi-Agent System,MAS)由多个自主智能体组成,这些智能体共同工作在同一环境中,并与环境实时交互,协调完成系统功能。为了描述MAS的不确定性以及动态性,研究者向系统模型中引入概率因子,形成了随机MAS(Stochastic MAS)。概率时间交替时态逻辑(Probabilistic Alternating-Time Temporal Logic,PATL/PATL*)可用于描述与验证并发随机MAS。然而,针对该时态逻辑的模型检测算法大多是基于特定的轮换MAS(Turn-Based MAS),而对于一般的模型系统,仍没有最优的解决策略。此外,针对该时态逻辑的可满足性问题也没有可行的判定算法。因此,提出可描述并发随机MAS的新型时态逻辑,并解决相应时态逻辑的可满足性以及模型检测问题成为本文的研究核心。首先,本文提出一种新型基于概率的时态逻辑:概率时间交替μ-演算(Prob-abilistic Alternating-Time μ-Calculus,PAMC)。PAMC 可用于描述与验证并发随机MAS,它是对时间交替μ-演算(Alternating-Time μ-Calculus,AMC)的概率扩展。PAMC将AMC中联合模态<<A>>ψ替换为概率联合模态<<A>>(?)kψ,概率性描述了一组智能体的策略选择问题。PAMC既包含了 AMC也涵盖了概率模态μ-演算(Probabilistic Modal μ-Calculus,PμTL),且 PAMC与PATL 及 PATL*是不可比较的。其次,本文分析了 PAMC的可满足性问题,并提出了相应的判定算法。本文利用相交图以及最大独立集,通过检测是否存在一个概率分布满足最大独立集内各公式的概率约束条件,继而判定PAMC公式是否可满足。通过上述方式将PAMC的可满足性问题归约到奇偶博弈(Parity Game)问题上:玩家0在博弈中存在一条获胜策略当且仅当PAMC公式可满足。PAMC可满足性问题的复杂度为2-EXPTIME。再者,本文在AMC以及μ-PCTL的模型检测算法基础上,提出了 PAMC模型检测算法。PAMC 在概率并发博弈结构(Probabilistic Concurrent Game Structure,PCGS)上的模型检测复杂度为UP∩co-UP,且针对该模型检测算法,存在某个常量c,使其在O((|φ|·|M|c·dep(φ)时间内可判定。最后,本文设计并实现了 PAMC可满足性检测工具PAMCSolver,它是目前第一个可以判定(概率)时间交替时态逻辑以及PμTL可满足性问题的检测工具。(本文来源于《华东师范大学》期刊2018-05-10）
满足性论文开题报告
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
创意时代的设计提出了更高的要求,国际前端产业链的竞争加剧了设计教育的改革步伐。这种改革不仅要从人文素养、团队合作模式等方面入手,也要从知识体系、企业与设计的协同创新入手,共同展开改革。创意时代的消费,其主要特征是满足消费者对产品的符号意义的需求和渴望为心理特征,而这种符号意义,代表着某一团体、亚文化、族群等方面的共同文化认可。
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
满足性论文参考文献
[1].任小芹.SAT问题的可满足性判定及其全解研究[D].电子科技大学.2019
[2].张波,赵榕榕.满足性符号意义的消费与设计——创意时代高端设计产业人才培养改革研究[J].创意与设计.2018
[3].翟治年,卢亚辉,万健,王中鹏,吴茗蔚.互斥约束工作流可满足性决策的匹配剪枝模式回溯法[J].中国机械工程.2018
[4].赵威亦,陈相锦,董怡雯,周冰滢,王杰.感知器神经网络线性可分判断的满足性算法[J].台州学院学报.2018
[5].金俊杰,储着飞,王伦耀,夏银水.基于可满足性模理论的CMOL电路单元映射[J].宁波大学学报(理工版).2018
[6].郭贝贝.基于融资担保机制的P2P网贷满足性研究[J].金融与经济.2018
[7].张晓.面向问题的需求满足性验证和测试方法研究与实现[D].广西师范大学.2018
[8].孙瑞.基于可满足性问题的密码体制构造及应用[D].贵州大学.2018
[9].丁陈陈.最大可满足性问题的博弈算法研究[D].中国科学技术大学.2018
[10].唐宇.概率时间交替μ-演算的可满足性与模型检测研究[D].华东师范大学.2018