Predicate learning and selective theory deduction for a difference logic solver

Chao Wang, Aarti Gupta, Malay Ganai

Research output: Chapter in Book/Report/Conference proceedingConference contribution

9 Scopus citations


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 therefore 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.

Original languageEnglish (US)
Title of host publication2006 43rd ACM/IEEE Design Automation Conference, DAC'06
PublisherInstitute of Electrical and Electronics Engineers Inc.
Number of pages6
ISBN (Print)1595933816, 1595933816, 9781595933812
StatePublished - 2006
Event43rd Annual Design Automation Conference, DAC 2006 - San Francisco, CA, United States
Duration: Jul 24 2006Jul 28 2006

Publication series

NameProceedings - Design Automation Conference
ISSN (Print)0738-100X


Conference43rd Annual Design Automation Conference, DAC 2006
Country/TerritoryUnited States
CitySan Francisco, CA

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Control and Systems Engineering


  • Decision procedure
  • Difference logic
  • SAT
  • SMT solver


Dive into the research topics of 'Predicate learning and selective theory deduction for a difference logic solver'. Together they form a unique fingerprint.

Cite this