“The Design and Implementation of the Model Constructing Satisfiability Calculus” by Dejan Jovanovic, Clark Barrett, and Leonardo de Moura. In Proceedings of the 13^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '13), Oct. 2013, pp. 173-180. Portland, Oregon.
We present the design and implementation of the Model Constructing Satisfiability (MCSat) calculus. The MCSat calculus generalizes ideas found in CDCL-style propositional SAT solvers to SMT solvers, and provides a common framework where recent model-based procedures and techniques can be justified and combined. We describe how to incorporate support for linear real arithmetic and uninterpreted function symbols in the calculus. We report encouraging experimental results, where MCSat performs competitive with the state-of-the art SMT solvers without using pre-processing techniques and ad-hoc optimizations. The implementation is flexible, additional plugins can be easily added, and the code is freely available.
BibTeX entry:
@inproceedings{JBdM13,
author = {Dejan Jovanovi{\'c} and Clark Barrett and Leonardo de Moura},
title = {The Design and Implementation of the Model Constructing
Satisfiability Calculus},
booktitle = {Proceedings of the {\it 13^{th}} International Conference
on Formal Methods In Computer-Aided Design (FMCAD '13)},
pages = {173--180},
publisher = {FMCAD Inc.},
month = oct,
year = {2013},
note = {Portland, Oregon},
url = {http://theory.stanford.edu/~barrett/pubs/JBdM13.pdf}
}
(This webpage was created with bibtex2web.)