Incorporating Multi-armed Bandit with Local Search for MaxSAT

As an optimization extension of the famous Boolean Satisfiability (SAT) decision problem, the Maximum Satisfiability (MaxSAT) problem aims at finding a complete assignment of the Boolean variables to satisfy as many clauses as possible in a given propositional formula in Conjunctive Normal Form (CNF) [1]. Partial MaxSAT (PMS) is a variant of MaxSAT where the clauses are divided into hard and soft. PMS aims at maximizing the number of satisfied soft clauses with the constraint that all the hard clauses must be satisfied. Associating a positive weight to each soft clause in PMS results in Weighted PMS (WPMS), whose goal is to maximize the total weight of satisfied soft clauses with the same constraint of PMS that all the hard clauses must be satisfied. Both PMS and WPMS, denoted as (W)PMS, have many practical applications such as planning [2], combinatorial testing [3], group testing [4], timetabling [5], etc. Existing solvers for (W)PMS can be divided into complete and incomplete according to whether their solutions have optimality guarantees.