• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Proceedings of the 46th Annual Design Automation Conference >Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts
【24h】

Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts

机译：使用DPLL，图形和观察切口对非子句公式进行有效的SAT求解

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

摘要

Boolean satisfiability (SAT) solvers are used heavily in hardware and software verification tools for checking satisfiability of Boolean formulas. Most state-of-the-art SAT solvers are based on the Davis-Putnam-Logemann-Loveland (DPLL) algorithm and require the input formula to be in conjunctive normal form (CNF). We present a new SAT solver that operates on the negation normal form (NNF) of the given Boolean formulas/circuits. The NNF of a formula is usually more succinct than the CNF of the formula in terms of the number of variables. Our algorithm applies the DPLL algorithm to the graph-based representations of NNF formulas. We adapt the idea of the two-watched-literal scheme from CNF SAT solvers in order to efficiently carry out Boolean Constraint Propagation (BCP), a key task in the DPLL algorithm. We evaluate the new solver on a large collection of Boolean circuit benchmarks obtained from formal verification problems. The new solver outperforms the top solvers of the SAT 2007 competitionand SAT-Race 2008 in terms of run time on a large majority of the benchmarks.
机译：布尔可满足性（SAT）求解器在硬件和软件验证工具中大量使用，用于检查布尔公式的可满足性。大多数最先进的SAT求解器都是基于戴维斯-普特南-洛格曼-洛夫兰（DPLL）算法的，并且要求输入公式必须为合态范式（CNF）。我们提出了一种新的SAT求解器，它可以对给定的布尔公式/电路的求反标准形式（NNF）进行运算。就变量数量而言，公式的NNF通常比公式的CNF更简洁。我们的算法将DPLL算法应用于NNF公式的基于图的表示形式。我们采用CNF SAT求解器的两次监视文学方案的思想，以便有效地执行布尔约束传播（BCP），这是DPLL算法中的关键任务。我们根据从形式验证问题获得的大量布尔电路基准评估新的求解器。在大多数基准测试的运行时间方面，新的求解器优于SAT 2007竞赛和SAT-Race 2008的顶级求解器。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号