What is it about?

We present SAT-based encodings of several well-known combinatorial and decision problems and we use them as benchmarks to compare the efficiency of a few popular SAT-solvers. In addition to several known reductions to SAT for the problems of graph k-colouring, vertex k-cover, Hamiltonian path, and verification of UML systems, we also define new original reductions for the N-queens problem, the knight’s tour problem, towers of Hanoi, extended string correction and bounded Post correspondence problem.

Featured Image

Read the Original

This page is a summary of: Applying Modern SAT-solvers to Solving Hard Problems, Fundamenta Informaticae, March 2019, IOS Press,
DOI: 10.3233/fi-2019-1788.
You can read the full text:

Read

Contributors

The following have contributed to this page