David Mitchell and Evgenia Ternovska
David Mitchell and Evgenia Ternovska
Aromas of coffee and chocolate grace the office in an old house near Vancouver’s Commercial Drive where Evgenia Ternovska and David Mitchell are working. Both are professors of computing science at SFU. They have often talked of restoring the place to its original glory, with historic details, but that dream has to wait. They have more pressing problems of an intellectual nature.
The couple specialize in the theory of computation, in methods for solving what computer scientists call “search” problems. An example is finding a schedule for all 30 NHL hockey teams with no conflicts while maximizing the number of games broadcast in prime time EST television markets. Such problems are challenging, and most people don’t have access to the software expertise to tackle them.
“We should be able to solve problems by describing them using a language that shows through logic what needs to be found, rather than by coming up with a step by step solution method,” says Ternovska. That is, by writing a specification instead of developing an algorithm. “Rather than hiring programmers, you describe the problem in a specification or modeling language,” says Mitchell. The specification, together with a problem instance (i.e., this year’s list of teams and possible dates), is then given to a software system, called a solver, that tries to construct a solution. Technology for solving computationally hard problems with many variables and constraints has been in development since World War II, when nations needed to optimize productivity for the war effort. Mitchell had been studying the logic underlying some recent advances in solver technology, and was thinking he needed a higher order representation for problems. He needed a form of logic that could represent problems in a certain way. Meanwhile, Ternovska was working on a higher level logic for formal knowledge representation, and wanted a way to apply it. She had also been reading scholarly papers on descriptive complexity theory, a branch of mathematical logic that characterizes the computational complexity of problems through logics, or formal languages.
Though the two had worked alongside each other for five years in the same department, they had never collaborated. Now they realized that logic and descriptive complexity theory could provide a basis for a formal theory underlying both modelling languages and solving technology. They knew that between them they had the right background for developing this idea into a practical system, and they could make it work.
So on that sunny afternoon in their home office they began working together on a framework for modelling and solving search problems. They called it MX for Model Expansion. Mitchell contributed his expertise on representing and solving problems while Ternovska provided her knowledge of logic and computation, with an emphasis on efficient reasoning.
By 2006 they had published a paper on the topic, which came to the attention of Bill Macready, VP of product development at D-Wave, a Vancouver company intent on building the world’s first commercial quantum computer. Unlike conventional computers which are based on bits that are either on or off, quantum computers rely on quantum bits, or qubits, which can be on or off or in a combination of both on and off at once. A quantum computer should be able to solve problems of great complexity in seconds instead of days. Applications include scheduling or finding bugs in complex microprocessors with over a billion transistors or in complicated computer programs with millions of lines of code.
“We can’t expect people to know how to program our quantum hardware because we cannot provide a procedural interface,” says Macready. “Instead we ask them to state precisely what their problem is and we have software that will automatically translate that into machine language for the quantum computer.” Ternovska and Mitchell’s MX system was designed for just this purpose. It was perfect for Macready because MX not only forces the problem to be clearly defined, it also describes the data and what a correct answer would look like. “It gives the relationship between the data and the solution as well as what it means to be a solution,” says Macready. To explain their MX framework, Mitchell and Ternovska use a database analogy. Computer professionals design a database with what is called a schema (Greek for plan). It is an abstract description of the structure of the data and how things are related. For instance, a university database describing student information and courses taught, might have a table for students listing their addresses and phone numbers, and another listing courses and grades. Modern database systems use a standard language, called SQL for Structured Query Language, to query a database for information. A typical query might be: “SELECT * FROM Students WHERE gpa>3.5 ORDER BY name”, which would give an alphabetical list of all students with high grade point averages. “Formally, we think of an SQL query as a logical formula, and a database schema as the application-specific symbols used in the formula,” says Ternovska. To illustrate the MX task, think of the entire database as an instance of a problem, e.g. a scheduling problem. The task is to come up with some new tables which describe the solution. The MX user writes a specification, which is much like an SQL query, that describes the relationship between the given database and a new one expanded with added solution tables. For example, “Rooms and times in the schedule for all lectures must be arranged so that all students registered can attend their classes with no conflicts.” The task for the MX solver is to construct a new table representing the schedule, listing all lectures and their assigned rooms. The resulting database now combines the given and new tables and satisfies the specification.
This is quite different from standard use of SQL, where queries are made with respect to the existing database only. Computationally, the MX task is very difficult, and is among the problems theoreticians call NP-complete. The MX user does everything with logical description. There is no procedure. MX already works well for existing solvers on conventional computers, although some queries may take a very long time to solve. Theoretically, quantum computers should find the answers suddenly, all at once, by simultaneously examining a vast array of probability distributions among qubit states rather than by turning switches on and off in long tedious procedural sequences, the way today’s digital computers work. D-Wave hopes their quantum computing machinery will substantially speed up problem solving in this way.
In March 2008, after a year and a half of negotiations, Ternovska and Mitchell signed a contract with D-Wave to provide MX software for their quantum computer, and to further develop the technology. D-Wave’s engineers like MX because with a bit of extra work they can translate it to SQL, which is already familiar to most programmers. “Dave and Evgenia’s software is like the glue in the middle between machine code and a high level user interface,” says Macready.
MX has been keeping the computing duo busy. “The project has a very large scope and we don’t have much manpower,” says Ternovska. Mitchell adds, “There’s a substantial body of work needed to get from the idea stage to an MX system for solving real problems”. Nevertheless, for the two theoreticians a practical implementation of their work is a goal worth working towards and they are very excited about their new deal with D-Wave. Who knows, maybe it will ultimately provide a solution to the problem of finding enough time to renovate their old house. Contact: ter@cs.sfu.ca.
Comment Guidelines