Research map / Learning theory and algorithms / Combinatorial and search optimization
An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Presents Algaroba, an eager SMT solver that reduces quantifier-free algebraic datatype queries to uninterpreted functions using depth-bounded acyclicality axioms, and shows it beats CVC5, Z3, and Princess on SMTCOMP-style and a new blocks-world benchmark.
Problem
Existing SMT solvers for algebraic data types (ADTs) all use lazy architectures and do not scale well on harder queries, and the community has few ADT-capable solvers.
Approach
Reduce quantifier-free ADT queries to quantifier-free UF queries eagerly: flatten and Skolemize the formula, compute a per-ADT depth bound k from the number of variables, and instantiate ADT axioms (constructor/selector rewriting, tester exclusivity, acyclicality up to depth k) so an off-the-shelf UF solver can be used.
Key results
- On the Bouvier set Algaroba solved 45.75% of queries versus 37.25% for the next best (CVC5 and Z3), and was 2.30x faster on average on solved queries.
- On the new blocks world set Algaroba solved 61.4% of queries versus 56.2% for Z3, and was 2.00x faster than Z3 on solved queries.
- Algaroba had the top SMTCOMP contribution rank on Bouvier and blocks world; the virtual best solver rose from 64.25% to 83.75% on Bouvier when Algaroba was included.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use Algaroba's eager ADT-to-UF reduction instead of the state-of-the-art solvers | SMT solving for ADT queries · Barrett et al. | average solve time: 0.05 seconds (CVC5) vs 0.08 seconds (Algaroba) | No clear effect |
| Use Algaroba's eager ADT-to-UF reduction instead of CVC5 | SMT solving for ADT queries · Bouvier | queries solved: 37.25% -> 45.75% | Helped |
| Use Algaroba's eager ADT-to-UF reduction instead of Z3 | SMT solving for ADT queries · Bouvier | average run time on successful queries: 437.18 seconds -> 190.11 seconds | Helped |
| Use Algaroba's eager ADT-to-UF reduction instead of CVC5 | SMT solving for ADT queries · Bouvier | standard deviation on successful queries: 346.83 seconds -> 267.13 seconds | Helped |
| Use Algaroba's eager ADT-to-UF reduction instead of Z3 | SMT solving for ADT queries · Blocks world | queries solved: 56.2% -> 61.4% | Helped |
| Use Algaroba's eager ADT-to-UF reduction instead of Z3 | SMT solving for ADT queries · Blocks world | average run time on successful queries: 175.05 seconds -> 87.34 seconds | Helped |
| Use Algaroba's eager ADT-to-UF reduction instead of Z3 | SMT solving for ADT queries · Blocks world | standard deviation on successful queries: 300.15 seconds -> 198.67 seconds | Helped |
| Use Algaroba instead of Princess | SMT solving for ADT queries · Blocks world | average run time on successful queries: 31.89 seconds (Princess) vs 87.34 seconds (Algaroba) | Hurt |
Surprising findings
- Princess, the other eager approach, is the fastest and most consistent on solved blocks world queries but solves 44.6 percentage points fewer queries than Algaroba.
- On the Barrett et al. benchmark all solvers solve every query, so performance differences there are negligible.
Limitations
- Scope is limited to quantifier-free ADT queries; quantifiers are left to future work.
- Double exponential blowup possible when finite universes are instantiated, and exponential blowup in selector depth for tree-like types.
- Performance on Barrett et al. benchmark is indistinguishable from other solvers.
Experimental setup
Datasets: Bouvier benchmark set Barrett et al. ADT benchmark set (SMTCOMP)
Benchmarks: Bouvier benchmark set Barrett et al. benchmark set Blocks world benchmark set (500 queries)
Metrics: percentage of queries solved within 1200s timeout average and standard deviation of solve time on solved queri SMTCOMP contribution rank (virtual best solver)
Baselines: CVC5 Z3 Princess
Builds on: Oppen 1980 decision procedure Princess eager ADT reduction SMT-LIB
Closest papers by meaning
- Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking (AAAI 2025 · similarity 0.86)
- SAT-Based Techniques for Lexicographically Smallest Finite Models (AAAI 2024 · similarity 0.85)
- A Complete Algorithm for Optimization Modulo Nonlinear Real Arithmetic (AAAI 2025 · similarity 0.84)
- The Impact of Literal Sorting on Cardinality Constraint Encodings (AAAI 2025 · similarity 0.84)
- Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits (ICML 2025 · similarity 0.84)
- A Compositional Atlas for Algebraic Circuits (NeurIPS 2024 · similarity 0.84)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.