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

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 DavisPutnam-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 com...

• Type: Conference
• Year: 2009
• Where: DAC
• Authors: Himanshu Jain, Edmund M. Clarke
• Keywords: Boolean Circuit Benchmarks, CNF SAT Solvers, DAC 2009, Design Automation, State-of-the-art Sat Solvers