Sciweavers

Share
DAC
2006
ACM

Predicate learning and selective theory deduction for a difference logic solver

10 years 27 days ago
Predicate learning and selective theory deduction for a difference logic solver
Design and verification of systems at the Register-Transfer (RT) or behavioral level require the ability to reason at higher levels of abstraction. Difference logic consists of an arbitrary Boolean combination of propositional variables and difference predicates and e provides an appropriate abstraction. In this paper, we present several new optimization techniques for efficiently deciding difference logic formulas. We use the lazy approach by combining a DPLL Boolean SAT procedure with a dedicated graph-based theory solver, which adds transitivity constraints among difference predicates on a "need-to" basis. Our new optimization techniques include flexible theory constraint propagation, selective theory deduction, and dynamic predicate learning. We have implemented these techniques in our lazy solver. We demonstrate the effectiveness of the proposed techniques on public benchmarks through a set of controlled experiments. Categories and Subject Descriptors B.6.3 [Logic desig...
Chao Wang, Aarti Gupta, Malay K. Ganai
Added 13 Nov 2009
Updated 13 Nov 2009
Type Conference
Year 2006
Where DAC
Authors Chao Wang, Aarti Gupta, Malay K. Ganai
Comments (0)
books