可满足性问题
可满足性问题的相关文献在1989年到2022年内共计134篇,主要集中在自动化技术、计算机技术、无线电电子学、电信技术、数学
等领域,其中期刊论文113篇、会议论文8篇、专利文献8846篇;相关期刊61种,包括阜阳师范学院学报(自然科学版)、安徽理工大学学报(自然科学版)、电脑知识与技术等;
相关会议8种,包括第32届中国数据库学术会议、第五届江苏计算机大会、2007全国开放式分布与并行计算学术年会等;可满足性问题的相关文献由269位作者贡献,包括殷志祥、王晓峰、唐璞山等。
可满足性问题
-研究学者
- 殷志祥
- 王晓峰
- 唐璞山
- 周电
- 唐震
- 常亮
- 徐扬
- 荆明娥
- 许道云
- 于卓
- 刘大为
- 刘志鹏
- 刘燕丽
- 史峰
- 吴宇翔
- 吴贯锋
- 周强
- 唐屹
- 张斌
- 张楠
- 张立明
- 张长胜
- 欧阳丹彤
- 贺毅朝
- 郭莹
- 丁敏
- 丁红胜
- 刘文君
- 刘显敏
- 古天龙
- 史忠植
- 叶安胜
- 姚尧
- 姜久雷
- 孙纪舟
- 尹文波
- 崔建中
- 张健
- 张婷
- 张英杰
- 张钹
- 徐小萍
- 曹泽轩
- 李建中
- 李强
- 杨帆
- 杨静
- 沈雪
- 熊伟
- 王金艳
-
-
梁晨;
王晓峰;
刘子琳;
芦磊;
牛鹏飞
-
-
摘要:
信息传播算法在可满足性(SAT)问题上性能表现优越,其收敛性却依赖于因子图的结构复杂程度,至今缺少系统的理论解释。调查传播算法(SP)是解决SAT问题效果最好的信息传播算法。为有效分析SP算法的收敛性,借助因子图转换技术和鲁汶算法划分因子图社区,基于K维结构熵理论,提出了SAT实例的K维结构熵度量模型,得出了随机SAT实例的K维结构熵。分析了SP算法收敛性与K维结构熵之间的关系,给出了SP算法收敛性的K维结构熵阈值。实验证明该方法有效。
-
-
孙瑞;
黄佳文;
孙学贵
-
-
摘要:
基于可满足性问题构造加密方案具有挑战性,关键是如何构造具有加密功能的难解的SAT合取范式,并将明文安全地隐藏在其中。文章首先改进了SRR(N,k,s)模型用以隐藏明文;其次,通过恰当选取约束密度值,保证密文的难解性;最后,证明方案满足选择明文攻击(IND-CPA)是安全的。
-
-
吴宇翔;
王晓峰;
丁红胜;
于卓
-
-
摘要:
Max-SAT问题是SAT问题的优化版本,目标是在给定的子句集中找到一组变元赋值,使得满足子句数最多,该问题是典型的NP-hard问题。随着大数据和人工智能的深度发展,过去原有的算法已不再适用,设计新的求解算法或对已有的求解算法进行优化是目前研究的热点。针对警示传播算法求解随机Max-3-SAT问题的局限性,提出了一种基于变元权值计算的警示传播算法,结合随机游走算法,给出一种新型算法WWP+WalkSAT,通过改进求解的局限性,更好地得到一组有效的初始解,从而提高算法的局部搜索能力。利用2016年Max-SAT国际竞赛部分基准实例,将WWP+WalkSAT算法与八种局部搜索算法进行精度方面的对比实验。实验结果表明,WWP+WalkSAT算法有较好的性能。
-
-
谢志新;
王晓峰;
曹泽轩;
于卓;
莫淳惠;
吴宇翔
-
-
摘要:
信息传播算法来自统计物理,被广泛应用于人工智能各个领域,特别是求解组合优化问题时,具有良好的有效性。通过对信息传播算法的相关文献进行分析,综述了信息传播算法以及其相关应用的发展史,根据信息传播算法的发展,介绍了求解可满足性问题的信息传播算法相关概念,主要涉及到警示传播算法、置信传播算法和调查传播算法,描述了三种算法发展中出现的收敛性、有效性研究,分别综述了各个算法在相关领域的应用情况,并总结了信息传播算法的研究路径和应用方向。
-
-
谢志新;
王晓峰;
于卓;
曹泽轩;
吴宇翔;
莫淳惠
-
-
摘要:
警示传播算法作为一种基本的信息传播算法,其收敛时求解可满足性问题十分有效,但因子图结构较为复杂时,算法往往不收敛导致求解失败。为了对这种现象给予理论解释,同时对警示传播算法收敛性进行有效分析,利用树分解方法构造了命题公式对应因子图的树宽度量模型,计算可满足随机实例的树宽。建立树宽与警示传播算法收敛性之间的关系,给出了基于树宽的警示传播算法收敛性判定条件。通过实验分析,结果表明该方法有效,对于分析其他信息传播算法收敛性分析研究具有十分重要的意义。
-
-
牛进;
王晓峰;
林青文
-
-
摘要:
收敛性是评价信息传播算法性能的重要指标,信息传播算法求解可满足性问题时,命题公式的结构特征影响算法的收敛性,具有复杂结构的命题公式,信息传播算法不总收敛.为了系统地对此现象给予理论解释,借助于结构熵的方法和技术,提出命题公式的结构熵模型及其度量方法,计算随机可满足性实例的结构熵.警示传播算法(WP)作为信息传播算法的基本模型,分析WP算法的收敛性对于研究其他信息传播算法的收敛性具有重要意义,分析了WP算法收敛性与结构熵之间的关系,给出WP算法收敛的判定条件.通过实验分析,该方法有效可行.
-
-
王晓峰;
许道云;
杨德仁;
姜久雷;
李强;
刘欣欣
-
-
摘要:
信念传播算法是基于因子图模型的消息传递算法,通过图中的边,将消息从一个结点传递给另一个结点,以高概率地确定部分变量的取值,这种方法被实验证明在求解可满足性问题时非常有效.然而,目前还未对其有效性从理论角度给予解释.通过对信念传播算法的收敛性分析,试图从理论上解释算法的有效性.在信息传播算法的信息迭代方程中,参数的取值范围为(0,1),将该取值范围扩展到整个实数空间,即(-∞,+∞).利用压缩函数的数学原理,得到了信息迭代方程收敛的判定条件.选取随机可满足性问题实例进行实验模拟,验证了结论的正确性.
-
-
王金艳;
胡春;
高健
-
-
摘要:
知识编译作为人工智能的重要方向,在实时查询和推理中起重要作用.有序二元决策图(ordered binary decision diagram,OBDD)是知识编译领域中一个主要的编译目标语言,已被广泛用于编译诸多实际的可满足性问题(SAT).近年来,OBDD的构造技术得到了深入研究,其目的是减少目标OBDD的大小并且缩短编译时间.OBDD的构造方式是影响编译效率的重要因素,为了提高编译时间效率,本文提出一种改进的OBDD构造算法,该算法将SAT问题的子句编译成OBDD的表示形式,并将这些OBDD合并成一个整体.不同于传统的合并算法逐一将OBDD合并到目标OBDD中,本文将一些OBDD先进行合并,然后再整合到目标OBDD中.对随机生成的SAT实例和产品配置问题的实验表明,本文提出的OBDD构造算法的性能优于原始算法.
-
-
王欣怡;
殷志祥;
唐震;
杨静;
崔建中
-
-
摘要:
DNA折纸术是一种全新的DNA自组装方法,具有可编程性、纳米可寻址性等优点,被广泛地应用于DNA计算中.利用DNA折纸术可折叠出特殊结构的特点,在DNA折纸基底上设计了一种求解可满足性问题的计算模型,该模型采用分子信标原理,通过观察荧光的明灭排除非解,从而找出可满足性问题的解.最后通过实例和模拟仿真表明了模型的可行性.
-
-
王钇杰;
徐扬;
吴贯锋
-
-
摘要:
对于SAT求解器,目前流行的分支变量决策策略大多是基于冲突的变量活跃度评估算法,选择具有最大活性的未赋值变量作为决策变量,优先解决最近的冲突.但是,它们都忽略了包含决策变量的子句数目对布尔约束传播(BCP)的影响.针对此问题,提出了 一种基于学习子句删除策略的分支变量决策策略(VDALCD),在删除学习子句的同时减小被删除子句中变量的活跃度.基于VDALCD策略分别对Glucose4.1,MapleLCMDistChronoBT-DL-v2.1进行改进,形成了求解器Glucose4.1_VDALCD和Maple-DL_VDALCD.以2018年、2019年SAT国际竞赛题为基准测试例,将改进版本与原版本求解器进行比较.实验结果表明,在2018年的例子测试中,Gluose4.1_VDALCD比Gluose4.1多求出26个例子,增加了 15.5%.在2019年的例子测试中,Maple-DL_VDALCD 比 MapleLCMDistChronoBT-DL-v2.1 多求出 17个例子,增加了 7.6%.
-
-
-
SUN Ji-Zhou;
孙纪舟;
LI Jian-Zhong;
李建中;
GAO Hong;
高宏;
LIU Xian-Min;
刘显敏
- 《第32届中国数据库学术会议》
| 2015年
-
摘要:
起初,作为一个数据库模式设计的工具,函数依赖理论得到了很多的关注,而在数据修复中,该理论并不是十分有效近年来,针对不一致数据的检测和修复问题,更多的约束被提出来,包括条件函数依赖、修复规则以及编辑规则等然而,据本文作者所知,已有方法都只关注了整个属性之间的依赖关系,而实际应用中的数据通常有部分属性之间的依赖关系例如,某单位员工的工号前两位决定了其所属的部门,而此依赖信息就被已有方法忽略本文首先提出了一类更一般化的约束—微函数依赖,微函数依赖引入提取函数,用来表示属性的部分信息利用提取函数之间的依赖关系,能够检测出更多的不一致数据理论方面,本文首先研究了微函数依赖的可满足性问题和蕴含问题,然后提供了一个正确且完备的推理系统最后,通过实验证实了微函数依赖能够在可接受的时间开销内检测出更多的错误数据.
-
-
-
熊伟;
唐璞山
- 《2007全国开放式分布与并行计算学术年会》
| 2007年
-
摘要:
提出了一项新的正向推理技术:对称扩展的一元子句推导(Symmetric Extended Unit Propagation).与传统的一元子句推导技术相比,文中的方法通过在一元子句推导过程中添加对称的蕴涵关系从而能够推导出更多的一元子句.基于这项新技术实现了一个可满足性问题(SAT)预处理器Snowball.实验结果验证了该项技术的有效性,表明该预处理器Snowball能够有效地化筒SAT问题的规模并减少解决SAT问题的时间.
-
-
-
-
-
-