Default Logic and Bounded Treewidth

In this paper, we study Reiter's propositional default logic when the treewidth of a certain graph representation (semi-primal graph) of the input theory is bounded. We establish a dynamic programming algorithm on tree decompositions that decides whether a theory has a consistent stable extension (Ext). Our algorithm can even be used to enumerate all generating defaults (ExtEnum) that lead to stable extensions. We show that our algorithm decides Ext in linear time in the input theory and triple exponential time in the treewidth (so-called fixed-parameter linear algorithm). Further, our algorithm solves ExtEnum with a pre-computation step that is linear in the input theory and triple exponential in the treewidth followed by a linear delay to output solutions.

Strong Backdoors for Default Logic

In this paper, we introduce a notion of backdoors to Reiter's propositional default logic and study structural properties of it. Also we consider the problems of backdoor detection (parameterised by the solution size) as well as backdoor evaluation (parameterised by the size of the given backdoor), for various kinds of target classes (cnf, horn, krom, monotone, identity). We show that backdoor detection is fixed-parameter tractable for the considered target classes, and backdoor evaluation is either fixed-parameter tractable, in para-DP2 , or in para-NP, depending on the target class.