# SyGuS Techniques in the Core of an SMT Solver

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 29 Nov 2017.

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

- [Reinforcement Learning and Data-Generation for Syntax-Guided Synthesis](https://mlsanity.com/paper/2307.09564/) (2023)

## Abstract (arXiv)

We give an overview of recent techniques for implementing syntax-guided synthesis (SyGuS) algorithms in the core of Satisfiability Modulo Theories (SMT) solvers. We define several classes of synthesis conjectures and corresponding techniques that can be used when dealing with each class of conjecture.