CS SEMINAR

Minimal Unsatisfiable Subsets

Speaker
Jaroslav Bendik
Chaired by
Dr Kuldeep S. MEEL, Associate Professor, School of Computing
meel@comp.nus.edu.sg

17 Oct 2019 Thursday, 03:00 PM to 04:00 PM

MR1, COM1-03-19

Abstract:
In many different applications we are given a set of constraints with the goal to decide whether the set is satisfiable. If the set is determined to be unsatisfiable, one might be interested in analyzing this unsatisfiability. Identification of minimal unsatisfiable subsets (MUSes) is a kind of such analysis. The more MUSes are identified, the better insight into the unsatisfiability is obtained. However, the full enumeration of all MUSes is often intractable. Therefore, algorithms that identify MUSes in an online fashion, i.e., one by one, are needed. Moreover, since MUSes find applications in various constraint domains and new applications still arise, there is a desire for domain agnostic MUS enumeration approaches.
In this talk, we describe 1) what are the Minimal Unsatisfiable Subsets, 2) we show various applications in various constraint domains, 3) and we discuss domain agnostic algorithms for MUS enumeration.

Biodata:
Jaroslav Bendik is a Ph.D. candidate at the Faculty of Informatics, Masaryk University, Czech Republic. His bachelor's and master's theses were defended also at Masaryk university and dealt with various graph problems related to the model checking problem. During his Ph.D. studies, he focuses on algorithms for finding so-called Minimal Unsatisfiable Subsets (MUSes). MUSes can be used to analyze the infeasibility of various constraint systems and find applications in many areas of computer science. For example, Jaroslav's work has been applied in the areas of requirements analysis, model checking, theorem proving, and constraint processing.