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 (DATE'05) Volume 2
Efficient Conflict-Based Learning in an RTL Circuit Constraint Solver
Munich, Germany
March 07-March 11
ISBN: 0-7695-2288-2
M. K. Iyer, University of California - Santa Barbara
G. Parthasarathy, University of California - Santa Barbara
K.-T. Cheng, University of California - Santa Barbara
We present new techniques for improving search in a hybrid Davis-Putnam-Logemann-Loveland based constraint solver for RTL circuits (HDPLL). In earlier work on HDPLL, the authors combined solvers for integer and Boolean domains using finite-domain constraint propagation with heuristic conflict-based learning. In this work, we describe a new algorithm that extends the conflict-based unique-implication point learning in Boolean SAT solvers to hybrid Boolean-Integer domains in HDPLL. We describe data-structures for efficient constraint propagation on the hybrid learned relations, similar to two-literal watching in Boolean SAT. We demonstrate that these new techniques provide considerable performance benefits when compared with other combinations of decision theories.
Citation:
M. K. Iyer, G. Parthasarathy, K.-T. Cheng, "Efficient Conflict-Based Learning in an RTL Circuit Constraint Solver," date, vol. 2, pp.666-671, Design, Automation and Test in Europe (DATE'05) Volume 2, 2005
Usage of this product signifies your acceptance of the Terms of Use.