Research Topics and Thesis Projects
===================================

Aria offers numerous opportunities for research and thesis projects across multiple areas of automated reasoning.

=========
Core Algorithm Development
=========

**Parallel CDCL(T) Solving** (``aria/smt/pcdclt``)
  Develop parallel algorithms for conflict-driven clause learning with theory reasoning. Focus on work distribution, clause sharing, and portfolio solving.

**Optimization Modulo Theory** (``aria/optimization``)
  Extend SMT solving with optimization capabilities. Implement algorithms for OMT over bit-vectors, arithmetic, and mixed theories.

**Advanced Model Counting** (``aria/counting``)
  Improve counting algorithms for Boolean, arithmetic, and quantifier-free bit-vector formulas. Focus on scalability and approximation techniques.

**Symbolic Abstraction** (``aria/symabs``)
  Develop new abstraction techniques for infinite state systems. Implement counterexample-guided abstraction refinement (CEGAR).

=========
Theory-Specific Solving
=========

**Finite Field SMT** (``aria/smt/ff``)
  Build decision procedures for Galois field constraints. Applications in cryptography and coding theory.

**Floating-Point Arithmetic** (``aria/smt/fp``)
  Develop efficient solvers for IEEE 754 floating-point constraints with proper handling of rounding modes and special values.

**String Constraint Solving**
  Extend string theory support with automata-based techniques. Implement length constraints and regular language operations.

=========
AI-Enhanced Reasoning
=========

**Machine Learning for Solvers** (``aria/ml``)
  Extract features for learned solver selection, clause learning prediction, and variable ordering heuristics.

**Automata Learning** (``aria/automata``)
  Apply active learning to infer automata from examples for string constraint solving and program verification.

=========
Advanced Sampling & Enumeration
=========

**Uniform Sampling** (``aria/sampling``)
  Develop algorithms for uniform solution sampling over complex constraint domains. Applications in probabilistic verification.

**AllSMT Algorithms** (``aria/allsmt``)
  Enumerate all solutions efficiently. Focus on diversity metrics and incremental solving techniques.

**Solution Space Analysis**
  Implement tools for analyzing solution spaces, including backbone computation and minimal unsatisfiable core extraction.

=========
Quantifier Handling
=========

**Quantifier Elimination** (``aria/quant/qe``)
  Develop QE procedures for mixed theories combining arithmetic, bit-vectors, and arrays.

**E-Matching Optimization** (``aria/quant/ematching``)
  Improve quantifier instantiation through better pattern matching and trigger selection.

**CHC Solving** (``aria/quant/chctools``)
  Scale algorithms for constrained Horn clause solving. Applications in program verification and synthesis.

=========
Applications & Tools
=========

**Interactive Theorem Proving** (``aria/itp``)
  Build proof assistant tools with support for multiple theories and automated proof search.

**Program Synthesis** (``aria/synthesis``)
  Implement syntax-guided synthesis techniques for bit-vectors, arithmetic, and string domains.

**Abductive Reasoning** (``aria/abduction``)
  Develop algorithms for generating explanations and hypotheses from constraint observations.

=========
Getting Started
=========

Each module includes examples and documentation. Start with ``aria/allsmt`` for basic usage patterns, then explore specialized areas based on your interests.