Satisfiability modulo Theories: Introduction and Applications

De Moura, Leonardo and Bjørner, Nikolaj

Checking the satisfiability of logical formulas, SMT solvers scale orders of magnitude beyond custom ad hoc solvers.

@article{demoura+:cacm11-smt,
  address = {New York, NY, USA},
  author = {De Moura, Leonardo and Bj\o{}rner, Nikolaj},
  date-added = {2020-11-15 23:36:57 -0800},
  date-modified = {2020-11-15 23:36:57 -0800},
  issn = {0001-0782},
  issue_date = {September 2011},
  journal = {Commun. ACM},
  month = sep,
  number = {9},
  numpages = {9},
  pages = {69--77},
  publisher = {Association for Computing Machinery},
  title = {Satisfiability modulo Theories: Introduction and Applications},
  volume = {54},
  year = {2011},
  bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxAfcGFwZXJzL2RlbW91cmErY2FjbTExLXNtdC1hLnBkZk8RAYYAAAAAAYYAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAAAAAABCRAAB/////xhkZW1vdXJhK2NhY20xMS1zbXQtYS5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAD/////AAAAAAAAAAAAAAAAAAEAAwAACiBjdQAAAAAAAAAAAAAAAAAGcGFwZXJzAAIAPi86VXNlcnM6Z2FtYmxpbjI6c3JjOmJ1aWxkLWJpYjpwYXBlcnM6ZGVtb3VyYStjYWNtMTEtc210LWEucGRmAA4AMgAYAGQAZQBtAG8AdQByAGEAKwBjAGEAYwBtADEAMQAtAHMAbQB0AC0AYQAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAPFVzZXJzL2dhbWJsaW4yL3NyYy9idWlsZC1iaWIvcGFwZXJzL2RlbW91cmErY2FjbTExLXNtdC1hLnBkZgATAAEvAAAVAAIAD///AAAACAANABoAJABGAAAAAAAAAgEAAAAAAAAABQAAAAAAAAAAAAAAAAAAAdA=},
  bdsk-url-1 = {https://doi.org/10.1145/1995376.1995394}
}