主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公English
2020-2021年专刊出版计划 微信服务介绍 最新一期:2020年第10期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
许道云,董改芳,王健.MAX(1)和MARG(1)中公式改名的复杂性.软件学报,2006,17(7):1517-1526
MAX(1)和MARG(1)中公式改名的复杂性
Complexities of Renaming for Formulas in MAX(1) and MARG(1)
投稿时间:2004-02-12  修订日期:2005-07-08
DOI:
中文关键词:  计算复杂性  改名  极小不可满足公式
英文关键词:complexity  renaming  minimal unsatisfiable formula
基金项目:Supported by the National Natural Science Foundation of China under Grant Nos.60463001, 10410638 (国家自然科学基金); the Special Foundation for Improving Scientific Research Condition of Guizhou Province of China (贵州省高层次人才科研条件特助经费);the Government Foundation of Gu
作者单位
许道云 贵州大,学计算机科学系,贵州,贵阳,550025 
董改芳 内蒙古农业大学,计算机与信息工程学院,内蒙古,呼和浩特,010018 
王健 软件工程国家重点实验室(武汉大学),湖北,武汉,430072 
摘要点击次数: 3355
全文下载次数: 2915
中文摘要:
      改名是一个将变元映射到变元本身或它的补的函数,变元改名是公式变元集合上的一个置换,文字改名是一个改名和一个变元改名的组合.研究CNF公式的改名有助于改进DPLL算法.考虑判定问题"对于给定的CNF公式H和F是否存在一个变元(或文字)改名ψ使得ψ(H)=F?"的计算复杂性.MAX(1)和MARG(1)是极小不可满足公式的两个子类,这两个子类中的公式可以用树表示.树同构的判定问题在线性时间内是可解的.证明了对于MAX(1)和MARG(1)中的公式,文字改名问题在线性时间内可解,变元改名问题在平方次时间内可解.
英文摘要:
      A renaming is a function mapping propositional variable to itself or its complement, a variable renaming is a permutation over the set of propositional variables of a formula, and a literal renaming is a combination of a renaming and a variable renaming. Renaming for CNF formulas may help to improve DPLL algorithm. This paper investigates the complexity of decision problem: for propositional CNF formulas H and F,does there exist a variable (or literal) renaming ψ such that ψ(H)=F? Both MAX(1) and MARG(1) are subclasses of the minimal unsatisfiable formulas, and formulas in these subclasses can be represented by trees. The decision problem of isomorphism for trees is solvable in linear time. Formulas in the MAX(1) and MARG(1), it is shown that the literal renaming problems are solvable in linear time, and the variable renaming problems are solvable in quadratic time.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利