Benchmarking SAT-solvers via necklace splitting
Supervisor
Suitable for
Abstract
We consider the problem of generating challenge-instances (or benchmarks) for SAT solvers.We propose to investigate the usage
of the "NECKLACE-SPLITTING" problem https://en.wikipedia.org/wiki/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.
