# Satisfiability and Synthesis Modulo Oracles

arXiv: https://arxiv.org/abs/2107.13477 · HTML: https://mlsanity.com/paper/2107.13477/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 38 references that are in the map.
- First posted on arXiv 28 Jul 2021.

## Builds on (most cited first, 7 of 7)

- [Program Synthesis using Conflict-Driven Learning](https://mlsanity.com/paper/1711.08029/) (2017)
- [A Theory of Formal Synthesis via Inductive Learning](https://mlsanity.com/paper/1505.03953/) (2015)
- [Modeling Black-Box Components with Probabilistic Synthesis](https://mlsanity.com/paper/2010.04811/) (2020)
- [Data-Driven Inference of Representation Invariants](https://mlsanity.com/paper/2003.12106/) (2020)
- [LoopInvGen: A Loop Invariant Generator based on Precondition Inference](https://mlsanity.com/paper/1707.02029/) (2017)
- [On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4](https://mlsanity.com/paper/1502.04464/) (2015)
- [CVC4 at the SMT Competition 2018](https://mlsanity.com/paper/1806.08775/) (2018)

## Built on by (most cited first, 1 of 1)

- [CDRL: Certification-Driven Reinforcement Learning for Neutrino Flavor Model Discovery](https://mlsanity.com/paper/2608.20686/) (2026)

## Abstract (arXiv)

In classic program synthesis algorithms, such as counterexample-guided inductive synthesis (CEGIS), the algorithms alternate between a synthesis phase and an oracle (verification) phase. Many synthesis algorithms use a white-box oracle based on satisfiability modulo theory (SMT) solvers to provide counterexamples. But what if a white-box oracle is either not available or not easy to work with? We present a framework for solving a general class of oracle-guided synthesis problems which we term synthesis modulo oracles. In this setting, oracles may be black boxes with a query-response interface defined by the synthesis problem. As a necessary component of this framework, we also formalize the problem of satisfiability modulo theories and oracles, and present an algorithm for solving this problem. We implement a prototype solver for satisfiability and synthesis modulo oracles and demonstrate that, by using oracles that execute functions not easily modeled in SMT-constraints, such as recursive functions or oracles that incorporate compilation and execution of code, SMTO and SyMO are able to solve problems beyond the abilities of standard SMT and synthesis solvers.