Incomplete MaxSAT Solving by Linear Programming Relaxation and Rounding

Show full item record



Permalink

http://urn.fi/URN:NBN:fi:hulib-202006172994
Title: Incomplete MaxSAT Solving by Linear Programming Relaxation and Rounding
Author: Kemppainen, Esa
Contributor: University of Helsinki, Faculty of Science
Publisher: Helsingin yliopisto
Date: 2020
URI: http://urn.fi/URN:NBN:fi:hulib-202006172994
http://hdl.handle.net/10138/316594
Thesis level: master's thesis
Abstract: NP-hard optimization problems can be found in various real-world settings such as scheduling, planning and data analysis. Coming up with algorithms that can efficiently solve these problems can save various rescources. Instead of developing problem domain specific algorithms we can encode a problem instance as an instance of maximum satisfiability (MaxSAT), which is an optimization extension of Boolean satisfiability (SAT). We can then solve instances resulting from this encoding using MaxSAT specific algorithms. This way we can solve instances in various different problem domains by focusing on developing algorithms to solve MaxSAT instances. Computing an optimal solution and proving optimality of the found solution can be time-consuming in real-world settings. Finding an optimal solution for problems in these settings is often not feasible. Instead we are only interested in finding a good quality solution fast. Incomplete solvers trade guaranteed optimality for better scalability. In this thesis, we study an incomplete solution approach for solving MaxSAT based on linear programming relaxation and rounding. Linear programming (LP) relaxation and rounding has been used for obtaining approximation algorithms on various NP-hard optimization problems. As such we are interested in investigating the effectiveness of this approach on MaxSAT. We describe multiple rounding heuristics that are empirically evaluated on random, crafted and industrial MaxSAT instances from yearly MaxSAT Evaluations. We compare rounding approaches against each other and to state-of-the-art incomplete solvers SATLike and Loandra. The LP relaxation based rounding approaches are not competitive in general against either SATLike or Loandra However, for some problem domains our approach manages to be competitive against SATLike and Loandra.
Subject: maxsat
combinatorial optimization
linear programming
algorithms
Discipline: none


Files in this item

Total number of downloads: Loading...

Files Size Format View
Kemppainen_Esa_MSc_2020.pdf 676.5Kb PDF View/Open

This item appears in the following Collection(s)

Show full item record