SAT问题
SAT问题的相关文献在1996年到2022年内共计81篇,主要集中在自动化技术、计算机技术、无线电电子学、电信技术、数学
等领域,其中期刊论文75篇、会议论文4篇、专利文献6528篇;相关期刊41种,包括中山大学学报(自然科学版)、贵州大学学报(自然科学版)、西南交通大学学报等;
相关会议3种,包括中国通信学会第五届学术年会、2006年中国科学院智能计算与生物信息学学术研讨会、中科院自动化研究所自动化与信息技术发展战略研讨会暨2003年学术年会等;SAT问题的相关文献由159位作者贡献,包括许道云、宋振明、徐扬等。
SAT问题
-研究学者
- 许道云
- 宋振明
- 徐扬
- 焦李成
- 何星星
- 吴学江
- 吴贯锋
- 徐云
- 李淑霞
- 王晓峰
- 谷文祥
- 陈国良
- 陈青山
- 丘海明
- 付非凡
- 任世军
- 余丰人
- 刘涛
- 刘芳
- 周育人
- 常文静
- 李国杰
- 李阳阳
- 杨晗
- 殷明浩
- 田宗权
- 胡显伟
- 范朝冬
- 许进
- 贺毅朝
- 郭莹
- 顾钧
- 高赛
- CHEN JianEr
- LI ShaoHua
- LI WenJun
- PAN LinQiang
- PAUN Gheorghe
- PEREZ-JIMENEZ Mario J.
- WANG JianXin
- 万武族
- 于茗谦
- 何彬
- 余文
- 余晓星
- 傅阳春
- 凌应标
- 刘伟
- 刘伯文
- 刘婷
-
-
芦磊;
王晓峰;
梁晨;
张九龙
-
-
摘要:
可满足(SAT)问题是指:是否存在一组布尔变元赋值,使得随机合取范式(CNF)公式中每个子句至少有1个文字为真。多文字可满足SAT问题是指:是否存在一组布尔变元赋值,使得随机CNF公式中每个子句至少有2个文字为真。此问题仍然是一个NP难问题。定义约束密度α为CNF公式子句数与变元数之比,对该问题的相变点上界α*进行了研究。如果α>α*,则多文字可满足SAT问题高概率不可满足。通过一阶矩一个简单的推断,可以证明α*=-ln 2/ln(1-(k+1)/2 k),当k=3时,α*=1。利用Kirousis等人的局部最大值技术,提升了多文字可满足3-SAT问题的相变点上界α*=0.7193。最后,选择了大量数据进行实验验证,结果表明,理论结果与实验结果相吻合。
-
-
何彬;
许道云
-
-
摘要:
通过构造适当的极小不可满足公式以实现在多项式时间内将3-CNF公式归约转换为一个正则(3,4)-CNF公式,转换后的公式与原公式具有相同的可满足性,同时公式的结构也发生相应的变化.图的社区结构反映了图的模块特性,文中将CNF公式转化为相应的图,研究公式图的模块特性与公式某些性质之间的关系.将归约前后的两类公式转换为相应的图并研究其模块特性,发现转换后得到的正则(3,4)-CNF公式具有较高的模块度.此外,在使用DPLL(Davis Putnam Logemann Loveland)算法求解CNF公式的过程中,发生冲突时利用冲突驱动子句学习策略,得到一个学习子句并将其添加到原公式中,使得原公式的模块度降低.研究发现:将DPLL算法与冲突驱动子句学习策略结合应用到正则(3,4)-CNF公式时,其学习子句所包含的绝大部分变元位于不同的社区中.
-
-
王帅;
王晓峰;
梁田;
李志
-
-
摘要:
警示传播WP算法是一类重要的信息传播算法,在命题公式的可满足性判定中非常有效.通过对WP算法的数学原理分析发现,当算法收敛时以高概率固定部分变元的赋值,可以对公式进行化简.基于这样的特征修改WP算法的迭代方程和变元赋值条件,设计了一种求解命题公式骨干集的信息传播算法.当变元数目超过400时,与经典骨干集求解算法对比,效率提高了40%,与目前常用算法对比也有10% 的提高.结果表明,所提算法求解命题公式骨干集时非常有效.
-
-
-
-
-
杨晗;
宋振明
-
-
摘要:
研究SAT问题不仅具有重要的理论意义,而且具有实际应用价值。设计高效的SAT问题的算法是国内外研究的热点。而分支策略是影响求解算法关键因素之一,目前大多数分支策略都是基于VSIDS策略提出的,虽然存在很多分支策略,但仍不能满足实际需要。为此,针对求解SAT问题实例会中出现子句长度不一致的情况,提出一种新的分支策略,基于子句长度的分支策略(BSBCL),并通过实验验证其有效性。
-
-
吴贯锋;
徐扬;
常文静;
陈树伟;
徐鹏
-
-
摘要:
为了提高SAT(boolean satisfiability)问题求解效率,在OpenMP(open multi-processing)编程框架下,将遗传算法与局部搜索算法结合,改进了混合遗传算法中的选择算法,将原有选择操作的时间复杂度降低到O(N)级别.算法采用OpenMP中的编译制导语句#pragma omp parallel粗粒度并行化驱动混合遗传算法,采用#pragma omp single语句块实现了子种群间个体的同步迁移操作.与同类算法HCGA(hybrid cloud genetic algorithm)比较分析表明:改进算法HGA(hybrid genetic algorithm)以及并行后的混合遗传算法CGPHGA(coarse-grained parallel hybrid genetic algorithm)在求解成功率和求解效率上都有显著提高,部分问题求解成功率提高达5倍.
-
-
陈秀兰;
刘婷
-
-
摘要:
分支启发式算法在CDCL SAT求解器中有着非常重要的作用,传统的分支启发式算法在计算变量活性得分时只考虑了冲突次数而并未考虑决策层和冲突决策层所带来的影响.为了提高SAT问题的求解效率,受EVSIDS和ACIDS的启发,提出了基于动态奖惩DRPB的分支启发式算法.每当冲突发生时,DRPB通过综合考虑冲突次数、决策层、冲突决策层和变量冲突频率来更新变量活性得分.用DRPB替代VSIDS算法改进了Glucose 3.0,并测试了SATLIB基准库、2015年和2016年SAT竞赛中的实例.实验结果表明,与传统、单一的奖励变量分支策略相比,所提分支策略可以通过减少搜索树的分支和布尔约束传播次数来减小搜索树的规模并提高SAT求解器的性能.
-
-
李梓齐;
许道云
-
-
摘要:
可满足性问题的求解算法和结构性质研究是计算机科学中重要问题之一,为寻求某些CNF公式子类问题有效算法或算法改进途径,对公式的结构加以某些限制,其中限定子句长度为恒定常数和变元出现次数是常见的处理方式.研究具有正则结构且每个变元正负出现均衡的结构化公式的可满足性问题求解,其随机生成模型的构建及随机实验测试有助于观察解分布状况.并且,随机局部搜索算法在求解具有一定规则结构CNF公式实例中具有良好效率.本文集中研究平衡正则(k,2r)-CNF公式的求解问题,即限制每个子句的长度为k,每个变元出现的次数为偶数2r,并且每个变元正负出现的次数在相等情况下的可满足性问题求解.给出BR(n,k,2r)模型,以此模型来生成具有特殊结构的平衡正则(k,2r)-CNF公式实例,利用随机局部搜索算法求解问题.通过限制初始指派的0文字和1文字各占一半且均匀生成,以WalkSAT算法和NSAT算法做实验对比,发现对于平衡正则(k,2r)-CNF公式,实例具有明显效率.