Ario: A Linear Integer Arithmetic Logic Solver

10 years 4 months ago
Ario: A Linear Integer Arithmetic Logic Solver
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.
Hossein M. Sheini, Karem A. Sakallah
Added 22 Aug 2010
Updated 22 Aug 2010
Type Conference
Year 2006
Authors Hossein M. Sheini, Karem A. Sakallah
Comments (0)