Solving MAXSAT by Decoupling Optimization and Satisfaction

• Main Author: Davies, Jessica
• Other Authors: Bacchus, Fahiem
• Language: en_ca
• Published: 2013
• Subjects: Combinatorial optimization; Propositional logic; Maximum satisfiability; Weighted constraints; Integer programming; Satisfiability; 0984; 0800; 0796
• Online Access: http://hdl.handle.net/1807/43539

Many problems that arise in the real world are difficult to solve partly because they present computational challenges. Many of these challenging problems are optimization problems. In the real world we are generally interested not just in solutions but in the cost or benefit of these solutions according to different metrics. Hence, finding optimal solutions is often highly desirable and sometimes even necessary. The most effective computational approach for solving such problems is to first model them in a mathematical or logical language, and then solve them by applying a suitable algorithm. This thesis is concerned with developing practical algorithms to solve optimization problems modeled in a particular logical language, MAXSAT. MAXSAT is a generalization of the famous Satisfiability (SAT) problem, that associates finite costs with falsifying various desired conditions where these conditions are expressed as propositional clauses. Optimization problems expressed in MAXSAT typically have two interacting components: the logical relationships between the variables expressed by the clauses, and the optimization component involving minimizing the falsified clauses. The interaction between these components greatly contributes to the difficulty of solving MAXSAT. The main contribution of the thesis is a new hybrid approach, MaxHS, for solving MAXSAT. Our hybrid approach attempts to decouple these two components so that each can be solved with a different technology. In particular, we develop a hybrid solver that exploits two sophisticated technologies with divergent strengths: SAT for solving the logical component, and Integer Programming (IP) solvers for solving the optimization component. MaxHS automatically and incrementally splits the MAXSAT problem into two parts that are given to the SAT and IP solvers, which work together in a complementary way to find a MAXSAT solution. The thesis investigates several improvements to the MaxHS approach and provides empirical analysis of its behaviour in practise. The result is a new solver, MaxHS, that is shown to be the most robust existing solver for MAXSAT.