“Problem Solving for the 21st Century: Efficient Solvers for Satisfiability Modulo Theories” by Clark Barrett, Daniel Kroening, and Thomas Melham. London Mathematical Society and Smith Institute for Industrial Mathematics and System Engineering technical report 3, June 2014. Knowledge Transfer Report.
What is the best way to allocate assets across an investment portfolio to minimise risk? How should an airline, operating on razor-thin profit margins, assign flight crew to flights to minimise costs-at the same time meeting regulations and ensuring the schedule is robust? What is the most effective way to test a software system in a limited time? Are there any unforseen security holes in a new business-critical computer system? All these practical problems involve finding solutions to complex systems of constraining requirements that can be formulated mathematically. The task resembles problem-solving in school maths: formulate some equations that relate quantities in the problem to be solved, and then find the right values for the variables that make the equations true. In business and industry, however, the problems are vastly larger and the mathematics much more complex and varied. These important problems cannot be solved by hand, but must be tackled by computer software algorithms. A prominent example is linear programming, a mathematical optimisation technique with wide applications in modern company management and microeconomics. First used in earnest for planning in World War II, linear programming has been a mainstay of business and industry since the 1950s. Over the past decade, a new and revolutionary problem-solving technology has emerged: Satisfiability Modulo Theories, or 'SMT' for short. Like linear programming, it is a computerised method for finding solutions to business and industrial problems expressed mathematically by systems of constraints. But SMT can handle a richer language of constraints than linear programming, and the method encompasses a more varied range of mathematical concepts-so it has the flexibility to tackle many different kinds of problems. With established success in the engineering design of computer chips, software that implements SMT does have limits to the size of problem it can handle-but it has also seen truly astonishing increases in speed and capacity over the past decade. The core SMT algorithms are generic and not special to a particular problem. So, end-users who can frame their practical business and industrial problems in a mathematical way suitable for SMT automatically benefit from intense investment by the highly skilled technical specialists who develop SMT algorithms, a smart way to tap into a sophisticated technology that is improving by leaps and bounds every year. To exploit SMT effectively, you have to express the problem to be solved in the right mathematical way. Some types of problems have well-understood translations into SMT, so the technology is ready for early adoption by at least some enterprises seeking competitive advantage. SMT solutions to other kinds of problems are the subject of active academic and industrial research-and many more lie awaiting creative discovery. This report explains the background to SMT technology and presents several success stories. Our aim is to give a sense of the potential of SMT as an effective solution to some of today's problems-and a unique emerging technology to watch in the future.
BibTeX entry:
@techreport{BKM14,
author = {Clark Barrett and Daniel Kroening and Thomas Melham},
title = {Problem Solving for the 21st Century: Efficient Solvers for
Satisfiability Modulo Theories},
institution = {London Mathematical Society and Smith Institute for
Industrial Mathematics and System Engineering},
number = {3},
month = jun,
year = {2014},
note = {Knowledge Transfer Report},
url = {http://theory.stanford.edu/~barrett/pubs/BKM14.pdf}
}
(This webpage was created with bibtex2web.)