• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of computer and system sciences >A sharp threshold in proof complexity yields lower bounds for satisfiability search
【24h】

A sharp threshold in proof complexity yields lower bounds for satisfiability search

机译：证明复杂性的严格阈值会产生可满足性搜索的下限

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Let F(rhon, Deltan) denote a random CNF formula consisting of rhon randomly chosen 2-clauses and Deltan randomly chosen 3-clauses, for some arbitrary constants rho, Delta greater than or equal to 0. It is well-known that, with probability 1 - o(1), if rho > 1 then F(rhon, Deltan) has a linear-size resolution refutation. We prove that, with probability 1- o(1), if rho < 1 then F(rhon, Deltan) has no subexponential-size resolution refutation. Our result also yields the first proof that random 3-CNF formulas with densities well below the generally accepted range of the satisfiability threshold (and thus believed to be satisfiable) cause natural Davis-Putnam algorithms to take exponential time (to find a satisfying assignment). (C) 2003 Published by Elsevier Inc. [References: 36]
机译：令F（rhon，Deltan）表示一个随机CNF公式，该公式由rhon随机选择的2个子句和Deltan随机选择的3个子句组成，对于某些任意常数rho，Delta大于或等于0。概率为1-o（1），如果rho> 1，则F（rhon，Deltan）具有线性大小的分辨率反驳。我们证明，当概率为1 o（1）时，如果rho <1，则F（rhon，Deltan）没有次指数大小的分辨率反驳。我们的结果还提供了第一个证明，即密度远低于可满足性阈值的公认范围（因此被认为是可满足的）的随机3-CNF公式导致自然的Davis-Putnam算法花费指数时间（以找到令人满意的赋值） 。 （C）2003年由Elsevier Inc.出版。[参考：36]

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号