On the use of autarkies for satisfiability decision

Autarkies are generalizations of satisfying assignments for conjunctive normal forms and detect “redundant” clauses, clauses which can not be used for refutations. Starting from an abstract theory of autarkies (in the framework of monoids operating on ordered sets) and autarky systems (restrictions of the notion of general autarkies), we discuss several autarky systems for generalized clause-sets, and the relation to polynomial time computability.