Proof of Concept: Fast Solutions to NP-problems by Using SAT and Integer Programming Solvers

TL;DR

This paper demonstrates that converting NP problems like finding the largest clique into SAT or Integer Programming instances and solving them with modern solvers can lead to faster solutions, showcasing a practical approach leveraging recent solver advancements.

Contribution

It introduces a proof of concept showing that NP problems can be efficiently solved by translating them into SAT or ILP and utilizing advanced solvers, outperforming traditional methods.

Findings

Integer programming translation was the fastest approach.

SAT translation outperformed optimized backtracking.

Modern solvers significantly improve NP problem solving efficiency.

Abstract

In the last decade, the power of the state-of-the-art SAT and Integer Programming solvers has dramatically increased. They implement many new techniques and heuristics and since any NP problem can be converted to SAT or ILP instance, we could take advantage of these techniques in general by converting the instance of NP problem to SAT formula or Integer program. A problem we consider, in this proof of concept, is finding a largest clique in a graph. We ran several experiments on large random graphs and compared 3 approaches: Optimised backtrack solution, Translation to SAT and Translation to Integer program. The last one was the fastest one.