General Variable Neighbourhood Search Approach to MAX-3SAT Problem

Abstract

MAX-3SAT problem is a version of MAX-SAT problem where every clause has exactly three literals. It is one of the most important problems of compu- tational complexity theory, and as such, many solvers have been developed for it. Since it belongs to the class of NP-complete problems, it is usually solved by implementing heuristic methods. In this paper we used general variable neighbourhood search (GVNS) to obtain the best possible solution in a given amount of time. GVNS is neighbor- hood based search algorithm that involves two main steps: perturbation and improvement. We defined two sets of neighbourhoods, each of them used in the perturbation step with a predefined probability p. For the improvement step we used variable neighbourhood descent (VND), which is a local search heuristic that explores several neighborhood structures in a deterministic way. The proposed GVNS approach is tested on a set of benchmark instances found at: https://www.cs.ubc.ca/ hoos/SATLIB/benchm.html, and compared with state-of-the-art WalkSAT implementation: http://www.cs.rochester.edu/u/kautz/walksat/. We concluded that for smaller instances our approach gives similar results as aforementioned WalkSAT imple- mentation, but it performed better for larger instances, given that it finds very good solutions very quickly.