极小不可满足公式在多项式归约中的应用 被引量：24

1

作者 许道云 《软件学报》 EI CSCD 北大核心 2006年第5期1204-1212,共9页

合取范式(CNF)公式F是极小不可满足的,如果F不可满足,并且从F中删去任意一个子句后得到的公式可满足,(r,s)-CNF是限制CNF公式中每个子句恰有r个不同的文字,且每个变元出现的次数不超过s次的公式类,对应的满足性问题(r,s)-SAT指实例公式... 合取范式(CNF)公式F是极小不可满足的,如果F不可满足,并且从F中删去任意一个子句后得到的公式可满足,(r,s)-CNF是限制CNF公式中每个子句恰有r个不同的文字,且每个变元出现的次数不超过s次的公式类,对应的满足性问题(r,s)-SAT指实例公式限制于(r,s)-CNF.对于正整数r≥3,有一个临界函数f(r),使得(r,f(r))-CNF中的公式都是可满足的,而(r,f(r)+1)-SAT却是NP-完全的.函数f是否可计算是一个开问题,除了知道f(3)=3,f(4)=4外,只能估计f(r)的界.描述了极小不可满足公式在CNF公式类之间转换中的作用.为使转换过程中引入较少的新变元,给出了CNF公式到3-CNF公式的一种新的转换方法,对于长度为l(>3)的子句,仅需引入???2l???个新变元.并且,给出了CNF到(r,s)-CNF公式转换以及(r,s)-CNF中不可满足公式构造的原理和方法. 展开更多

关键词 极小不可满足公式 问题 多项式归约 NP-完全 公式构造

在线阅读 下载PDF 职称材料

一个极小不可满足公式子集的构造

2

作者 陈庆燕 姚雷博 《洛阳理工学院学报（自然科学版）》 2011年第4期77-79,87,共4页

对于极小不可满足公式和它的子类的研究是近年来兴起的一个热门方向。极小不可满足公式通过分裂得到的公式保持了极小不可满足性,它的子类的某些性质对于建立在分裂上的归纳证明是很有用的。找到了一个能递归构造的极小不可满足公式的子... 对于极小不可满足公式和它的子类的研究是近年来兴起的一个热门方向。极小不可满足公式通过分裂得到的公式保持了极小不可满足性,它的子类的某些性质对于建立在分裂上的归纳证明是很有用的。找到了一个能递归构造的极小不可满足公式的子类MAX+,并证明这种递归构造方法具有可靠性和完备性,最后给出了一个构造实例。 展开更多

关键词 极小不可满足公式 MAX+(k)公式集 分裂对

在线阅读 下载PDF 职称材料

一个极小不可满足公式子类的等价结构(英文)

3

作者 许道云 《贵州大学学报（自然科学版）》 2001年第2期79-89,102,共12页

研究一个极小不可满足公式子类 (MAX( 1 ) )的等价结构 考虑了MAX( 1 )上的变元改名问题和文字改名问题 此两个问题均可在O(nlog2 (n) )

关键词 极小不可满足公式 变元改名 等价结构 文字改名 MAX(1) O时间

在线阅读 下载PDF 职称材料

一个极小不可满足公式子类改名的复杂性研究

4

作者 陈庆燕 《滨州学院学报》 2011年第6期82-85,共4页

改名规则在创建有效的满足性算法和简化某些消解难例的证明中起到了重要作用,对于一些具有对称结构的难例公式,可以通过改名来降低其证明的复杂性.研究了一个极小不可满足公式子类,给出了该子类的改名算法,并证明了对该子类中改名问题... 改名规则在创建有效的满足性算法和简化某些消解难例的证明中起到了重要作用,对于一些具有对称结构的难例公式,可以通过改名来降低其证明的复杂性.研究了一个极小不可满足公式子类,给出了该子类的改名算法,并证明了对该子类中改名问题可以在多项式时间内判定. 展开更多

关键词 改名 极小不可满足公式 子类 多项式时间

在线阅读 下载PDF 职称材料

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

5

作者 张庆顺 许道云 《贵州大学学报（自然科学版）》 2005年第4期348-358,共11页

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

关键词 变量出现 极小不可满足公式 公式的扩张

在线阅读 下载PDF 职称材料

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

6

作者 李立峰 《西安邮电学院学报》 2009年第5期144-147,共4页

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

关键词 合取范式 极小不可满足子公式 概念格

在线阅读 下载PDF 职称材料

极小不可满足核及其提取

7

作者 徐小萍 《廊坊师范学院学报（自然科学版）》 2011年第5期14-15,共2页

在极小不可满足公式和可满足公式的基础上给出极小不可满足核的定义,并给出用布尔可满足求解器提取不可满足公式的极小不可满足核的方法。

关键词 极小不可满足公式 提取 求解器

在线阅读 下载PDF 职称材料

MAX(1)和MARG(1)中公式改名的复杂性(英文) 被引量：3

8

作者 许道云 董改芳 王健 《软件学报》 EI CSCD 北大核心 2006年第7期1517-1526,共10页

改名是一个将变元映射到变元本身或它的补的函数,变元改名是公式变元集合上的一个置换,文字改名是一个改名和一个变元改名的组合.研究CNF公式的改名有助于改进DPLL算法.考虑判定问题“对于给定的CNF公式H和F是否存在一个变元(或文字)改... 改名是一个将变元映射到变元本身或它的补的函数,变元改名是公式变元集合上的一个置换,文字改名是一个改名和一个变元改名的组合.研究CNF公式的改名有助于改进DPLL算法.考虑判定问题“对于给定的CNF公式H和F是否存在一个变元(或文字)改名,使得(H)=F?”的计算复杂性.MAX(1)和MARG(1)是极小不可满足公式的两个子类,这两个子类中的公式可以用树表示.树同构的判定问题在线性时间内是可解的.证明了对于MAX(1)和MARG(1)中的公式,文字改名问题在线性时间内可解,变元改名问题在平方次时间内可解. 展开更多

关键词 计算复杂性 改名 极小不可满足公式

在线阅读 下载PDF 职称材料

MAX和MARG中公式改名的复杂性(英文)

9

作者 许道云 《南京大学学报（数学半年刊）》 CAS 2006年第2期181-199,共19页

研究了判定问题“对于命题CNF公式F和H,是否存在一个变元(或文字)改名(?),使得(?)(F)=H?”的复杂性．对于极小不可满足公式的子类MAX和MARG,我们证明了:其变元改名和文字改名的复杂性等价于图同构问题GI．

关键词 复杂性 变元改名 文字改名 极小不可满足公式 图同构

在线阅读 下载PDF 职称材料

MU(1)内公式改名的多项式可判定性(英文)

10

作者 许道云 《贵州大学学报（自然科学版）》 2003年第1期9-19,35,共12页

研究判定合取范式公式F和H之间是否存在一个改名 φ使得 φ(F) =H的计算复杂性。公式的改名是将命题变元映到变元本身或变元的否定的一个映射 ,对于极小不可满足公式的子类MU( 1 )中的公式 ,我们证明了其改名判定问题在多项式时间内是... 研究判定合取范式公式F和H之间是否存在一个改名 φ使得 φ(F) =H的计算复杂性。公式的改名是将命题变元映到变元本身或变元的否定的一个映射 ,对于极小不可满足公式的子类MU( 1 )中的公式 ,我们证明了其改名判定问题在多项式时间内是可判定的。 展开更多

关键词 MU(1)内公式 多项式可判定性 极小不可满足公式 计算复杂性 变元 映射 改名

在线阅读 下载PDF 职称材料

MAX+ (k)中公式改名的多项式时间可判定性(英文)

11

作者 陈庆燕 许道云 《贵州大学学报（自然科学版）》 2005年第2期184-192,共9页

MAX+ (k)是极小不可满足公式的一个子类。作者引入了MAX+ (k)中公式的一种递归构造方法, 基于分裂技术并通过证明MAX(1)中公式改名问题在多项式时间内可以判定。证明了MAX+ (k)中公式的改名问题在多项式时间内可以判定。

关键词 判定问题的复杂性、改名、极小不可满足公式、MAX^+(k)-公式

在线阅读 下载PDF 职称材料

k-LSAT(k≥3)是NP-完全的(英文) 被引量：5

12

作者 许道云 邓天炎 张庆顺 《软件学报》 EI CSCD 北大核心 2008年第3期511-521,共11页

合取范式(conjunctive normal form,简称CNF)公式F是线性公式,如果F中任意两个不同子句至多有一个公共变元.如果F中的任意两个不同子句恰好含有一个公共变元,则称F是严格线性的.所有的严格线性公式均是可满足的,而对于线性公式类LCNF,... 合取范式(conjunctive normal form,简称CNF)公式F是线性公式,如果F中任意两个不同子句至多有一个公共变元.如果F中的任意两个不同子句恰好含有一个公共变元,则称F是严格线性的.所有的严格线性公式均是可满足的,而对于线性公式类LCNF,对应的判定问题LSAT仍然是NP-完全的.LCNF≥k是子句长度大于或等于k的CNF公式子类,判定问题LSAT≥k的NP-完全性与LCNF≥k中是否含有不可满足公式密切相关.即LSAT≥k的NP-完全性取决于LCNF≥k是否含有不可满足公式.S.Porschen等人用超图和拉丁方的方法构造了LCNF≥3和LCNF≥4中的不可满足公式,并提出公开问题:对于k≥5,LCNF≥k是否含有不可满足公式?将极小不可满足公式应用于公式的归约,引入了一个简单的一般构造方法.证明了对于k≥3,k-LCNF含有不可满足公式,从而证明了一个更强的结果:对于k≥3,k-LSAT是NP-完全的. 展开更多

关键词 线性CNF公式 不可满足性 NP-完全性 极小不可满足公式 归约

在线阅读 下载PDF 职称材料

一个从k-CNF到t-CNF归约的有效算法 被引量：7

13

作者 王健 许道云 《南京大学学报（数学半年刊）》 CAS 2005年第1期53-65,共13页

根据极小不可满足公式的特征,对于固定的3 ≤t＜k.我们给出了一个将k-CNF公式归约到t-CNF公式的有效算法.对于给定的k-CNF公式F,t-CNF公式的转换可以在公式F的长度的线性时间内完成.

关键词 极小不可满足公式 归约 算法

在线阅读 下载PDF 职称材料

HITMU(2)的结构和复杂度 被引量：2

14

作者 徐小萍 丁德成 《襄樊学院学报》 2004年第5期3-6,共4页

SAT问题(可满足性问题)是计算机科学的核心问题,研究SAT问题的方法很多,利用极小不可满足公式的性质来研究SAT问题是近几年兴起的一个热点研究方向. 本文主要利用1(,)*-消解和分裂方法研究了差为2的碰撞极小不可满足公式集()2(MUHIT-)... SAT问题(可满足性问题)是计算机科学的核心问题,研究SAT问题的方法很多,利用极小不可满足公式的性质来研究SAT问题是近几年兴起的一个热点研究方向. 本文主要利用1(,)*-消解和分裂方法研究了差为2的碰撞极小不可满足公式集()2(MUHIT-)的结构和复杂度.此前,只有G.Davydov, I.Davydova 和H.Kleine Büning对)1(MU和)2(MU的结构和复杂度得出了较好的结果. 展开更多

关键词 差为2的碰撞极小不可满足公式 HIT-MU(2)的结构 复杂度

在线阅读 下载PDF 职称材料

MAX-k-SAT的PTAS归约等价性

15

作者 许道云 秦永彬 《计算机科学与探索》 CSCD 2009年第6期641-648,共8页

通过构造适当的极小不可满足公式,利用子句拼接技术,引入了一个一般化的从k-CNF公式(k≥3)到3-CNF公式之间的归约转换。基于该转换,给出了一个真值指派的转换算法,并证明了MAX-k-SAT与MAX-3-SAT是PTAS归约等价的。因此,对于k,t≥3,MAX-k... 通过构造适当的极小不可满足公式,利用子句拼接技术,引入了一个一般化的从k-CNF公式(k≥3)到3-CNF公式之间的归约转换。基于该转换,给出了一个真值指派的转换算法,并证明了MAX-k-SAT与MAX-3-SAT是PTAS归约等价的。因此,对于k,t≥3,MAX-k-SAT与MAX-t-SAT是PTAS归约等价的。 展开更多

关键词 极小不可满足公式 归约 MAX—k—SAT问题 PTAS等价

在线阅读 下载PDF 职称材料

MAX-MU(2)的结构和复杂度 被引量：1

16

作者 徐小萍 《襄樊学院学报》 2006年第5期12-15,共4页

SAT问题(可满足性问题)是理论计算机科学的核心问题,研究SAT问题的方法很多,利用极小不可满足公式的性质来研究SAT问题是近几年的一个热点研究方向.文章主要利用(1,*)-消解和分裂方法研究了差为2的极大极小不可满足公式集(MAX-MU(2))的... SAT问题(可满足性问题)是理论计算机科学的核心问题,研究SAT问题的方法很多,利用极小不可满足公式的性质来研究SAT问题是近几年的一个热点研究方向.文章主要利用(1,*)-消解和分裂方法研究了差为2的极大极小不可满足公式集(MAX-MU(2))的结构和复杂度. 展开更多

关键词 差为2的极大极小不可满足公式 SAT问题 (1 ＊)-消解

在线阅读 下载PDF 职称材料

MARG-MU(2)的结构和复杂度

17

作者 徐小萍 《井冈山大学学报（自然科学版）》 2009年第2期30-33,共4页

SAT问题(可满足性问题)是理论计算机科学的核心问题,研究SAT问题的方法很多,利用极小不可满足公式的性质来研究SAT问题是近几年兴起的一个热点研究方向。本文主要利用(1,*)-消解方法研究了差为2的边缘极小不可满足公式集(MARG-MU(2))的... SAT问题(可满足性问题)是理论计算机科学的核心问题,研究SAT问题的方法很多,利用极小不可满足公式的性质来研究SAT问题是近几年兴起的一个热点研究方向。本文主要利用(1,*)-消解方法研究了差为2的边缘极小不可满足公式集(MARG-MU(2))的结构和复杂度:在结构方面,MARG-MU(2)中的公式要么是F22,要么是某一文字在其中仅出现一次的公式;在复杂度方面,如果MARG-MU(2)对(1,*)-消解封闭,则某个含有n个变元和n+2个子句的公式是否为MARG-MU(2)中的公式的问题可以在时间O(n3)内被判定。 展开更多

关键词 极小不可满足公式 可满足性问题 边缘 消解

在线阅读 下载PDF 职称材料

集合MU的某些子类间的包含关系

18

作者 徐小萍 《襄樊学院学报》 2008年第8期11-14,39,共5页

通过具体公式在增加或删去某些文字或子句后生成的新公式的可满足性来研究极小不可满足公式类的常见子类Dis-MU,HIT-MU,Unique-MU,MARG-MU,MAX-MU和SYM-MU之间的包含关系.

关键词 极小不可满足公式 真值指派 包含关系

在线阅读 下载PDF 职称材料

用于求解正则(3,4)-SAT实例集的修正警示传播算法 被引量：2

19

作者 佘光伟 许道云 《计算机科学》 CSCD 北大核心 2018年第11期312-317,共6页

利用极小不可满足公式的临界特性,可以将任意的一个3-CNF公式多项式时间归约转换为一个正则(3,4)-CNF公式,从而得到一个保留NP完全性的正则(3,4)-SAT问题。警示传播算法(Warning Propagation,WP)在归约转换后的正则(3,4)-SAT实例集上高... 利用极小不可满足公式的临界特性,可以将任意的一个3-CNF公式多项式时间归约转换为一个正则(3,4)-CNF公式,从而得到一个保留NP完全性的正则(3,4)-SAT问题。警示传播算法(Warning Propagation,WP)在归约转换后的正则(3,4)-SAT实例集上高概率收敛,但在任意一个实例上都无法判断公式的可满足性,因此算法求解失效。对于一个归约转换后的正则(3,4)-CNF公式,每一变元出现的正负次数之差具有趋于稳定的结构特征,基于该特征,提出基于变元正负出现次数规则的WP算法来求解归约转换后的正则(3,4)-SAT实例。实验结果表明,修正的WP算法对正则公式的可满足性判定有效,从而可以利用公式的正则性特征进一步研究WP算法的收敛性特征条件。 展开更多

关键词 极小不可满足公式 正则(3 4)-SAT问题 警示传播算法

在线阅读 下载PDF 职称材料