skip to content

Department of Computer Science and Technology

Image shows, from top to bottom, Viktor Toth, Sean Holden and Tom Lee

A Senior Lecturer and two of his students have just won a Distinguished Paper award at a top artificial intelligence conference for their work in developing a state-of-the-art solver for Quantified Satisfiability problems.

Sean Holden together with former MPhil student Thomas L Lee and current Part III student Viktor Toth received the award earlier this month at the Association for the Advancement of Artificial Intelligence 2021 conference.

It’s a great accolade for them: their paper 'IQ – Incremental Learning for Solving QSAT’ was one of just 12 to receive an award out of more than 9,000 that were submitted to the conference this year.

Viktor (seen top right in main picture) says: "I have found it fascinating how Machine Learning can guide the problem in searching for a formal proof."

Tom (seen bottom right in main picture) says: "Working on this project was very rewarding and it was great that it got an award at AAAI." 

The paper discusses their work in using incremental learning to develop a new solver for quantified satisfiability (QSAT) problems.

As well as being of foundational/theoretical interest, these problems have numerous practical applications in computing, ranging from model-checking to reasoning to planning.

"Think of QSAT as a language that you can convert many different problems into in order to help solve them," says Sean Holden (seen centre right in main picture).

A tool for solving computationally very hard problems
"If you have an AI problem that involves representing knowledge and reasoning with it, you can convert it into the format of a QSAT problem and solve it as that.

"QSAT is also used for solving computer planning problems, or for producing proof that computer hardware is functioning properly. It's a unified method that is used because it can be easier to convert a problem into the format of a QSAT problem and solve it like that than to write a dedicated solver for the problem in its original form."

However, all of these tasks require good QSAT solvers. And writing them, and making significant progress in developing them, is far from easy.  

"QSAT applies to problems that are known to be computationally very hard," Sean says, "and potentially time consuming for computers to solve. So the challenge is to write good QSAT solvers."

He and his students say they have made a great step forward in this regard. They have developed a new QSAT solver, called IQ, by taking an existing solver (QFUN) that uses machine learning for part of its operation, and refining the machine learning element in two important ways.

"First, it replaces batch learning with a carefully selected incremental learning method," the paper’s abstract explains. "Second, it carefully monitors the performance of its learners to decide when to use the learned rules."

"We show, through extensive experiments on a large collection of problems," the authors say, "that our new QSAT solver IQ achieves state-of-the-art performance."

The trio have made their code available on Github and will be interested to see which interested parties take it up.

Competition time
And they are also getting competitive. There is an international QSAT solver competition every year and they are quietly confident that they are in with a good chance of winning.

"We missed the deadline for the last competition," Sean says. "But IQ has soundly outperformed the solver that won for the last two years, so we’ll certainly be entering the next one."

Published by Rachel Gardner on Monday 15th February 2021