间接使用扩展规则求解#SAT问题

针对求解#SAT问题时算法时间会随着子句集的规模迅速增加的问题,提出一种间接应用扩展规则的MCEHST算法。该算法首先求出子句集的所有极小碰集,然后应用扩展规则计算这些极小碰集所能扩展出的极大项的数量,即模型数。实验结果表明:MCEHST算法运行时间随子句集规模增加的速度要比CDP和CER算法慢;当子句的长度较短、子句数较多时,MCEHST算法的时间效率较高。     

基于满足性判定的布尔网络环求解算法

环是布尔网络状态转换过程中的稳定态,在模式检测、基因调控网络和可达性分析等领域都有重要的意义。计算布尔网络状态转换中的所有环是一个NP完全问题。该文基于全解布尔满足性判定(SAT)算法,设计了一种求解所有小于等于指定步长环的算法。算法基于布尔网络的状态转换函数和状态环属性生成合取范式形式(CNF)的问题集,通过融合冲突子句学习(CDCL)、非时序回退、阻塞子句和变量分类等技术,降低算法的计算复杂度。实验结果表明,该算法能够高效地计算指定步长的环。对于无法计算所有环的复杂网络,指定步长计算环的方式将更有应用价值。     

求解公式关键文字集的信息传播算法

关键文字集影响判定布尔公式可满足性的判定难度。如果能找到公式的关键文字集或关键文字集的子集,就可使公式的可满足性判定变得容易。通过对警示传播算法的原理分析,发现高概率决定的部分变元对公式的求解难度有一定的影响。当某个子句与变元之间的警示信息具有一致性时,表明该子句的可满足性完全由该变元的取值决定,其它变元的取值都不能使得该子句可满足。进一步研究发现,当该算法收敛时,具有一致性的警示信息对应的变元集合是关键文字集的子集,这就佐证了警示传播算法可用于求解公式的关键文字集。基于该算法的特征,给出了一个寻找公式关键文字集的信息传播算法。     

一种寻找极小不可满足子公式的方法

用F表示经典命题逻辑的合取范式(CNF)公式,Ci为F中的子句。公式F是极小不可满足的,如果F不可满足,并且从F中删去任意一个子句后得到的公式可满足。本文在经典命题逻辑中引入由F所诱导的形式背景,并基于此建立了概念格;给出了F不可满足公式的判定方法,当F为不可满足公式时,运用概念格的方法从F及其子句集的关系出发给出了F极小不相容子公式的判定定理。     

基于格局检测的并行模型计数方法

在经典的可满足性问题求解中,针对处理模型数较少的实例,SWcc迭代法和SWcc优化增量法与完备的模型计数方法相比,求解适用性更高,但SWcc迭代法和SWcc优化增量法均为串行求解方法,没有对解空间进行剪枝、化简等处理。本文基于此设计了基于格局检测的并行模型计数算法。该算法以化简解空间和启发式为核心,将原解空间分解成为若干子空间并对原子句集进行化简后,并行处理各个子空间。实验结果表明:对于模型个数较少、公式规模较大的问题,该算法比原算法更具有适用性。     

隐蔽集求解的相关问题分析

SAT命题可满足性问题的隐蔽集作为引导搜索SAT问题的关键决策变量,可以优化SAT问题的求解,成为人工智能方向的研究热点之一。本研究对SAT问题隐蔽集中的若干问题进行研究,分别从隐蔽集的概念、隐蔽集的分类进行全面分析,提出影响求解隐蔽集大小的相关因素,论述隐蔽集的参数复杂性与问题难度的关系。     

利用一种SAT问题全解算法求Trivium可滑动对

Trivium是进入到eSTREAM计划最终方案的一个序列密码体制,而在其初始化过程中存在可滑动对。SAT求解器可以有效地求解非线性方程组,然而一般的SAT求解器在求出一个解之后便会结束。对MiniSAT求解器中的算法进行改进,使之可以得出方程所有解。将改进的算法应用于Trivium中可滑动对的求解,得到了初始化拍数从111到120的所有可滑动对。相比于使用Grobner基方法,求解效率有了极大的提高。     

基于超扩展规则的动态在线推理算法

为了提高扩展规则的扩展性能,提出了超扩展规则,并证明了其与扩展负超归结之间的关联关系。KCER算法中使用扩展规则扩展子句,利用超扩展规则替换扩展规则能够更清晰地展示扩展过程,因此提出了基于超扩展规则的动态在线推理算法IKCCER。IKCCER采用离线编译和在线推理过程交互执行的方式,在保持推理效率不变的同时,其空间复杂性为KCCER算法空间复杂性的2/(n+1),其中n为输入子句集的子句数。     

云环境下网络感知的虚拟机分配问题的求解方法

提出了一种云环境下网络感知的虚拟机分配问题的求解方法,该方法能求解带有任务优先级和强制任务的最大虚拟机分配问题等5类问题。该方法通过将虚拟机分配问题编码成对应的SAT类问题,并调用现有的SAT类求解器进行求解,可以更有效地解决较大规模的虚拟机分配问题。最后,通过实验验证了本文算法的合理性和有效性。通过与现有算法在以上5类问题中进行对比,表明了本文算法具有更高的求解效率和更大的求解规模。     

基于符号模拟和变量划分的SAT算法

针对SAT算法中回溯次数较多的问题,采用基于符号模拟和变量划分的方法来解决其不足.基于符号模拟和变量划分的SAT算法将一个较大的CNF分解为两个子集,每个子集所包含的变量又划分为两个互不相交的子集,仅对那些无法判断的子集,赋以符号值,从而限定了赋予符号值的变量范围,即可减少算法的回溯次数,又能降低内存占用率.理论及实验结果均证明,该算法是合理且有效的.     

A polynomial-time algorithm for reducing the number of variables in MAX SAT problem

Maximum satisfiability (MAX SAT) problem is an optimization version of the satisfiability (SAT) problem. This problem arises in certain applications in expert systems and knowledge base revision. MAX SAT problem is NP-hard Some algorithms can solve this problem, but they are not adapted to the special cases where the number of variables is larger than the number of clauses. Usually, the number of variables has great impact on the efficiency of these algorithms. Thus, a polynomial-time algorithm is proposed to reduce the number of variables. Let T be any instance of the MAX SAT problem. The algorithm transforms T into another instance P of which the number of variables is smaller than the number of clauses of T. Using other algorithms, the optimal solution to P can be found, and it can be used to construct the optimal solution of T. Therefore, this algorithm is an efficient preprocessing step.     

用布尔可满足性验证逻辑电路的等价性

提出了使用布尔可满足性来验证数字电路的等价性验证方法.这一验证方法把每个电路抽象成一个有限状态机,为两个待验证的电路构造积机,把等价性验证问题转换成了积机的断言问题.改进了Tseitin变换方法,用于把电路约束问题变换成合取范式公式.用先进的布尔可满足性求解器zChaff判定积机所生成的布尔公式的可满足性.事例电路验证说明了该方法的有效性.     

地球物理资料非线性反演方法讲座（十一）模拟原子跃迁反演法

模拟原子跃迁反演法源于原子物理学,它模拟了物理学中原子从激发态向基态跃迁的物理过程。模拟原子跃迁反演算法的基本思想是：将地球物理反演理论中的反演目标函数生成目标能级函数,然后通过能级跃迁过程使模拟的系统最终达到系统能级最小值的过程。模拟原子跃迁反演法是利用了地球物理反演问题求解过程与原子中能级跃迁过程的相似性建立的一种新的地球物理反演方法。本讲座概要地介绍了模拟原子跃迁法的基本原理、目标能级化过程、能级跃迁、模型搜索及解的接受准则及模拟原子跃迁法的实现过程,并给出了模拟原子跃迁法对典型测试函数和大地电磁资料反演,最后总结和归纳了模拟原子跃迁法的特点。     

用AIG推理检验组合电路的等价性

大部分基于SAT的组合电路等价性检验方法是将两个待检验的电路组合成一个miter电路,将这个电路变换成CNF形式,然后调用一个SAT判定器来确定这个CNF是否是可满足的．但是,当miter电路被变换成CNF之后,就丢掉了电路的结构信息．针对这种方法的不足,先假定miter的输出为1,然后从miter的输出端开始,回溯检查是否存在冲突来判定miter的可满足性．利用AIG的特点,把每个节点的四种输入组合归结为一种,从而使推理得到了简化．实验表明,此方法有更快的处理速度．     

采用正交免疫克隆粒子群算法求解SAT问题

根据Kennedy和Eberhart提出的二进制粒子群算法,基于抗体克隆选择理论提出一种求解合取范式可满足问题的粒子群算法——正交免疫克隆粒子群算法．该算法将合取范式可满足问题转换为求解目标函数最小值的优化问题,为提高收敛速度,根据子句的先验知识计算出个体的初始指派概率对种群进行初始化．为了避免算法早熟收敛,提高粒子群个体解分布的均匀性,将离散正交交叉算子用于免疫基因操作中,并给出适应于求解合取范式可满足问题的免疫粒子群进化算子．实验采用标准SATLIB库中变量个数从20~250的3700个不同规模的标准合取范式可满足问题对正交免疫克隆粒子群算法的性能作了全面的测试,并与标准粒子群算法和免疫克隆选择算法进行了比较．结果表明,正交免疫克隆粒子群算法的成功率在3个算法中最高,运行时间和评价次数最少．     

Two phase clustering method for CNF clauses

Aimed at the Boolean clauses clustering, a two phases clustering method for CNF clauses is proposed. At the beginning, each clause is treated as a cluster. In the first phase, by a link based clustering method, the common neighbors between two clusters is used to determine how to merge the clusters. In the second phase, a similarity based clustering method is used. The first phase uses a global view to cluster the clauses, so the global optimum can be achieved in some sense. The second phase uses similarity to merge clusters, so the setting of the number of the final clusters in the algorithm is unnecessary. Experimental results show that the proposed method can lead to better clustering results with fewer common variables.     

基于多染色体演化的自适应类别数聚类方法

为了解决在遗传算法聚类分析中影响算法效率的互相关性问题以及在没有先验知识的情况下确定类别数问题,在充分分析基因的互相关性对算法效率和收敛性影响的基础上,借鉴多染色体生物的进化特性,提出多染色体取代传统单染色体的遗传算法.算法在进化过程中充分利用类簇之间的相互关系,提高了遗传算法的效率和收敛能力,并且在遗传过程中类别数量可变;为了明确地控制类别数,采用基于分布拟合的适应度函数,为在没有先验知识的情况下确定类别数提供了分析依据.通过与K均值的遗传算法（KGA）、最大期望算法（EM算法）的对比分析以及针对遥感影像的实验表明,该遗传算法在对类别数能进行自适应控制的基础上,在效率和收敛性上也都能取得较好的效果.     

多用户多径长码DS-CDMA系统参数估计CRB和MCRB

多用户参数估计直接影响了多用户检测算法的性能。在多用户多径长码直接序列码分多址（DS-CDMA）系统下,首先推导出已知激活用户导频比特和扩频码时,多用户相位、时延和幅度参数联合估计的Cramer-Rao界（CRB）;然后给出了当激活用户导频比特和扩频码未知时,把激活用户扩频码看作随机变量,参数联合估计的修正CRB（MCRB）。数据仿真结果显示了导频比特长度、信噪比和激活用户个数对CRB和MCRB的影响;同时与单径长码DS-CDMA系统参数联合估计CRB和MCRB做了仿真比较。