Multilevel techniques and learning automata for the Maximum Satisfiability (MAXSAT) problem

Abstract

The Maximum Satisfiability (MAXSAT) Problem is a propositional logic and an optimization based problem that has great importance in the theoretical and practical domain. In the recent years MAXSAT has risen great interest in the industry. Example problems from the industry that can be encoded as MAXSAT problems are circuit design and debugging, hardware verification, bioinformatics and scheduling. These kind of problems often tend to be large and increase exponentially with the problem size, and therefore algorithms for solving such problems incorporate different techniques and methods to solve the problems in a smart and efficient manner. In this thesis we introduce a range of algorithms that extend the well-known Stochastic Local Search (SLS) algorithm called WalkSAT. WalkSAT is extended with the multilevel paradigm and Learning Automata. The multilevel paradigm is a technique that splits large and difficult problems into smaller problems. These problems are expectedly less complex and therefore easier to solve. Learning Automata are a branch of machine learning that can be seen as a decision-making entity that is employed in an unknown environment. Through feedback from the environment the Learning Automata try to learn the optimal actions. The core of this thesis is the observations and findings of how these dissimilar techniques affect the performance and behaviour of WalkSAT when solving industrial MAXSAT problem instances. Through extensive experiments our results confirm that combining multilevel techniques and Learning Automata with WalkSAT, separately and together, give promising results. We compare these composite algorithms with WalkSAT on selected industrial MAXSAT problems throughout the thesis, and show that all these composite algorithms perform better than WalkSAT.