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

摘要

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