Solving combinatorial search problems using a SAT-checker.

Brief Description:

Boolean satisfiability is the paradigmatic NP-complete problem. Still, modern SAT-solvers are capable of solving large instances of satisfiability fairly quickly. The NP-completeness of SAT means that in principle, any problem in NP, including many classical combinatorial search problems can be reasonably efficiently transformed into SAT. The aim of this project is to investigate to what extent such reductions can be used to obtain reasonable algorithms for combinatorial search which use a SAT-solver as a back-end. The front-end will be a specification language for describing combinatorial problems, based on second-order logic.

The project will involve investigating and comparing existing SAT solvers, building a front-end to read in search problem specifications and convert them to Boolean formulae, and running large experiments to benchmark the results.