Browse Prior Art Database

Quasi-linear reduction of Hamiltonian Cycle Problem (HCP) to Satisfiability Problem (SAT)

IP.com Disclosure Number: IPCOM000237123D
Publication Date: 2014-Jun-04

Publishing Venue

The IP.com Prior Art Database

Abstract

This paper shows a way of converting any Hamiltonian Cycle problem (HCP) with n vertices and m directed edges to a Boolean Satisfiability problem (SAT) problem with approximately n.log2(m) variables and 2m.(log2(n)+1) clauses. It uses vertex numbering using a linear feedback shift register (LFSR) sequence together with variables identifying active edges, and simple algebraic constraints between a vertex number and its successors' vertex number based on active edges. By adding redundant constraints on the edges a SAT solver can now solve HCP problems with 500 to 1000 vertices.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 10% of the total text.

Page 01 of 16

Quasi-linear reduction of Hamiltonian Cycle Problem (HCP) to Satisfiability Problem (SAT)

Introduction

    An algorithm is disclosed which performs a quasi-linear reduction of any Hamiltonian Cycle problem (HCP) to a Boolean Satisfiability problem (SAT). If the HCP has n vertices and m directed edges then the SAT problem has approximately
n.log2(m) variables and 2m.(log2(n) + 1) clauses. The process is simple and is based on using a set of boolean variables to number each of the vertices in the path. The numbers are represented using a linear feedback shift register sequence

which allows an small number of clauses to represent the constraints between the

vertex numbers of two adjacent vertices.

    Two classic problems in computer science are the Hamiltonian Cycle problem
[1] and the Boolean Satisfiability problem [2].

    The Hamiltonian cycle problem is finding a route around a graph that visits all the vertices by following edges from one vertex to the next before returning to the start.

    The satisfiability problem is finding a set of Boolean variables which make an expression in Conjunctive Normal Form (CNF) true.

    For example:
(a | b) & (a | !c) & (b | c) & (b | !a)

This expression has 3 variables, 8 literals and 4 clauses.

    The Hamiltonian Cycle problem has significant business value as the basis of solving the Travelling Salesman Problem, involved in finding optimum routes for parcel delivery; circuit board component placement or hole drilling. Both HCP and SAT are NP-complete, meaning that as far as anyone knows solving them is exponentially hard with size of problem, but checking a solution is much easier as it can be done in polynomial time. All NP-complete problems can be converted between each other in polynomial time. There are conversions between them[3][4], but it is harder to go from HCP to SAT than vice versa and there is no known linear conversion from HCP to SAT[5]. There many solvers for SAT, but only some for HCP[6].

Existing HCP to SAT conversions

    The current best known way is the HCP -> SAT Cubic time algorithm [7]. This is cubic in terms of vertices to clauses and quadratic in variables, so an HCP with 1000 vertices would have 1,000,000,000 clauses and 1,000,000 variables in SAT. Cubic conversions are impracticable for large (>10000) n. A smaller conversion might allow HCP to be solved by converting to SAT then using an SAT solver. In the future better SAT solvers might be invented, especially as many NP-complete problems can be linearly converted to/from SAT, so a solver for those problems also solves SAT. They might be ordinary algorithms, or there is the possibility of a quantum computer. A quantum computer is more likely for SAT (just a combination

of qubits) than HCP. Also, other problems such as Vertex Cover can be reduced to Hamiltonian cycle in a linear reduction, so could then be reduced to SAT via this method.

    The existing method uses a timing chart of an n by n grid of vertices and time steps, with variables rep...