可满足性(SAT)问题的概率研究

本文首先构造了随机均匀产生的ｄ－ＳＡＴ问题的概率模型；然后给出了ＳＡＴ问题的解的个数的均值的计算公式．使用矩方法研究了解空间的元素满足方程的概率以及在临界点方程有解的概率的极限性质．最后确定了ｎ／ｍ＝ｒｄ＝（ｌｎ２）／（ｌｎ（２ｄ／２ｄ－１） ）是其解的平均个数的临界点，并且当 ｎ／ｍ＝ｒｄ时，方程有解的概率随着ｍ→∞而趋于０．

基于可满足性问题求解器的星上FPGA永久损伤容错技术研究

现代卫星广泛使用的FPGA在空间高能粒子的影响下,会产生门电路的永久性损伤。而传统的三模冗余等容错方法不但成倍增加了系统硬件开销,还存在因冗余器件耗尽而失效的风险。因此,提出一种利用FPGA自身冗余资源,修复永久性损伤的容错方案。该方案通过建立FPGA内部资源的功能模型,将容错问题转化为数学上的可满足性问题。并且利用经过改进的GSAT算法对该问题求解,可以获得在功能上与损伤前完全相同的电路结构,及其所对应的FPGA配置文件。将该文件重新下载到FPGA中,可以屏蔽损伤带来的影响,从而达到利用FPGA自身冗余资源容错的目的。通过实验和分析可以看出,本文方案具有对损伤修复成功率高、计算量小和需要内存空间少的特点,因此符合星上计算能力和硬件资源十分有限的实际情况。

可满足性问题的三维DNA图结构算法

论文提出用三维图结构解决DNA分子计算问题,给出了解决3-SAT问题的方法。在所提出的方法中,算法所要求的步骤与公式中变量的数目相等。

求解SAT问题的拟人退火算法

该文利用一个简单的变换 ,将可满足性 (SAT)问题转换为一个求相应目标函数最小值的优化问题 ,提出了一种用于跳出局部陷阱的拟人策略 .基于模拟退火算法和拟人策略 ,为 SAT问题的高效近似求解得出了拟人退火算法 (PA) ,该方法不仅具有模拟退火算法的全局收敛性质 ,而且具有一定的并行性、继承性 .数值实验表明 ,对于本文随机产生的测试问题例 ,采用拟人策略的模拟退火算法的结果优于局部搜索算法、模拟退火算法以及近来国际上流行的 WAL KSAT算法 。

组织进化算法求解SAT问题

基于组织的概念设计了一种新的进化算法———求解SAT问题的组织进化算法 (OrganizationalEvolution aryAlgorithmforSATproblem ,OEASAT) .OEASAT将SAT问题分解成若干子问题 ,然后用每个子问题形成一个组织 ,并根据SAT问题的特点设计了三种组织进化算子———自学习算子、吞并算子和分裂算子以引导组织的进化 .根据组织的适应度 ,将所有组织分成两个种群———最优种群和非最优种群 ,然后用进化的方式来控制各算子 ,以协调各组织间的相互作用 .OEASAT通过先解决子问题 ,再协调相冲突变量的方式来求解SAT问题 .由于子问题的规模较小 ,相对于原问题来说较容易解决 ,这样就达到了降低问题复杂度的目的 .实验用标准SATLIB库中变量个数从 2 0～ 2 5 0的 370 0个不同规模的标准SAT问题对OEASAT的性能作了全面的测试 ,并与著名的WalkSAT和RFEA2的结果作了比较 .结果表明 ,OEASAT具有更高的成功率和更高的运算效率 .对于具有 2 5 0个变量、10 6 5个子句的SAT问题 ,OEASAT仅用了 1.5 2 4s,表现出了优越的性能 .

一种求解难SAT问题的改进DP算法

DP算法是求解SAT问题的最有效完全算法之一 ,论文分析和讨论了DP算法中的各种分枝文字策略 .并基于对不满足解数估计的方法 ,提出了一个有效的分枝文字策略 .实验结果表明 ,提出的改进DP算法对难SAT实例有较好的平均性能 .

基于离散Lagrange方法的分布式SAT问题求解

基于对离散Lagrange方法(DLM)的扩充,提出一个分布式SAT求解算法:EDLMSAT。求解过程中,单个Agent的行为由预先定义的EDLM规则所决定,这些局部的行为聚集起来,形成整个系统对问题的求解趋势。设计了一些对3＿SAT基准问题的模拟实验,实验结果表明了这个算法良好的求解性能。

基于海明距的改进免疫算法及其在SAT中的应用

免疫算法可以克服遗传算法的早熟和发散现象,是一种有效的全局寻优算法.针对传统基于信息熵的免疫算法的浓度计算中含有过多的对数计算,浪费了机时,影响了免疫算法效率的缺陷;本文提出了一种基于海明距与加速免疫进化的变异算子的改进免疫算法,证明了基于海明距与基于信息熵的浓度定义在控制中所起的作用是等效的,并将这种改进算法应用于SAT求解.实验结果表明,改进的免疫算法在求解速度,成功率等方面都有明显的改善.

Survey Propagation:一种求解SAT的高效算法

Survey ProPagation是一种新生的SAT(CSP)算法。它基于统计物理的sPin glass 模型,针对具体问题进行纵览(survey),从而极大地降低求解的复杂度。但sp算法在某些时候不收敛,或引导向错误的解。对此,G.Parisi提出一种复杂回溯(backtrack)算法,而作者在sp中加入简单回溯,也使一部分此类问题得到解决。

无界模型检验中融合电路信息的SAT算法研究

针对从电路转化而来的SAT问题,通用SAT求解器存在一个缺陷——电路互连信息的缺失,这是造成很多无关推导的根源.文中提出了一个统一的基于CNF数据结构的电路SAT无界模型检验框架.首先作者提出了定值子句的概念,利用这一概念可以在CNF结构中保存电路的互连信息,在搜索过程中更早地识别可满足解,减少不必要的搜索.其次,文中提出了在CNF结构上的状态变量赋值精简方法,摆脱了以往基于SAT的无界模型检验中这一步骤对门级电路结构的依赖.实验数据表明,利用文中方法进行前像计算能够取得明显的加速.同时,文章比较了两种搜索顺序在多时帧搜索中的效果.实验结果表明利用文中方法可以验证传统模型检验方法难以验证的复杂电路属性.

描述逻辑程序系统的设计与实现

Eiter等人为语义网提出的回答集程序和描述逻辑相结合的描述逻辑程序,获得了本体上的非单调表达和推理能力。王以松等人证明了描述逻辑程序的完备化和环公式可以精确刻画描述逻辑程序的回答集。在此基础上,进一步证明了若完备化公式的模型不是回答集则一定存在终止环公式反例,它们是多项式时间可计算的。设计并实现了借助SAT求解器MiniSAT以及描述逻辑推理机RacerPro计算描述逻辑强回答集的原型DLP_SAT。实验结果表明,该原型能有效地计算一些熟知的描述逻辑程序的强回答集。