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

The MAthSAT Solver. A progress report

Bozzano, Marco;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 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
2004
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/2552
 Attenzione

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

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