Authors: Katalin Fazekas, Fahiem Bacchus and Armin Biere
Paper Information
Title: | Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories |
Authors: | Katalin Fazekas, Fahiem Bacchus and Armin Biere |
Proceedings: | IJCAR Proceedings 9th IJCAR, 2018 |
Editors: | Stephan Schulz, Didier Galmiche and Roberto Sebastiani |
Keywords: | Maximum Satisfiability, Satisfiability, Satisfiability Modulo Theories, Implicit Hitting Set |
Abstract: | ABSTRACT. Solving optimization problems with SAT has a long tradition, particularly in the form of MaxSAT, which maximizes the weight of satisfied clauses in a propositional formula. The extension to maximum satisfiability modulo theories (MaxSMT) is less mature but allows problems to be formulated in a higher-level language closer to actual applications. In this paper we describe a new approach for solving MaxSMT based on lifting one of the currently most successful approaches for MaxSAT, the implicit hitting set approach, from the propositional level to SMT. We also provide a unifying view of how optimization, propositional reasoning, and theory reasoning can be combined in a MaxSMT solver. This leads to a generic framework that can be instantiated in different ways, subsuming existing work and supporting new approaches. Experiments with two instantiations clearly show the benefit of our generic framework. |
Pages: | 16 |
Talk: | Jul 14 11:30 (Session 95F: SMT 1) |
Paper: |