Exact cover via satisfiability: An empirical study

Abstract

Many tasks in combinatorial computation admit a natural formulation as instances of the exact cover problem. We observe that the exact cover problem can in turn be compactly translated to the satisfiability (SAT) problem, allowing the basic Davis-Putnam-Logemann-Loveland procedure with no clause learning to linearly simulate backtrack search for exact cover. This SAT-based approach is empirically compared with a widely applied backtrack search algorithm, Knuth's "Dancing Links X" algorithm, on a set of benchmark problems arising in combinatorial enumeration. The experimental results indicate that the current model-counting SAT solvers are in general superior in pruning the search space, but still need to be optimized for running time. © 2010 Springer-Verlag.