loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Design, Automation and Test in Europe Conference and Exhibition Volume I (DATE'04)
Arithmetic Reasoning in DPLL-Based SAT Solving
Paris, France
February 16-February 20
ISBN: 0-7695-2085-5
ASCII Text
x 
 
Markus Wedler, Dominik Stoffel, Wolfgang Kunz, "Arithmetic Reasoning in DPLL-Based SAT Solving," Design, Automation and Test in Europe Conference and Exhibition, vol. 1, pp. 10030, Design, Automation and Test in Europe Conference and Exhibition Volume I (DATE'04), 2004.
 
 
BibTex
x
 
@article{ 10.1109/DATE.2004.1268823,
author = {Markus Wedler and Dominik Stoffel and Wolfgang Kunz},
title = {Arithmetic Reasoning in DPLL-Based SAT Solving},
journal ={Design, Automation and Test in Europe Conference and Exhibition},
volume = {1},
year = {2004},
issn = {1530-1591},
pages = {10030},
doi = {http://doi.ieeecomputersociety.org/10.1109/DATE.2004.1268823},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Design, Automation and Test in Europe Conference and Exhibition
TI - Arithmetic Reasoning in DPLL-Based SAT Solving
SN - 1530-1591
SP
EP
A1 - Markus Wedler,
A1 - Dominik Stoffel,
A1 - Wolfgang Kunz,
PY - 2004
KW - null
VL - 1
JA - Design, Automation and Test in Europe Conference and Exhibition
ER -
 
Markus Wedler, University of Kaiserslautern
Dominik Stoffel, University of Kaiserslautern
Wolfgang Kunz, University of Kaiserslautern
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.
Citation:
Markus Wedler, Dominik Stoffel, Wolfgang Kunz, "Arithmetic Reasoning in DPLL-Based SAT Solving," date, vol. 1, pp.10030, Design, Automation and Test in Europe Conference and Exhibition Volume I (DATE'04), 2004
Usage of this product signifies your acceptance of the Terms of Use.