@Article{NieOT-JACM-06,
  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 =	 {Journal of the ACM},
  year =	 2006,
  volume =	 53,
  number =	 6,
  pages =	 {937--977},
  month =	 nov,
}