Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts
Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts
复制标题
使用 DPLL、图表和观察剪切对非子句公式进行高效 SAT 求解
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
E. Clarke
中科院分区：
文献类型：
--
作者：
Himanshu Jain;E. Clarke
布尔可满足性(SAT)求解器广泛应用于硬件和软件验证工具中，用于检查布尔公式的可满足性。大多数最先进的SAT解算器基于Davis-Putnam-Logemann-Loveland(DPLL)算法，并要求输入公式采用合取范式(CNF)。我们提出了一个新的SAT求解器，它对给定的布尔公式/回路的否定范式(NNF)进行运算。就变量的数量而言，公式的NNF通常比公式的CNF更简洁。我们的算法将DPLL算法应用于NNF公式的图形化表示。为了有效地执行DPLL算法中的关键任务布尔约束传播(BCP)，我们采用了CNF SAT求解器中的双观察文字方案的思想。我们在从形式验证问题中获得的大量布尔电路基准上对新的求解器进行了评估。在大多数基准测试中，新的解算器在运行时间方面都超过了SAT 2007竞赛和SAT-Race 2008的顶级解算器。
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 competition and SAT-Race 2008 in terms of run time on a large majority of the benchmarks.