7 October 2020 – The NUS team comprising Sung Kah Kay Assistant Professor Kuldeep S. Meel, Visiting Senior Research Fellow Mate Soos, and research intern Arijit Shaw took home the top prizes at the SAT Competition 2020.
An annual competition for solvers of the Boolean Satisfiability (SAT) problem, this year’s event was held alongside the 23rd International Conference on Theory and Applications of Satisfiability Testing, which was held online from 3 to 10 July.
The team took part in three tracks of the competition: the main track, planning track, and incremental library track.
The main track involves sequential SAT solvers, with participants having to solve as many problems (from a set of 300–600) within 5,000 seconds, while the incremental library track involves incremental SAT solvers. The newly added planning track involved SAT solvers that are good for encoding AI planning problems.
The team emerged champions in the incremental library track, and took home second and third place respectively in the planning and main tracks.
“Our work stood out because of its sophisticated hybrid approach, using ideas and tools from both the local search and the conflict-driven clause learning (CDCL) search world. Furthermore, we have used a new hybrid technique for variable branching heuristics, significantly improving the speed of our solver,” said Dr Soos.
Although the competition was delayed because of COVID-19, this gave the team more time to integrate all the key ideas that they were initially afraid would not make it into the final submission.
“In this sense, we made the best of a dark situation and the opportunities it gave us,” said Dr Soos.
Another opportunity involved gaining access to the resources at the National Supercomputing Centre (NSCC) Singapore, which Dr Soos says helped them iron out significant performance bottlenecks during the competition.
“We are also thankful to DSO National Laboratories for their generous funding and Dr Adam Chai from DSO for several wonderful discussions,” added Dr Meel.
The results were seen as a cumulation of the hard work and effort put in by Dr Meel and his research group.
“In 2018, we set out to build the first research group in Singapore focused on improving core SAT/SMT solving techniques. The results of this competition serve as validation for all the effort that was put in over the past two and half years,” said Dr Meel.
“Soos’ multi-month long annual stints in Singapore has also been incredibly useful, as it has allowed group members to learn from one of the foremost experts in SAT solving at very early stages of their career,” he added.
