| Abstract |
|
We propose a new arithmetic reasoning calculus to speed up a SAT solver based on the Davis Putnam Longman Loveland (DPLL) procedure. It is based on an arithmetic bit level description of the arithmetic circuit parts and the property. This description can easily be provided by the front-end of an RTL property checker. The calculus yields significant speedup and more robustness on hard SAT instances derived from the formal verification of arithmetic circuits.
|
 Additional Information
|
Citation:
Markus Wedler, Dominik Stoffel, Wolfgang Kunz,
"Arithmetic Reasoning in DPLL-Based SAT Solving,"
date,
p. 10030,
Design, Automation and Test in Europe Conference and Exhibition Volume I (DATE'04),
2004
|
