• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Discrete Applied Mathematics >On good algorithms for determining unsatisfiability of propositional formulas
【24h】

On good algorithms for determining unsatisfiability of propositional formulas

机译：关于确定命题公式不满足的好的算法

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

摘要

This paper is concerned with an algorithm that provides short certificates of unsatisfiability with high probability when an input j is a random instance of 3-SAT. Rather than build a refutation DAG, the algorithm finds bounds on nj(true), the number of variables that must be set to true, and nj(false), the number that must be set to false, if all clauses of j are to be satisfied. If the sum nj(true) + nj(false) is greater than the number of variables in j then j must be unsatisfiable. Bounds on nj(true) and nj(false) may be found by throwing out all clauses except those having only negative or only positive literals and finding n_j~+(true) for the remaining positive clause set j~+ and n_(j-)(false) for the remaining negative clause set j~-. These questions can alternatively be stated as 3-hitting set problems on j~+ and j~- separately. It is shown that a good enough approximation algorithm for 3-hitting set can determine useful bounds on n_j(true) and n_j(false) (high probability of success for large enough constant ratio of clauses to variables). Although a good enough algorithm seems evasive, one that comes fairly close is proposed and analyzed.
机译：本文涉及一种算法，当输入j为3-SAT的随机实例时，该算法可提供高概率的短期不满足证书。如果不将j的所有子句都设为nj（true）（必须设置为true的变量数）和nj（false）（必须将其设置为false的数），则算法不会建立反驳DAG，而是找到界限。满意。如果总和nj（true）+ nj（false）大于j中的变量数，则j必须不满足。 nj（true）和nj（false）的界线可以通过抛出所有仅具有负或仅正文字的子句，并为剩余的正子句集j〜+和n_（j- ）（false）表示剩余的否定子句集j〜-。可以选择将这些问题表示为j〜+和j〜-上的三连集问题。结果表明，对于3-hitset而言，足够好的近似算法可以确定n_j（true）和n_j（false）上的有用边界（对于子句与变量的足够恒定的比率，成功的可能性很高）。尽管似乎有足够好的算法可以避免，但仍提出并分析了一种相当接近的算法。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号