Default logic, propositional logic and constraints

We present a mapping from a class of default theories to sentences in propositional logic, such that each model of the latter corresponds to an extension of the former. Using this mapping we show that many properties of default theories can be determined by solving propositional satisfiability. In particular, we show how CSP techniques can be used to identify, analyze and solve tractable subsets of Reiter's default logic.