Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

FMCAD

2006

Springer

2006

Springer

Ario is a solver for systems of linear integer arithmetic logic. Such systems are commonly used in design verification applications and are classified under Satisfiability Modulo Theories (SMT) problems. Recognizing the fact that in many such applications the majority of atoms are equalities or integer unit-two-variable inequalities (UTVPIs), we present a framework that integrates specialized theory solvers for those atoms within a SAT solver. The unique feature of our strategy is its simultaneous adoption of both a congruence-closure equality solver and a transitive-closure UTVPI solver to find a satisfiable set of those atoms. A full-scale ILP solver is then utilized to check the consistency of all integer constraints within the solution. Other notable features of our solver include its combined deduction and learning schemes that collectively make our solver distinct among similar solvers.

Related Content

Added |
22 Aug 2010 |

Updated |
22 Aug 2010 |

Type |
Conference |

Year |
2006 |

Where |
FMCAD |

Authors |
Hossein M. Sheini, Karem A. Sakallah |

Comments (0)