Combinatorial Optimization Via Proposition Reasoning

As a branch of optimization, combinatorial optimization is a central topic in computer science and operations research. Its domain is optimization problems where the set of feasible solutions is discrete or can be reduced to a discrete one, and the goal is to find the best possible solution. Combinatorial optimization has numerous real applications such as job shop scheduling, planning, resource allocation, vehicle routing problem, integer programming, and cutting stock problem. In this modern time where maximizing benefit and minimizing resource consuming become more and more important, combinatorial optimization is often crucial for many economical actors to be competitive for increasing their benefit and reducing the negative impact of their activities to the environment.Combinatorial optimization problems are often NP-hard. In other words, for all but the smallest problems, finding global optimum solutions is computationally complex. In many real cases, intuitive and straightforward solutions are simply used that could be far from the optimum. Therefore, relatively small progress in solving these problems can give a significant profit in practice. Furthermore, many combinatorial optimization problems are related with each other, progress in solving one problem can be directly or indirectly adapted to solve other ones.The propositional SATisfiability (SAT) problem is the first problem proven to be NP-Complete. SAT is the prototype of all NP-complete problems and captures intensive attention of researchers over 60 years. There is an international research community for SAT and an annual international conference ranked"A"on SAT. However, the real application of SAT is rather limited, because propositional reasoning is a very low-level reasoning. Furthermore, SAT instances always lose the structural information of the original problems, making their solving generally harder. On the contrary, Vertex Coloring Problem (VCP) and its variants are often more suitable than SAT for describing the extrinsic relations and structural information of a combinatorial problem. The VCP is a typical NP-hard combinatorial optimization problem, and has received much attention in the literature, not only for its real world applications in many engineering fields, including, among many others, scheduling, timetabling, register allocation and communication networks, but also for its theoretical aspects and for its difficulty from the computational point of view.This paper proposes an exact algorithm based on propositional reasoning for VCP, which is believed to be new. We start by introducing some crucial techniques used in the best modern SAT solvers, and then go on to show how a series of improvements enhance the performance of an existing VCP solver. In the end, we demonstrate that combining with propositional reasoning is a promising way to raise the performance to the point where it is able to compete with some of the state-of-the-art approaches on a series of benchmark problems.