Practical Applications of Algorithms Associated with NP-problems

Lecturer: Professor Wiktor Marek (University of Kentucky, USA).

About the Lecturer | Course Summary | Slides: 1 2 3 | Assignment

About the lecturer: Dr. hab. Wiktor Marek is a Professor of Computer Science at the University of Kentucky, Lexington, KY, USA. He received his education at Warsaw University and worked for a number of years at the Mathematical Institute of Warsaw University. He is an author of over 180 papers in journals and proceedings of international meetings, and promoted 15 Ph.D. students. His Curriculum Vitae is available here.

Course summary: This series of lectures will be devoted to the applications of widely-understood Logic in Computer Science. The course covers the introduction to the Satisfiability, at present widely researched problem with a variety of applications in Constraint Solving, Combinatorial Optimization, Security, Model Checking, and other areas of Computer Science. The bibliography, given below, provides "pointers" to additional reading for individuals that want to try to conduct the original research in the area.

These lectures are intended primarily for the Ph.D. program students. We assume some knowledge of Logic, but a graduate student should also be able to follow the lectures. The purpose of these lectures is to offer the participant a perspective on representing Boolean functions, one of the most important objects of widely-understood Computer Science. We will mostly stress Logic perspective, although we will touch upon other points of view including the algebraic one.

The most important theme of our lectures will be Propositional Satisfiability (usually denoted SAT) Ñ a logic-based formalism for declarative programing constraint solving. In this paradigm, atoms of the language represent facts about the domain of the problem. Formulas represent constraints. The idea is that a collection of formulas T represents the problem in such a way that there is a one-to-one correspondence between the satisfying assignments for the atoms and the solutions to the problem. Once a satisfying assignment is found, a solution to the original problem is read-off such assignment.

In this perspective, SAT-solvers (given enough of resources) look for solutions of instances of NP-search problems (also known as the class FNP). Since this class of problems is ubiquitous in practice, and the semantics of formulas and theories is easily explainable to reasonable population of students, SAT-solvers is quite popular as a tool for solving NP-complete problems such as graph coloring, Hamiltonian cycle, etc.

Out of necessity our examples will be simple, but should present the student with some idea on modeling problems that are solved by SAT. In particular so-called DIMACS programming format for SAT solving will be presented. We will focus on the basic algorithm for solving SAT. This is so-called DPLL algorithm based on the techniques developed by M. Davis and H. Putnam and then transformed into a backtracking search-cum-Boolean Constraint Propagation. We will discuss the fundamental improvements of this algorithm that now form a backbone of existing SAT solvers. In particular we will discuss the recent research on clause learning and back-jumping.

We will present the algebraic interpretation of Boolean functions via the ring of polynomials over the field Z2 and comment on the use of algebraic techniques for an alternative approach to SAT. We will also discuss so-called "easy cases" of satisfiability, i.e. classes of theories for which polynomial-time solving algorithms are known. We will discuss "mix-and-match" theorems that show that "divide-and-conquer" strategies for SAT solving do not work.

We will discuss applicability of SAT in areas such as Computer Engineering focusing on the Equivalence Checking, widely applicable technology for testing functional equivalence of digital combinational circuits. We will discuss the issue of proof-checking and model-checking with SAT. We will also discuss applications of SAT-solving to extremal combinatorics.

We will also shortly discuss a competing logic-based formalism for description and solving the class FNP called Answer Set Programming which is quite popular but is related to a different logic. Finally, we will also discuss applications of Logic to so-called Rough Sets, a knowledge representation for incomplete information, as often encountered in practical statistics. In this part of our presentation we will focus on a recent result of Liu and Wu and relating Rough Sets to matroids, a subject of well- known combinatorial theory related to Graph Theory and Linear Algebra. This result, relating Rough Sets to greedy algorithms, has a potential of increasing applicability of rough sets in combinatorial optimization problems.

References:

  1. K.R. Apt, Principles of Constraint Programming, 2nd ed. Cambridge University Press, 2009.
  2. C. Baral, Knowledge Representation, Reasoning and Declarative Problem Solving, 2nd ed. Cambridge University Press, 2010.
  3. M. Heule et. al. Handbook of Satisfiability, IOS Press, 2009.
  4. V.W. Marek, Introduction to Mathematics of Satisfiability, CRC Press, 2009.
  5. Z. Pawlak, Rough Sets, Springer 1991.

Assignment:

You can find the problem set here. There is additional ZIP file attached to the problem set here. Please send your solutions (or questions, should you have any) to Bartosz Klin by Sunday, February 2.