[Back]

M. Lackner, A. Pfandler:
"Algorithms for finding minimal models";
Talk: Workshop - Parameterized Complexity: Not About Graphs, Darwin, Australien; 2011-08-05 - 2011-08-08.

The classical satisfiability problem asks whether there exists a model for a propositional formula. Such a model is called a minimal model if it is subset minimal with respect to the variables set to true. Computing minimal models is an important task in AI and Reasoning that appears in formalisms such as circumscription [McCarthy 1980], diagnosis [Reiter 1987], ASP [Marek and Truszczynski 1999] and belief revision (see e.g. [Eiter and Gottlob 1992]). This importance originates from human reasoning in which one ignores facts that are not relevant to the current situation. Despite the fundamental importance of minimal models, very little work has been done so far on identifying parameters that yield fixed parameter tractability. This is of particular importance since this problem is Sigma_2-complete and therefore highly intractable. Furthermore, studying the parameterized complexity of a Sigma_2-complete problem is of additional interest, since most of the work in parameterized complexity focuses on NP-complete problems. The aim of our work is to provide a solid basis for applying FPT techniques to minimal model-related problems in AI and Reasoning. We explore several parameterizations of this problem, some of which yield fixed parameter tractability. The concept of backdoor sets [Nishimura, Ragde and Szeider 2004] is especially useful, which we modify to be applicable to minimal model problems. We conclude with a discussion of open problems and further research directions.