• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Conference on Theory and Applications of Satisfiability Testing(SAT 2005); 20050619-23; St Andrews(GB) >Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas
【24h】

Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas

机译：预处理CNF公式的经济高效的超分辨率

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

摘要

We present an improvement to the HYPRE preprocessing algorithm that was suggested by Bacchus and Winter in SAT 2003. Given the power of modern SAT solvers, HYPRE is currently one of the only cost-effective preprocessors, at least when combined with some modern SAT solvers and on certain classes of problems. Our algorithm, although it produces less information than HYPRE, is much more efficient. Experiments on a large set of industrial Benchmark sets from previous SAT competitions show that HYPERBINFAST is always faster than HYPRE (sometimes an order of magnitude faster on some of the bigger CNP formulas), and achieves faster total run times, including the SAT solver's time. The experiments also show that HYPERBiNFAST is cost-effective when combined with three state-of-the-art SAT solvers.
机译：我们提出了Bacchus和Winter在SAT 2003中提出的对HYPRE预处理算法的改进。鉴于现代SAT求解器的强大功能，HYPRE当前是唯一具有成本效益的预处理器之一，至少与某些现代SAT求解器和关于某些类别的问题。我们的算法虽然产生的信息少于HYPRE，但效率更高。在之前的SAT比赛中对大量工业基准测试集进行的实验表明，HYPERBINFAST总是比HYPRE快（有时在某些较大的CNP公式上快一个数量级），并且可以获得更快的总运行时间，包括SAT求解器的时间。实验还表明，将HYPERBiNFAST与三个最新的SAT求解器结合使用时，具有成本效益。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号