主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2019-2020年专刊出版计划 微信服务介绍 最新一期:2019年第2期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
许道云,韦立,王晓峰.鸽巢公式的一些性质.软件学报,2011,22(11):2553-2563
鸽巢公式的一些性质
Some Properties of Pigeon-Hole Formulas
投稿时间:2010-07-07  修订日期:2010-11-03
DOI:10.3724/SP.J.1001.2011.03957
中文关键词:  鸽巢公式  极小不可满足  最大可满足指派  标准形式  子结构同构
英文关键词:pigeon-hole formula  minimal unsatisfiability  maximal satisfiable assignment  normal form  substructure isomorphism
基金项目:国家自然科学基金(60863005, 61111130186)
作者单位E-mail
许道云 贵州大学 计算机科学系,贵州 贵阳 550025 dyxu@gzu.edu.cn 
韦立 贵州大学 计算机科学系,贵州 贵阳 550025  
王晓峰 贵州大学 计算机科学系,贵州 贵阳 550025  
摘要点击次数: 3385
全文下载次数: 3097
中文摘要:
      由鸽巢原理定义的鸽巢公式PHnn+1 是著名的消解难例之一,研究该公式的结构和性质有助于其他难例的构造.证明了PHnn+1 是一个极小不可满足公式,根据其极小不可满足性,给出了最大可满足真值指派的两种标准形式,Haken 关于PHnn+1 的难解证明用到了其中一种标准形式.公式PHnn+1 具有良好的子结构同构性质,如果DPLL 算法中允许使用同构规则,则存在PHnn+1 的反驳证明,其复杂性可以降至O(n3).
英文摘要:
      The pigeon-hole formula PHnn+1, defined from the pigeon hole principles, is one of the hardest examples on resolution. The research of the formula’s constructions and properties is helpful for constructing other hard examples. It is shown that PHnn+1 is a minimal unsatisfiable formula. The two normal forms of maximal satisfiable truth assignments for PHnn+1 are presented by the minimal unsatisfiability of PHnn+1, which one of normal forms is used in Haken’s proof of hardness for PHnn+1. The formula PHnn+1 has well isomorphics properties on substructures. For the modified DPLL algorithm introduced by the isomorphism rule, the complexity of refutation proof of PHnn+1 can be reduced to O(n3).
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

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