Solving the boolean satisfiability problem using multilevel techniques

Abstract

There are many complex problems in computer science that occur in knowledge-representation (artificial thinking), artificial learning, Very Large Scale Integration (VLSI) design, security protocols and other areas. These complex problems may be deduced into satisfiability problems where the Boolean Satisfiability Problem (SAT) may be applied. This deduction is made in order to simplify complex problems into a specific propositional logic problem. The SAT problem is the most well-known nondeterministic polynomial time (NP) complete problem in computer science. It is a Boolean expression which is composed of a specific amount of variables (literals), clauses that contain disjunctions of the literals and conjunctions of the clauses. The literals have the logical values TRUE and FALSE, the task is to find a truth assignment that makes the entire expression TRUE. The main goal of the thesis is to solve the SAT problem using a clustering technique - Multilevel - combined first with Tabu Search and combined thereafter with finite Learning Automata. Tabu Search and finite Learning Automata are two very efficient approaches that have been used to solve SAT. Benchmark experiments are conducted in order to disclose whether combining Multilevel with existing solutions to solve SAT will provide better results - than the two mentioned approaches alone - mainly in terms of computational efficiency