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

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 verification
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/2559
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact