The Effect of Totalizer Bound Tightening on MaxSAT Solving

Abstract

Maximum Satisfiability (MaxSAT) is a known problem within the optimization field which has led many different solving approaches to be devised in the last several decades. From Linear Search to unsatisfiable core-based solvers, many MaxSAT algorithms rely on cardinality constraints to express how many soft clauses can be violated at most. However, as MaxSAT is expressed in the Conjunctive Normal Form, there is a need to translate, or encode, these cardinality constraints into CNF. A popular encoding algorithm, the Totalizer Encoding, is used within these solvers - a system of encoding that builds a binary tree to express the cardinality constraint. This paper aims to introduce an alternate construction for the Totalizer Encoding, referred to as the Layered Totalizer Encoding, which interleaves the mechanics of encoding and solving as to cut down on runtime as well as potentially solve previously unsolved instances. The research shows that the Layered Totalizer Encoding outperforms Linear Search on average, solves more instances than Linear Search, and can be tuned through heuristics to show even more favorable results. Moreover, the Layered Totalizer Encoding is shown to not only work as a standalone algorithm, but can also boost the performance of the OLL algorithm.