Project
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.