@article{NieuwenhuisetalJACM2006,
 author = {Robert Nieuwenhuis and Albert Oliveras and Cesare Tinelli},
 title = {{Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T)}},
 journal = {J. ACM},
 volume = {53},
 number = {6},
 year = {2006},
 issn = {0004-5411},
 pages = {937--977},
 doi = {http://doi.acm.org/10.1145/1217856.1217859},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }