FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories

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: