SMT (Satisfiability Modulo Theories) solving extends SAT solving by incorporating theories such as arithmetic, arrays, and uninterpreted functions, enabling the solution of more expressive logical formulas.
Our Research Focus
Theory Combination
Research on efficiently combining different theories in SMT solving:
- Nelson-Oppen combination method
- Model-based theory combination
- Equality propagation techniques
- Care-graph optimizations
Theory-specific Algorithms
Develop and optimize decision procedures for specific theories:
- Linear arithmetic (real and integer)
- Non-linear arithmetic
- Array theory
- Bit-vector operations
- Uninterpreted functions
CDCL(T) Framework
Enhance the CDCL(T) framework for efficient SMT solving:
- Theory propagation mechanisms
- Conflict explanation generation
- Theory-aware preprocessing
- Learning strategies
- Incremental solving techniques
Our research has produced several cutting-edge SMT solvers:
- AriParti: A parallel SMT solver with variable-level partitioning
- Z3++: A hybrid solver integrating local search with complete algorithms
- hybridSMT: A hybrid algorithm SMT solver