Solving hard problems with local search for Boolean satisfiability

Computers have become essential tools for solving scientific problems. Whilst humans are good at many aspects of problem solving, computers outclass them in many ways, for example in precise logical reasoning using propositional logic, also known as `automated reasoning'. This is essential in industry, and it is arguably one of the most versatile tools in computer science. Many problems, including any problem in NP-complete, can be translated into a logic problem. Questions in a range of fields, from bio-informatics, language modeling, mathematics, to computer vision can be answered by logic. Efficient solvers are available that can answer questions that a decade ago were considered intractable. Even better, formally-verified tools can provide proof of correctness for these answers.

Our research focuses on developing novel automated reasoners to efficiently find suitable solutions to NP-hard problems.