极小不可满足公式在多项式归约中的应用
DOI:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

Supported by the National Natural Science Foundation of China under Grant No.60463001(国家自然科学基金);the Special Foundation for Improving Scientific Research Condition of Guizhou(贵州省高层次人才科研条件特助基金);the Special Foundation of Government of Guizhou Province(贵州省省长基金)


Applications of Minimal Unsatisfiable Formulas to Polynomially Reduction for Formulas
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    合取范式(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)的子句,仅需引入|l/2|个新变元.并且,给出了CNF到(r,s)-CNF公式转换以及(r,s)-CNF中不可满足公式构造的原理和方法.

    Abstract:

    A conjunctive normal form (CNF) formula F is minimal unsatisfiable if F is unsatisfiable and the resulting formula removing any clause from F is satisfiable. (r,s)-CNF is a subclass of CNF in which each clause of formula has exactly r distinct literals and every variable occurs at most s times. The corresponding satisfiable problem (r,s)-SAT means that the instances are restricted in (r,s)-CNF. For positive integer r≥3, there exists a critical function f(r) such that all formulas in (r,f(r))-CNF are satisfiable, but (r,f(r)+1)-SAT is already NP-Complete. It is open whether or not the function f is computable. One can only estimate some bounds of f(r) except for f(3)=3 and f(4)=4. In this paper, the applications of minimal unsatisfiable formulas are described for transformations between CNF formulas. A new algorithm is presented to introduce less new variables in transformation from CNF to 3-CNF, which for clauses with length l(>3) only ??????2l new variables are introduced. The principle and method for transforming CNF to (r,s)-CNF and constructing unsatisfiable formulas in (r,s)-CNF are presented.

    参考文献
    相似文献
    引证文献
引用本文

许道云.极小不可满足公式在多项式归约中的应用.软件学报,2006,17(5):1204-1212

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2005-06-15
  • 最后修改日期:2005-12-16
  • 录用日期:
  • 在线发布日期:
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号