云南高校图书馆联盟文献共享服务平台- 可满足性

可满足性: 作品数：202被引量：370H指数：9; 导出分析报告; 相关领域：自动化与计算机技术更多>>; 相关作者：李光辉常亮李晓维翟治年刘歆更多>>; 相关机构：清华大学浙江大学西安电子科技大学北京航空航天大学更多>>; 相关期刊：更多>>; 相关基金：国家自然科学基金国家高技术研究发展计划国家重点基础研究发展计划浙江省自然科学基金更多>>

模态计数逻辑ML(#)在不同框架类下的可判定性: 《逻辑学研究》2024年第3期86-101,共16页付小轩赵之光; supported by Tsinghua University Initiative Scientific Research Program;supported by Taishan Young Scholars Program of the Government of Shandong Province,China(No.tsqn201909151);Shandong Provincial Natural Science Foundation,China(No.ZR2023QF021);Support Plan on Science and Technology for Youth Innovation of Universities in Shandong Province(No.2021KJ086)。; 在本文中,我们给出模态计数逻辑ML(#)在不同框架类下的可满足性的判定过程。我们使用两种方法,一种是通过修改ML(#)相对于全部克里普克框架的可满足性的判定算法,另一种是将ML(#)的可判定性归约到基本模态逻辑。我们还证明了分次模态计...; 关键词：可满足性模态逻辑可判定性归约克里普克判定算法框架类判定过程

(G,N)-蕴涵关于常见推理规则的可满足性: 《兰州理工大学学报》2024年第2期161-168,共8页李冉冉于鹏; 国家自然科学基金(12171294)。; 针对(G,N)-蕴涵是否满Modus Ponens、Modus Tollens和Hypothetical Syllogism等推理规则问题展开讨论,给出了几类常见t-模下,(G,N)-蕴涵满足相应推理规则的判定条件,为优化模糊推理算法的设计提供了参考依据.; 关键词：三角模 (G N)-蕴涵 MP规则 MT规则 HS规则

共识协议的形式化验证研究现状与展望: 《软件学报》2023年第11期4989-5007,共19页葛宁贺俞凯翟树茂李晓洲张莉; 国家重点研发计划(2018YFB1402700);国家自然科学基金(61902011);北京航空航天大学软件开发环境国家重点实验室开放课题(SKLSDE-2021ZX-01)。; 分布式系统在计算环境中发挥重要的作用,其中的共识协议算法用于保证节点间行为的一致性.共识协议的设计错误可能导致系统运行故障,严重时可能对人员和环境造成灾难性的后果,因此保证共识协议设计的正确性非常重要.形式化验证能够严格...; 关键词：共识协议形式化验证限界模型检测定理证明布尔表达式可满足性理论可满足性模理论

工作流可满足性的约简增量模式回溯法: 《计算机集成制造系统》2023年第11期3624-3638,共15页翟治年刘关俊卢亚辉向坚吴茗蔚丰明坤; 国家自然科学基金面上项目(62172299,61972357);浙江省基础公益研究计划资助项目(LGF22F020017)。; 在大量云/服务化资源造成的性能压力下,增量模式回溯法(Incremental Pattern Backtracking, IPB)及其k指派技术是工作流可满足性求解的首选途径,但对“欠约束”实例,其模式枚举性能显著下降,不利于大量可行解的优化选择。针对该问题提...; 关键词：可满足性工作流授权约束资源分配模型计数模式

可满足性问题的精确算法和计算复杂性: 《广州大学学报（自然科学版）》2023年第5期41-51,共11页陈建二杨伟; 国家自然科学基金资助项目(61872097)。; 可满足性(SAT)问题是计算机科学中最重要的理论研究和实际应用问题之一。文章从标准计算复杂性理论的角度论述SAT问题的精确算法和计算复杂性,主要论述算法的发展,分析算法(最坏情况)的复杂度,并探讨SAT问题的复杂度上限。对一些具有意...; 关键词：可满足性 SAT算法 NP完全性精确算法计算复杂性理论

有限域(F_(2)^(8))^(8)上基于循环异或移位结构的次优扩散层研究被引量：1: 《陕西科技大学学报》2023年第4期188-194,共7页王鑫郭雅婷杨波; 国家自然科学基金项目(61801281);陕西省科技厅重点研发计划项目(2020GY-091);陕西省科技厅自然科学基础研究计划项目(2022JM-346);陕西省社会发展科技攻关计划项目(2016SF-418);陕西科技大学博士科研启动基金项目(BJ11-12)。; 基于循环移位异或运算的MDS线性变换以其具有良好的扩散雪崩性能被广泛应用于分组密码扩散层的设计中.在现有研究中,小有限域(F_(2)^(n))^(4)上最优线性变换寻找工作已接近完备,而大有限域(F_(2)^(n))^(8)上异或项数为9和11时,却不存在...; 关键词：分组密码有限域扩散层循环异或次优线性变换可满足性

利用命题逻辑最大可满足性的冗余通孔最优插入方法: 《计算机辅助设计与图形学学报》2023年第7期1132-1138,共7页杨成杨骏张亚东; 在纳米尺度的集成电路设计中,冗余通孔插入是减轻通孔失效造成良率降低问题的常用技术.文中将最优冗余通孔插入问题规约到命题逻辑最大逻辑可满足性(maximum satisfiability,Max SAT)问题,并利用完备求解器求取最优解.Max SAT问题是一...; 关键词：冗余通孔插入命题逻辑最大可满足性问题版图后优化可制造性设计

约束可满足性中求解RB模型实例的算法综述: 《计算机应用研究》2023年第7期1929-1936,1946,共9页杨易王晓峰莫淳惠庞立超杨澜赵星宇; 国家自然科学基金资助项目(62062001);宁夏青年拔尖人才资助项目(2021)。; 约束满足问题是人工智能领域中最基本的NP完全问题之一。多年来,随着约束满足问题的深入研究,国内外学者提出多种实例模型。其中,RB模型是一种能生成具有精确相变的增长域约束满足问题实例,其求解难度极具挑战性。为了寻找其求解的新型...; 关键词：约束满足问题 RB模型回溯启发式算法信息传播算法元启发式算法

资源独立工作流可满足性的最小增量模式回溯: 《软件学报》2023年第4期1543-1569,共27页翟治年卢亚辉刘关俊雷景生向坚吴茗蔚; 国家自然科学基金(62172299,61972357);浙江省教育厅一般科研项目(Y201737476)。; 工作流可满足性是业务安全规划的基本问题,正在面临高资源配比(资源数n显著大于步骤数k)造成的性能挑战.在资源独立约束下,其最高效求解途径是模式空间上的增量回溯法IPB.为克服结点真实性验证的性能瓶颈,它增量计算模式k指派(二部)图及...; 关键词：工作流授权约束资源独立资源分配可满足

芯片设计形式验证被引量：5: 《前瞻科技》2023年第1期23-32,共10页詹博华吴志林; 国家重点研发计划(2021ZD0113300)。; 芯片设计验证是对芯片设计是否正确与安全进行检查,在芯片设计流程中具有非常重要的地位,占其将近1/2的成本和时间。形式验证是保证计算机软硬件系统正确性与安全性的非常重要的手段,已经成功用于芯片设计验证。全世界三大电子设计自动...; 关键词：芯片设计正确性与安全性电子设计自动化等价性验证基于断言的形式验证命题逻辑可满足性(SAT)求解模型检测

可满足性