The Effect of Totalizer Bound Tightening on MaxSAT Solving
A. Tatabitovska (TU Delft - Electrical Engineering, Mathematics and Computer Science)
E. Demirović – Mentor (TU Delft - Algorithmics)
S. Picek – Coach (TU Delft - Cyber Security)
Maarten Flippo – Graduation committee member (TU Delft - Algorithmics)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
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.