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 discuss the advances in the development of MathSat. In particular, the current version of the tool is built on minisat, a new-generation propositional SAT solver, and Cassowary, an incremental mathematical reasoner, and it incorporates support for integer variables. We compare the performance of MathSat with CVCL and show that MathSat is significantly more efficient on a set of benchmarks related to word-level verification
The MathSAT Solver - a comparative evaluation
Bozzano, Marco;Bruttomesso, Roberto;Cimatti, Alessandro;Sebastiani, Roberto
2004-01-01
Abstract
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 discuss the advances in the development of MathSat. In particular, the current version of the tool is built on minisat, a new-generation propositional SAT solver, and Cassowary, an incremental mathematical reasoner, and it incorporates support for integer variables. We compare the performance of MathSat with CVCL and show that MathSat is significantly more efficient on a set of benchmarks related to word-level verificationI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
