The MAthSAT Solver. A progress report

Many problems of practical relevance are conveniently expressed as boolean combinations of propositional variables and mathematical constraints. The development of decision procedures able to check the satisfiability of such formulas is therefore being devoted an increasing interest. The MathSat family of deciders is based on the extension of a DPLL propositional satisfiability procedure, used as an assignment enumerator. MathSat pioneers a lazy and layered approach, where propositional reasoning is tightly integrated with solvers of increasing expressive power (e.g. to reason about equality and linear arithmetic) in such a way that ``more expensive'' layers are called less frequently. In this paper, we show the advances in the development of MathSat. We discuss the implications related to the use of Minisat, a new-generation propositional SAT solver; the role of an incremental mathematical reasoner; the role of static learning; and the extension to integer variables. We show that the new version of MathSat is significantly more efficient than the previous one