Handbook of Satisfiability Chapter 13: Fixed-Parameter Tractability
Marko Samer and Stefan Szeider
Chapter 13, pp. 425-454.
Handbook edited by Armin Biere, Marien Heule, Hans van
Maaren, and Toby Walsh. IOS Press, 2009. 980 pages. ISBN:
978-1-58603-929-5
Handbook's homepage with ordering information
from publisher
Abstract
Parameterized complexity is a new theoretical framework that
considers, in addition to the overall input size, the effects on
computational complexity of a secondary measurement, the
parameter. This two-dimensional viewpoint allows a fine-grained
complexity analysis that takes structural properties of problem
instances into account. The central notion is "fixed-parameter
tractability" which refers to solvability in polynomial time for each
fixed value of the parameter such that the order of the polynomial
time bound is independent of the parameter. This chapter presents main
concepts and recent results on the parameterized complexity of the
satisfiability problem and it outlines fundamental algorithmic ideas
that arise in this context. Among the parameters considered are the size
of backdoor sets with respect to various tractable base classes and the
treewidth of graph representations of satisfiability instances.
Back Cover Text
Satisfiability (SAT) related topics have attracted researchers from various disciplines: logic, applied areas such as planning, scheduling, operations research and combinatorial optimization, but also theoretical issues on the theme of complexity and much more, they all are connected through SAT.
My personal interest in SAT stems from actual solving: The increase in power of modern SAT solvers over the past 15 years has been phenomenal. It has become the key enabling technology in automated verification of both computer hardware and software. Bounded Model Checking (BMC) of computer hardware is now probably the most widely used model checking technique. The counterexamples that it finds are just satisfying instances of a Boolean formula obtained by unwinding to some fixed depth a sequential circuit and its specification in linear temporal logic. Extending model checking to software verification is a much more difficult problem on the frontier of current research. One promising approach for languages like C with finite word-length integers is to use the same idea as in BMC but with a decision procedure for the theory of bit-vectors instead of SAT. All decision procedures for bit-vectors that I am familiar with ultimately make use of a fast SAT solver to handle complex formulas.
Decision procedures for more complicated theories, like linear real and integer arithmetic, are also used in program verification. Most of them use powerful SAT solvers in an essential way.
Clearly, efficient SAT solving is a key technology for 21st century computer science. I expect this collection of papers on all theoretical and practical aspects of SAT solving will be extremely useful to both students and researchers and will lead to many further advances in the field.
--Edmund Clarke
Edmund Clarke, FORE Systems University Professor of Computer Science
and Professor of Electrical and Computer Engineering at Carnegie
Mellon University, is one of the initiators and main contributors to
the field of Model Checking for which he received the 2007 ACM Turing
Award.
[back to Stefan
Szeider's homepage]
|