Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization

This paper introduces a new anytime algorithm for Weighted MaxSAT consisting of two main algorithmic components. First, we propose a new efficient polarity selection heuristic and an enhancement to the variable decision heuristic for SAT-based anytime Weighted MaxSAT solving (and, more generally, for solving any optimization problem with a SAT-based anytime algorithm). Second, we enhance an existing Bit-vector Optimization-based algorithm for solving Unweighted MaxSAT and generalize it to Weighted MaxSAT. Our resulting Weighted MaxSAT solver outscores the state-of-the-art solvers in the settings of both the 60-second and 300-second weighted incomplete tracks of MaxSAT Evaluation 2018. In addition, we describe a new application of incremental anytime Weighted MaxSAT solving: placement at the physical design stage of Computer-aided Design (CAD).