Witness-producing model-based projections for SMT synthesis with uncomputable symbols beyond EUF and linear arithmetic

The FMCAD 2025 framework of Hozzová and Bjørner ("Synthesiz3 This") reduces the synthesis of recursion-free single-invocation functions from specifications containing uncomputable symbols — symbols allowed in the specification but forbidden in the synthesized program — to quantifier elimination by model-based projection, and introduces witness-producing projections (called ∃MBPR) that simultaneously project the quantified variable away and output a computable realizer term. Complete witness-producing projections are established only for the theory of equality and uninterpreted functions (EUF), linear arithmetic, and their combination; the prototype is additionally incomplete on the non-convex integer case, and for theories such as arrays, algebraic datatypes, and nonlinear arithmetic only projections without witness extraction, or nothing at all, are available. The open problem is to develop complete witness-producing projections for these further theories — or to prove impossibility — and to delineate the boundary: for which theory combinations do finite quantifier-free uniform interpolants, and hence terminating complete projection-based synthesis procedures, exist, given that specifications combining an uncomputable predicate with integer arithmetic already admit no finite maximal solution.

Background

Program synthesis asks for the automatic construction of a program meeting a logical specification. In the SMT (satisfiability modulo theories) setting, a specification is a formula over a background theory — commonly EUF, the theory of equality with uninterpreted function symbols, which constrains only which terms must or must not be equal; linear arithmetic over reals or integers (LRA/LIA); the extensional theory of arrays, whose select and store operations read and write array cells; algebraic datatypes, i.e., freely generated inductive structures such as lists and trees; and nonlinear arithmetic, whose terms are polynomials. A specification of the form $\forall \boldsymbol{c}.\exists y.\forall \boldsymbol{u}.\varphi[y,\boldsymbol{c},\boldsymbol{u}]$ asks for a function returning $y$ on inputs $\boldsymbol{c}$, where the universally quantified $\boldsymbol{u}$ may range over auxiliary first- and second-order symbols.

Following terminology introduced in saturation-based synthesis (Hozzová, Kovács, Norman, and Voronkov, CADE 2023), Hozzová and Bjørner (FMCAD 2025) call the symbols $\boldsymbol{c}$ computable and the symbols $\boldsymbol{u}$ uncomputable: uncomputable symbols may occur in the specification but must not occur in the synthesized program. This restriction is expressive — it can, for example, force the synthesized function to be maximal among all solutions, or make the function discover properties of specification-only functions — and it raises the core question of how to eliminate the uncomputable symbols from the specification. Their framework covers total function synthesis (find a computable term $R$, a realizer, such that $\varphi[R/y]$ is valid) and partial function synthesis (find pairs $\langle C, R\rangle$ of a precondition $C$ and a realizer $R$, ideally with $C$ the strongest such condition, a maximal solution).

The framework is modular: one iterative algorithm repeatedly calls projection primitives. Existential model-based projection ($\exists$MBP) takes a model $\mathcal{M}$ of a quantifier-free formula $\Phi$ and a variable $x$, and returns a quantifier-free formula $\pi^{\exists}$ not mentioning $x$ with $\mathcal{M}\models\pi^{\exists}$ and $\pi^{\exists}\implies\exists x.\Phi$. Its extension $\exists$MBPR additionally returns a realizer term $r$ such that $\pi^{\exists}$ is satisfiable, $\pi^{\exists}\implies\Phi[r/y]$, and $y$ occurs in neither $\pi^{\exists}$ nor $r$; each such pair contributes one piece of the solution. Because not every model admits a computable realizer, the source's contract includes a fallback branch (Algorithm 1, step 4–5; Proposition 9): when no computable realizer exists, the procedure returns $r=\bot$ together with the plain $\exists$MBP projection, with $\pi^{\exists}\implies\exists y.\Phi$, and the synthesis loop refines the specification by $\neg\pi^{\exists}$ and continues; a complete $\exists$MBPR procedure produces a realizer exactly when one exists and returns the $\bot$-fallback otherwise. Universal projection handles the $\forall\boldsymbol{u}$-quantifier by enumerating unsatisfiable cores (in the style of the MARCO algorithm for minimal unsatisfiable subset enumeration) and projecting each core. Whenever these primitives exist for a theory, they plug into the same synthesis algorithm. The paper establishes complete $\exists$MBP/$\exists$MBPR for EUF, linear real and integer arithmetic, and their combination EUFLIA — witness extraction for integers relying on the complete functional synthesis of Kuncak, Mayer, Piskac, and Suter — and universal projection for EUF+LRA, where covering algorithms (Gulwani and Musuvathi) compute strongest quantifier-free consequences. Termination of the algorithm is tied to uniform interpolation: the existence, for every formula, of a strongest quantifier-free consequence in the remaining vocabulary (a finite quantifier-free uniform interpolant).

Two barriers delimit this state of the art. First, prior model-based projection algorithms cover arrays, integer arithmetic, and algebraic datatypes (e.g., Komuravelli, Bjørner, Gurfinkel, and McMillan, FMCAD 2015), but, as the source paper stresses, they "do not cover extracting computable realizers from projections"; for nonlinear arithmetic only template-based methods exist; and the prototype's witness extraction for integers is incomplete, sidestepping the non-convexity of LIA. Second, an inherent limit: synthesis solutions for first-order specifications are recursively enumerable but live in the undecidable $\forall\exists\forall$ fragment (Kahr, Moore, and Wang, 1962), and the paper's Example 4 exhibits a specification combining an uncomputable predicate with integer bounds whose only maximal solution is infinite, so finite quantifier-free uniform interpolants do not always exist for combinations of theories. Complete algorithms are therefore impossible in general, and the scientifically sharp question is where the boundary runs: for which theories and theory combinations can witness-producing projection be made complete, terminating exactly when the corresponding uniform interpolants exist.

Problem Statement

Within the framework of Synthesiz3 This (Hozzová and Bjørner, FMCAD 2025), extend witness-producing model-based projection — and thereby the modular synthesis algorithm for specifications with uncomputable symbols — beyond EUF and linear arithmetic:

1. For the extensional theory of arrays and for algebraic datatypes, where model-based projection without witness extraction already exists: construct $\exists$MBPR procedures, i.e., given a model $\mathcal{M}$ of a quantifier-free specification $\Phi[y]$ over the theory (combined with EUF and linear arithmetic as needed), compute a satisfiable quantifier-free formula $\pi^{\exists}$ over the computable symbols, not containing $y$, together with a computable realizer term $r$ with $\pi^{\exists}\implies\Phi[r/y]$, or, following the source's fallback, $r=\bot$ together with the plain $\exists$MBP projection ($\pi^{\exists}\implies\exists y.\Phi$) when no computable realizer exists for $\mathcal{M}$; prove soundness and prove completeness in the source's sense (producing a realizer exactly when one exists and the $\bot$-fallback otherwise, and finite elimination of all models, or termination of the projection-based synthesis loop) for the fragment claimed.

2. For nonlinear arithmetic over reals and integers: do the same to the extent undecidability permits (nonlinear integer satisfiability is undecidable by Hilbert's tenth problem), identifying fragments for which witness-producing projections with completeness or controlled semi-decision behavior exist.

3. Close the implementation-level gap for the non-convex integer case of linear integer arithmetic, where the current prototype's witness extraction is incomplete.

4. Delineate the completeness boundary: characterize for which combinations of the standard SMT-LIB theories finite quantifier-free uniform interpolants exist — a question the source ties to whether every synthesis specification has a finite maximal solution for that combination — and prove non-existence for the combinations where they fail, given that they already fail for combinations of an uncomputable predicate with integer arithmetic (the source's Example 4).

Positive answers plug directly into the source's modular algorithm; negative answers close the corresponding cases. The four deliverables are independent research questions, each of which admits a definite positive or negative outcome (a construction with soundness and completeness proved for the fragment it covers, a characterization of where such constructions can exist, or an impossibility or undecidability result where they cannot): a resolution of any one is a self-contained result, but the task as a whole is resolved only when all four are settled, since the stated objective joins the constructions to a complete account of where terminating procedures exist. These deliverables jointly serve one objective: making projection-based synthesis with uncomputable symbols available for theories beyond EUF and linear arithmetic, with a precise account of where complete, terminating procedures are possible at all.

References

1. Petra Hozzová and Nikolaj Bjørner. Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols. arXiv:2504.16536, DOI 10.48550/arxiv.2504.16536, 2025; published at FMCAD 2025. https://arxiv.org/abs/2504.16536
2. Márton Hajdu, Petra Hozzová, Laura Kovács, and Eva Maria Wagner. Completeness of Synthesis under Realizability Assumptions using Superposition. arXiv:2605.19683, 2026. https://arxiv.org/abs/2605.19683
3. Márton Hajdu, Petra Hozzová, Laura Kovács, Andrei Voronkov, Eva Maria Wagner, and Richard Steven Žilinčík. Synthesis Benchmarks for Automated Reasoning. arXiv:2507.19827, 2025. https://arxiv.org/abs/2507.19827
4. Viorica Sofronie-Stokkermans. On Symbol Elimination and Uniform Interpolation in Theory Extensions. arXiv:2506.01664, 2025. https://arxiv.org/abs/2506.01664
5. Rodrigo Raya and Christophe Ringeissen. Towards Quantifier-Free Interpolation in Array Languages with Unbounded Data Specifications. arXiv:2607.05126, 2026. https://arxiv.org/abs/2607.05126
6. Fabian Achammer, Stefan Hetzl, and Renate A. Schmidt. Computing Witnesses Using the SCAN Algorithm (Extended Preprint). arXiv:2506.00163, 2025. https://arxiv.org/abs/2506.00163
7. Anvesh Komuravelli, Nikolaj Bjørner, Arie Gurfinkel, and Kenneth L. McMillan. Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. arXiv:1508.01288, 2015 (FMCAD 2015). https://arxiv.org/abs/1508.01288
8. Petra Hozzová, Laura Kovács, Chase Norman, and Andrei Voronkov. Program Synthesis in Saturation. In Automated Deduction – CADE 29, Lecture Notes in Computer Science, DOI 10.1007/978-3-031-38499-8_18, 2023; extended version arXiv:2402.18962, 2024. https://arxiv.org/abs/2402.18962
9. A. S. Kahr, Edward F. Moore, and Hao Wang. Entscheidungsproblem Reduced to the AEA Case. Proceedings of the National Academy of Sciences 48(3):365–377, 1962. DOI 10.1073/pnas.48.3.365. https://doi.org/10.1073/pnas.48.3.365
10. Benjamin Caulfield, Markus N. Rabe, Sanjit A. Seshia, and Stavros Tripakis. What's Decidable about Syntax-Guided Synthesis?. arXiv:1510.08393, 2015. https://arxiv.org/abs/1510.08393
11. Sumit Gulwani and Madan Musuvathi. Cover Algorithms and Their Combination. ESOP 2008, Lecture Notes in Computer Science, DOI 10.1007/978-3-540-78739-6_16, 2008. https://doi.org/10.1007/978-3-540-78739-6_16
12. Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, and Philippe Suter. Complete functional synthesis. Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), DOI 10.1145/1806596.1806632, 2010. https://doi.org/10.1145/1806596.1806632