Departmental Seminar: Incremental Maximum Satisfiability

Title: Incremental Maximum Satisfiability

Abstract: Various problem domains call for iterative solving procedures where a sequence of related instances are solved. Modern Boolean satisfiability (SAT) solvers allow for efficient incremental computations by reusing information obtained during previous calls. This feature is key to efficient employment of SAT solvers iteratively for developing complex decision and optimization procedures, including maximum satisfiability (MaxSAT) solvers. However, enabling incremental computations on the level of constraint optimization remains a noticeable challenge. In this talk we give an overview of recent developments in incremental MaxSAT solving. Firstly, we describe IPAMIR, a standard interface for implementing incremental MaxSAT solvers and for developing applications making use of incremental MaxSAT, used in the new Incremental Track of MaxSAT Evaluations. Secondly, we detail how incremental computations are enabled in the implicit hitting set (IHS) approach to MaxSAT solving. As a practical result, we develop iMaxHS, an incremental version of the IHS-based MaxSAT solver MaxHS. Finally, we provide empirical evidence on the benefits of incremental MaxSAT solving in several application scenarios.