Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools

An overview is given of a number of recent developments in SAT and SAT Modulo Theories (SMT). In particular, based on our k of Abstract DPLL and Abstract DPLL modulo Theories, we explain our DPLL(T) approach to SMT. Experimental results and future projects are discussed within BarcelogicTools, a set of logic-based tools developed by our research group in Barcelona. At the 2005 SMT competition, BarcelogicTools won all four categories it participated in (out of the seven existing categories).

• Type: Conference
• Year: 2005
• Where: LPAR
• Authors: Robert Nieuwenhuis, Albert Oliveras
• Keywords: Abstract DPLL, Dpll Modulo Theories, LPAR 2005, Modulo Theories