CNF公式赋值空间上可满足解的概率性质

为分析合取范式(conjunctive normal form,CNF)公式的赋值空间在可满足性情况下的结构性质,引入一个变元翻转次数控制的参数k,k不小于1且不大于n,n为公式中出现的变元个数,以赋值作为结点,基于翻转界控制下赋值满足子句数的大小,引入一类有向图——BF(bounded flips)图。研究带翻转控制参数的BF图的若干基础性质,根据BF图的性质研究CNF公式可满足解的概率性质。对于含有n个变元m个子句CNF公式,随着翻转控制参数k的增大,在其BF图上取得可满足解的概率也相应增大。当k靠近n时,概率稳定。对于可满足的CNF公式,在其任意k值下的BF图上进行t次随机游走。当t足够大时,取得可满足解的概率最终会收敛于1。最后,实验仿真支持性质的正确性。

2-CNF理论的逻辑差

如何刻画知识库不同版本之间的区别是研究知识库动态更新中的一个重要问题。提出了命题逻辑知识库的逻辑结论差概念(称为逻辑差)。然而,一般知识库之间逻辑差的计算是不易处理的,而且不满足范畴性,即不能保证其结果仍然可以用同类型的知识库来表达;由于2-CNF理论的可满足问题的易处理性,证明了2-CNF理论的逻辑差具有范畴性,并设计了一个多项式时间算法计算它们的逻辑差。

从合取范式到析取范式的转换研究

为了解决粗糙集分辨函数的计算、概念格中内涵缩减的计算、逻辑程序设计的规则简化等问题,抽象出了从合取范式到析取范式转换这一核心问题。提出了利用极小覆盖来实现从合取范式到析取范式的转换,给出了一个增量式的算法。为了扩大范式转换的使用范围,定义了伪合取范式,并给出伪合取范式到析取范式的转换方法。

两类动态信息规律模型及其在信息伪装、风险识别中的应用

函数P-集合是P-集合的函数形式,是通过改进P-集合得到的一个具有动态特征、规律(函数)特征的信息规律模型。在函数P-集合中,函数的属性满足数理逻辑中的合取范式。函数逆P-集合是函数P-集合的对偶模型,在函数逆P-集合中,函数的属性满足数理逻辑中的析取范式。这里定义函数P-集合是一类动态信息规律模型,定义函数逆P-集合是另一类动态信息规律模型;在函数P-集合与函数逆P-集合的结构、动态特征与它们的属性范式特征的基础上,给出函数P-集合在信息图像拼接与伪装中的简单应用,以及函数逆P-集合在商品利润的风险估计-识别中的简单应用。函数P-集合、函数逆P-集合是关于动态信息规律应用研究的新理论、新模型。

双枝模糊逻辑

在双枝模糊集基础上,建立了双枝模糊逻辑的框架,这是对单枝模糊逻辑的合理扩展。从双枝模糊命题入手,给出双枝模糊逻辑的性质和双枝模糊逻辑公式,以及双枝模糊逻辑的析取范式与合取范式。这些结果为研究双枝模糊推理和双枝模糊控制奠定了基础。

一种求解3-SAT问题的新方法

可满足性问题(SatisfiabilityProblem,SAT)是计算科学的典型问题之一,目前有DP算法、SAT1.3算法和遗传算法等多种求解方法。文章根据Kennedy和Eberhart提出的二进制粒子群优化算法(BinaryParticleSwarmOptimizers),基于局部随机搜索策略,给出了一种求解3-SAT问题的新方法:基于局部随机搜索的改进二进制粒子群优化算法(ModifedBinaryParticleSwarmOptimizersBasedonlocalstochasticsearch,简称MBPSO)。数值实验表明,对于随机产生的3-SAT问题测试实例,该算法是一种高效实用的新方法。

基于模型诊断中结合问题特征的新方法

基于模型诊断一直是人工智能领域中热门的研究问题.近些年来,随着SAT求解器效率的逐渐提高,基于模型的诊断也被转换成SAT问题进行求解.在对基于模型诊断求解方法 CSSE-tree深入研究基础上,结合诊断问题和SAT求解过程的特征,给出先对包含组件个数较多的候选诊断进行求解的方法,进而减小SAT求解问题的规模;在对极小诊断解和非极小诊断解剪枝方法的基础上,首次提出非诊断解定理及非诊断解空间的剪枝方法,有效地实现了对诊断的无解空间进行剪枝.根据组件个数较多的候选诊断先求解及有解无解剪枝方法特征,构建基于反向搜索的LLBRS-tree方法.实验结果表明:与CSSE-tree算法相比,LLBRS-tree算法减少了SAT求解次数、减小了求解问题规模,效率较好,尤其是求解多诊断时效率提高更为显著.

双枝模糊逻辑(II)

在双枝模糊集基础上,通过对单枝模糊逻辑的合理扩展,建立了双枝模糊逻辑的框架。从双枝模糊命题入手,给出双枝模糊逻辑的性质和双枝模糊逻辑公式,以及双枝模糊逻辑的析取范式与合取范式。这些结果为研究双枝模糊推理和双枝模糊控制奠定了基础。

求解SAT问题的改进粒子群优化算法

利用限制性公式的相关理论将可满足性问题(SAT)等价转换为定义在{0,1}m上的多项式函数优化问题,并将二进制粒子群优化算法(BPSO)与局部爬山搜索策略相结合,给出了一种求解SAT问题的新算法:基于局部爬山搜索的改进二进制粒子群优化算法(简称IBPSO)。数值实验表明,对于随机产生的3-SAT问题测试实例,该算法的计算结果均优于著名的WalkSAT算法和SAT1.3算法。

基于资源受限的非线性约束多目标排课模型及算法

通过对排课资源和约束规则的分析与描述,提出并建立了一个基于资源受限的非线性约束多目标的排课模型。在该模型中,运用鸽子巢原理对问题是否有解加以判断,利用分治策略将问题分解,用主合取范式寻找所有可选方案,利用析取范式求得排课结果。在排课算法的设计中,综合应用了最小离差平方和法和间隔法。实验及应用证明该排课算法灵活高效,具有较强的冲突解决能力,并能在时空方面确保课表分布的均匀性。

属性约简中的范式转换算法研究

通过研究属性约简中合取范式到析取范式的转换过程,发现减少冗余项和重复计算可以适当提高转换效率。同时考虑到范式的动态变化,设计一种边转换边化简的增量转换算法,可以利用已有结果直接进行计算。对于减量情况,抽象出范式转换的数学模型,给出相应转换的构造形式和分析过程,并提出一种近似减量转换算法,从而实现了不同变化情况下生成析取范式的动态计算。最后通过仿真实验验证了算法的可行性和高效性。

基于粗糙集和SAT算法的属性约简

粗糙集理论是80年代初由波兰数学家Z.Pawlak首先提出的一个分析数据的数学理论。该理论近几年来日益受到各领域的广泛关注,并已在机器学习、模式识别、决策分析、过程控制、数据库知识发现等广泛领域得到成功应用。论文提出了一种求最小约简的基于命题可满足性(简称SAT)算法的算法,提出一个解决SAT问题的分割和结合的算法。实验结果表明,论文所提算法在高度准确分类的基础上,所得约简中大大减少了规则的数目。

高阶Hopfield神经网求解合取范式可满足性问题

本文提出用高阶Hopfield神经网络求解SAT问题，给出了连续及离散高阶神经网络模型与相应的离散快速求解算法，证明了网络的稳定性．并用实验证明了该方法的可行性，且将该算法与LocalSearch算法进行了比较．

多值Lukasiewicz逻辑公式的范式表示和计数问题

将符号化计算树逻辑中的Shannon展开式做了推广,在n值ukasiewicz逻辑系统n中,研究了由逻辑公式导出的n值McNaughton函数的展开式,给出了m元n值McNaughton函数的准析取范式和准合取范式.在此基础上,给出了m元n值McNaughton函数的计数问题,并在n值ukasiewicz逻辑系统n中,给出了m元逻辑公式的构造方法及其逻辑等价类的计数问题.

基于聚类和划分的SAT分治判定

提出了一种将布尔公式划分为子句组来进行布尔可满足性判定的方法.CNF(conjunctive normal form)公式是可满足的当且仅当划分产生的每个子句组都是可满足的,因此,通过判定子句组的可满足性来判定原公式的可满足性,相当于用分治法将复杂问题分解为多个子问题来求解.这种分治判定方法一方面降低了原公式的可满足性判定复杂度;另一方面,由于子句组的判定可以并行,因而判定速度能够得到进一步的提高.对于不能直接产生布尔子句组划分的情形,提出了一种利用聚类技术将CNF公式聚类成多个簇,然后消去簇间的公共变量来产生子句组划分的方法.

MiniSAT求解器在判定可满足性问题中的应用

目前布尔逻辑已成为计算机科学的重要理论基础之一,是研究人类思维规律的重要工具。可满足性问题是典型的NP问题,SAT求解器的开发使得判定可满足性问题更加自动化。以与门电路为例,描述了如何将电路问题转换成可满足性SAT问题并使用MiniSAT求解器进行求解,包括输入格式、选项以及输出格式要求。

主范式的计算方法及其在命题公式中的作用

针对数理逻辑中主范式的求解难度较大、方法繁琐,充分利用极小项与极大项的特征及其与二进制数的关系,综合求解主范式的各种传统方法,给出较为简洁实用的计算方法。同时系统论述两种主范式在命题逻辑中对于理解和分析命题公式诸多方面的作用。

合取范式化为析取范式的DNA表面计算

合取范式化为析取范式的计算复杂度是指数级别的,为了降低它的计算复杂度,提出了合取范式化为析取范式的DNA表面计算.因为DNA中碱基对的配对可以同时进行,所以DNA表面计算具有并行计算能力,它实现了将合取范式化为析取范式的计算复杂度降低到多项式级别.

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

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

线性逻辑方程组的解

软件设计和硬件设计中经常遇见用逻辑方程或逻辑方程组表示的数学模型,讨论这类数学模型的求解问题是非常必要的。给出了=0,=1,=,=1(中不含逻辑非变量,中含逻辑非变量)等类型的线性逻辑方程组有解、有惟一解的充分必要条件,讨论了解的个数并给出了求解公式或解集表示式,阐明了任何形式的逻辑方程或逻辑方程组都可转化为线性逻辑方程组求解。采用置换矩阵和极大项两种方法,系统全面地解决了线性逻辑方程组、一般逻辑方程和一般逻辑方程组的求解问题。