Skip to main content

Benchmarking SAT-solvers via necklace splitting


Suitable for

MSc in Computer Science
Mathematics and Computer Science, Part C
Computer Science and Philosophy, Part C
Computer Science, Part C


We consider the problem of generating challenge-instances (or benchmarks) for SAT solvers.We propose to investigate the usage of the "NECKLACE-SPLITTING" problem to create such challenges instances, since this problem is hard but has guaranteed solutions. The project involves generating instances of NECKLACE-SPLITTING, converting them to SAT instances, and passing them to various SAT-solvers to test the SAT-solvers' performance. It will also be of interest to know whether certain constrained kinds of solutions are harder to find via this approach. There is scope to experiment with alternative ways of generating the random instances of NECKLACE-SPLITTING.