# Proof Generation in CDSAT

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 4 of its 30 references that are in the map.
- First posted on arXiv 6 Jul 2021.

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

- [Efficient Certified RAT Verification](https://mlsanity.com/paper/1612.02353/) (2016)
- [A CDCL-style calculus for solving non-linear constraints](https://mlsanity.com/paper/1905.09227/) (2019)
- [Extending Description Logic EL++ with Linear Constraints on the Probability of Axioms](https://mlsanity.com/paper/1908.10405/) (2019)
- [Solving bitvectors with MCSAT: explanations from bits and pieces (long version)](https://mlsanity.com/paper/2004.07940/) (2020)

## Abstract (arXiv)

The main ideas in the CDSAT (Conflict-Driven Satisfiability) framework for SMT are summarized, leading to approaches to proof generation in CDSAT.