一次性求解多个SAT问题

在实际应用中通常需要求解对应CNF(Conjunctive Normal Form)公式之间仅相差几个子句的一系列SAT(Satisfiability Problem)问题,但目前绝大多数SAT求解算法都是针对单一SAT问题设计的。为此,基于DPLL提出了nDPLL算法,并在随机问题上对该算法的效率进行测试。实验结果表明,nDPLL算法能一次性求解多个SAT问题,对于特定范围的CNF公式集具有较高的效率,CNF公式集的规模越大、相近因子越高、子句数和变量数的比值越大,则nDPLL算法的效率越高。     

一种增加了对称破缺的改进子集可满足性算法

为了消除子集可满足性算法在布线过程中带来运行时间增加的负面影响,提出了一种新的布线流程.针对子集可满足性算法在求解同时增加额外的变量和字句,而使得对称数量按指数级增长的问题,选用增加静态对称破缺的方法对合取范式(CNF)进行预处理,侦测并破缺其中的对称,从而达到减少搜索路径的目的.用简化图自同构的方法侦测所有对称,在增加合适的对称破缺判定(SBPs)后,限制搜索在空间的非对称领域进行,从而减少了搜索空间,而不影响CNF公式的可满足性.然后把预处理过的CNF送入布尔可满足性(SAT)解法器进行求解.试验结果表明,这种方法可以显著减少运行时间,加速求解过程.     

一个求解SAT问题的随机算法

本文中引入了一个求解满足性问题的随机算法。在该算法中,利用CNF公式转换为其对偶式——DNF公式,通过对满足DNF公式的真值赋值数Y作出估计。根据Y与2n比较结果,对CNF公式的可满足性进行估计并对其满足性进行判断。     

基于混合蚁群遗传算法的SAT问题求解

根据SAT问题的特点,通过分析传统蚁群算法和遗传算法在求解SAT问题上的不足,提出一种基于混合蚁群遗传算法的SAT问题求解方法。给出一种新的初始解的生成方式;在迭代过程中,根据较优解的累积信息提出进化算子;利用当前得到的最优解,通过改变不满足子句中文字的取值,增加变异算子。最后选取标准测试集中的20个实例对算法进行测试,实验结果表明:改进后的算法通常仅通过较少次数的迭代就能找到解,能够有效避免蚁群算法和遗传算法过早收敛的缺点,具有较强的寻优能力。     

DPLL算法及其改进的新方法

对命题公式可满足性问题的判别方法进行了深刻的剖析,基于启发式算法,定义命题公式的核心文字,通过改进DPLL算法给出求解SAT问题的新方法。     

基于CNF权重学习求解3-SAT问题的进化算法

SAT（Satisfiability）可满足性问题研究具有很广的应用价值,是计算机和人工智能领域内的一个重要问题,也是第一个被证明为NP完全的问题。随着对SAT问题的深入研究,已经提出了很多高效的算法,其中随机算法（WalkSAT）、进化算法等启发式算法是今年来研究的热点。进化算法是遗传算法的一种,通过对生物组织进化的学习,形成的一种高效算法。针对CNF（Coniecture Normal Formula）权重和生物进化算法相结合,提出一种有效求解难SAT问题的不完全算法WOSAT．     

加速混合遗传算法及其在暴雨强度公式参数优化中的应用

根据重现期P-降雨历时t-暴雨强度i的关系表,推求暴雨强度公式参数,是一个已知关系式的非线性模型参数优化求解问题.在理论分析及前人研究的基础上,把求解无约束最优化问题的交尺度DFP算法嵌入到改进浮点编码遗传算法中,得到一种基于变尺度DFP算法和改进浮点编码遗传算法的加速混合遗传算法.该方法兼顾了改进浮点编码遗传算法和DFP算法的优点,既有较快速的收敛速度,又能求得最优化问题全局精确解.经求解暴雨强度公式参数的实例表明,该法是有效的和可行的,且求解结果优于其它方法.     

混合exactly-one约束的模型计数研究

模型计数是求给定命题公式的模型数，是人工智能领域的一个基本问题.在贝叶斯网络、有界模型检测、精确集合覆盖等众多实际问题中，存在许多exactly-one约束.常见的处理方法是将exactly-one约束编码为CNF公式，再调用模型计数器求解.这种方法扩大了命题公式的规模，容易导致求解时间过长.本文分别提出从CNF公式中还原exactly-one约束的ECR算法和处理exactly-one约束的ECP算法.ECR算法能明显提高C2D编译器的求解效率.基于最新的模型计数器ExactMC，本文改进了能识别和单独处理exactly-one约束的模型计数器ECMC.实验结果表明，ECMC的时间效率相比ExactMC有显著提高.     

一个SAT问题有解的充要条件

合取范式可满足性问题(简称SAT问题)是一个NP完全问题.引入了一个饱和合取范式的概念,利用饱和合取范式的性质,对SAT问题的本质进行了研究.在此基础上,证明了一个SAT问题有解的充要条件,它为SAT问题完全算法和非完全快速算法的深入研究提供了一条新的思路.     

可满足公式到极小不可满足公式MU(1)的扩张复杂性

可满足合取范式（CNF）公式F到极小不可满足公式MU（1）的扩张是,对给定的CNF公式F,是否存在一个公式G满足条件var（G）包含var（F）并使得F＋G∈MU（1）。Horn公式到MU（1）公式的扩张问题可在多项式时间内解决,但对一般CNF公式F的扩张问题,至今尚未解决。这里我们将给出一个多项式时间的算法解决这一问题。