Natural Domain SMT: A Preliminary Assessment

SMT solvers have traditionally been based on the DPLL(T) algorithm, where the driving force behind the procedure is a DPLL search over truth valuations. This traditional framework allows for a degree of modularity in the treatment of theory solvers. Over time, theory solvers have become more and more closely integrated into the DPLL process, and consequently less and less modular. In this paper, we present a DPLL-like algorithm for SMT solving in which the search takes place over the natural domain of the variables in the problem. As a case study, we analyze its application to continuous domain linear arithmetic, present implementation techniques and some experimentation with difference logic. Results indicate the method can sometimes outperform leading SMT solvers but that the method is not yet robust.

• Type: Journal
• Year: 2010
• Where: FORMATS
• Authors: Scott Cotton
• Keywords: Formal Methods, FORMATS 2010, Present Implementation Techniques, SMT Solvers, Theory Solvers