Supervisor

Suitable for

Abstract

Constraint programming is a programming paradigm, in which programmers write programs by specifying the problem description (in terms of

constraints) and letting computers use their computational power to figure out the solution automatically. This is in contrast to typical programming paradigms, wherein programmers explicitly spell out procedures for carrying out the computation. Constraint programming has a wide range of applications (e.g. optimisation, planning, ) and rely on powerful constraint solvers to solve computational problems. SAT-solvers --- claimed by some researchers to be among the greatest achievements in the past decade --- are one of the most powerful solvers in the constraint programming toolbox. In a nutshell, SAT-solvers are algorithms for solving satisfiability of boolean formulas, which is an NP-complete problem that can be used as a universal language for encoding many practical combinatorial problems. Although the problem of satisfiability of boolean formulas is difficult in theory, SAT-solvers have greatly advanced in the past two decades to the extent that large formulas (with millions of variables/ clauses) can now be handled.

The aim of the project is to investigate ways in which to improve the performance of SAT-solvers by embedding symmetry information (e.g. variable symmetry). Boolean formulas that arise in practice (e.g. as encodings of combinatorial problems) exhibit many symmetries, which the programmers typically know. Specific questions to explore include: (1) what is a convenient (but general) way to specify symmetry information in boolean formulas? (2) given the symmetry information, how do we engineer SAT-solvers to exploit such information to speed up the search for solutions?