Developed at Electrical Engineering and Computer Science Department of University of Michigan (Ann Arbor, MI) by Hossein Sheini, ARIO* is a full-scale SAT Solver capable to solve SATisfiability Modulo Theories (SMT) and Optimization problems represented by Boolean, Pseudo-Boolean (PB) and/or Integer Linear constraints.

In addition to the information provided below and in the published papers and technical reports, an interactive demo is also available here that demonstrates the communication and operation of different engines of ARIO. More information can be obtained by contacting the tool administrator, Ahura.

Specification Details

1. Mithra - The Boolean (Main) Solving Engine

• Variable State Independent Decaying Sum (VSIDS) heuristic
• Integrated application specific heuristics
• Two-Literal Watch Strategy for CNF clauses
• UIP conflict Analysis - Implication Graph traversal and non-chronological backtracking

2. Pueblo - The Pseudo-Boolean Solving Engine More info

• Selectable Watch-Fewest-Literal or Watch-Cheap-Literal strategies for PB constraints
• Additional PB Learning based on ILP Cutting Plane Theory

3. Anahita - The Unit-Two-Variable-Per-Inequality (UTVPI) Solving Engine

• Independent on-line solver for Unit-Two-Variable-Per-Inequality (UTVPI) integer constraints integrated into the Boolean/PB SAT Solver
• Implication-based and efficient encoding of integer constraint predicates into the SAT solver
• Integrated conflict analysis for integer constraint predicates

4. Haoma - The Integer/Real Linear Programming (ILP) Solving Engine

• Modern state-of-the-art routine for efficient refinement of inconsistent solutions to the off-line integer programming problem
• Off-line Simplex-based solver for non-UTVPI integer constraints

5. Surena - The Optimization Engine

• Incremental and Binary based Search methods
• Integrated application-based algorithms for optimizing specific properties

5. Daena - Output Analyzer Engine

• Minimally UnSatisfiable (MUS) Extractor

6. Apadana - The Input File Parsing Engine

• SMT-LIB format

News...

Download

Please contact the developer at: hsheini AT eecs DOT umich DOT edu or the tool administrator Ahura AT umich DOT edu for any problems with downloading.

Publications and Technical Reports