Katalin Fazekas, Fahiem Bacchus, Armin Biere,
"Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories"
: Proc. 9th Intl. Joint Conf. on Automated Reasoning (IJCAR'18), Serie Lecture Notes in Computer Science (LNCS), Vol. 10900, Springer, Seite(n) 134-151, 2018
Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories
Sprache des Titels:
Proc. 9th Intl. Joint Conf. on Automated Reasoning (IJCAR'18)
Solving optimization problems with SAT has a long tradition in the form of MaxSAT, which maximizes the weight of satis?ed clauses in a propositional formula. The extension to maximum satis?ability 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 di?erent ways, subsuming existing work and supporting new approaches. Experiments with two instantiations clearly show the bene?t of our generic framework.