The Design and Implementation of the Model Constructing Satisfiability Calculus

by Dejan Jovanović, Clark Barrett, Leonardo de Moura
Abstract:
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.
Reference:
The Design and Implementation of the Model Constructing Satisfiability Calculus (Dejan Jovanović, Clark Barrett, Leonardo de Moura), In Proceedings of the 13th International Conference on Formal Methods In Computer-Aided Design (FMCAD ’13), FMCAD Inc., 2013. (Portland, Oregon)
Bibtex Entry:
@inproceedings{JBdM13,
  url       = "http://www.cs.stanford.edu/~barrett/pubs/JBdM13.pdf",
  author    = "Dejan Jovanović and Clark Barrett and Leonardo de Moura",
  title     = "The Design and Implementation of the Model Constructing Satisfiability Calculus",
  booktitle = "Proceedings of the 13th International Conference on Formal Methods In Computer-Aided Design (FMCAD '13)",
  publisher = "FMCAD Inc.",
  pages     = "173--180",
  month     = oct,
  year      = 2013,
  note      = "Portland, Oregon",
  category  = "Conference Publications",
  abstract  = "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."
}

Fork me on GitHub