|
Abstract : |
Abstract. This paper discusses polynomial-time reductions from Hamiltonian Circuit (HC), k-Vertex Coloring (k-VC), and k-Clique Problems to Satisfiability Problem (SAT) which are efficient in the number of Boolean variables needed in SAT. We first present a basic type of reductions that need (n 0 1) log(n 0 1), (n 0 1) log k, and k log n variables for HC, k-VC and k-Clique, respectively. Several heuristics can reduce the number of variables. Some of them achieve: (n 0 I 0 1) log(n 0 1) +6 log d i for HC (I is the size of any independent set of vertices v i 's whose degree is d i 's), and log n + (k 0 1) log D for k-Clique (D is the kth largest degree of the graph). Recent revolutionary progress in SAT algorithms will make it increasingly reasonable to solve (hard) combinatorial problems after reducing them to SAT. Efficiency in the above sense apparently plays a key role in this approach. From a different viewpoint, the number of variables can act as a complexity measure for the original problems, if the reduction is sufficiently efficient. The merits of heuristics can also be evaluated by (the reduction of) this complexity., |
