@phdthesis {
   2004-Thesis-PhD-Li,
   author = "X. Y. Li",
   title = "Optimization Algorithms for the Minimum-Cost Satisfiability Problem",
   school = "Computer Science,
             North Carolina State University",
   address = "Raleigh, N.C.",
   month = "August",
   year = "2004",
abstract = "
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~\mincostsat\ 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, \maxsat, and \gpmaxsat.

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 \maxsat, \pmaxsat, and \gpmaxsat\ 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 groups: covering problems and non-covering
problems. The covering problems include the unate or set covering and the binate covering
problems. They have applications in Operations Research (e.g., routing and scheduling)
and logic synthesis (e.g., logic minimization and finite state machine minimization). In
the covering problems, all or most clauses contain no complemented variables and a
feasible solution is relatively easy to find. The non-covering problems contain clauses
that are highly constrained, and sometimes only a small fraction of the variables are
weighted. The non-covering problems have applications in minimum-size test pattern and
minimum-length plans.

We study two important performance factors, among others, in
branch-and-bound \mincostsat\ solvers. They are the lower-bounding and upper-bounding
strategies. For lower bounding, we incorporate two advanced techniques: linear
programming relaxation and cutting planes. Both methods can provide much higher quality
lower-bounds than previous methods based on maximum independent sets of rows. For upper
bounding, we show that our local-search \mincostsat\ solver, when initialized and
terminated properly, can find the best upper-bound quickly.

Other techniques that contribute to the engineering of state-of-the-art solvers for
applications of \mincostsat\ are also introduced.  This work has led to the development
of (1)~a solver for covering problems that consistently outperforms previous leading
solvers by as much as two orders of magnitude, (2)~a logic minimizer that is able to
solve three benchmark problems whose solution has eluded solvers for more than a decade,
(3)~a \maxsat\ solver that challenges the dominance of linear programming solvers,
particularly \cplex, on \maxtwosat\ benchmarks, and (4)~a stochastic local-search solver
for \gpmaxsat\ (with applications to FPGA routing) that finds known optima quickly and is
able to find better than previously-known solutions on benchmarks whose optima remain
unknown.
",
}