Optimization algorithms for the minimum-cost satisfiability problem
Xiao Yu Li, Matthias F. M. Stallmann, F. Brglez · 2004
Given a Boolean satisfiability (Sat) problem whose variables have non-negative weights, the minimum-cost satisfiability (MinCostSat) problem finds a satisfying truth assignment that minimizes a weighted sum of the truth values of the variables. Many NP-optimization problems are either special cases of MinCostSat or can be transformed into MinCostSat efficiently. However, in the past, these problems have been largely considered in isolation. In this dissertation, we (1) classify existing Min-CostSat problems, (2) study factors affecting the performance of MinCostSat solvers, (3) propose algorithms for MinCostSat problems, and (4) implement and validate the performance of state-of-the-art solvers for special cases of MinCostSat, including set and binate covering, Max-Sat, and group-partial Max-Sat. We categorize MinCostSat problems as either native or non-native. Non-native problems can only be transformed into MinCostSat by adding slack variables. These problems include the Max-Sat, partial Max-Sat, and group-partial Max-Sat problems which have applications ranging from course assignment to FPGA detailed routing. Native problems are various sub-cases of MinCostSat. We further divide these into two