Investigations on autark assignments

AbstractThe structure of the monoid of autarkies and the monoid of autark subsets for clause-sets F is investigated, where autarkies are partial (truth) assignments satisfying some subset F′⊆F (called an autark subset), while not interacting with the clauses in F⧹F′. Generalising minimally unsatisfiable clause-sets, the notion of lean clause-sets is introduced, which do not have non-trivial autarkies, and it is shown that a clause-set is lean iff every clause can be used by some resolution refutation. The largest lean sub-clause-set and the largest autark subset yield a (2-)partition for every clause-set. As a special case of autarkies we introduce the notion of linear autarkies, which can be found in polynomial time by means of linear programming. Clause-sets without non-trivial linear autarkies we call linearly lean, and clause-sets satisfiable by a linear autarky we call linearly satisfiable. As before, the largest linearly lean sub-clause-set and the largest linearly autark subset yield a (2-)partition for every clause-set, but this time the decomposition is computable in polynomial time. The class of linearly satisfiable clause-sets generalises the notion of matched clause-sets introduced in a recent paper by J. Franco and A. Van Gelder, and, as shown by H. van Maaren, contains also (“modulo Unit-clause elimination”) all satisfiable q-Horn clause-sets, introduced by E. Boros, Y. Crama and P. Hammer. The class of linearly lean clause-sets is stable under “crossing out variables” and union, and has some interesting combinatorial properties with respect to the deficiency δ=c−n, the difference of the number of clauses and the number of variables: So for example (non-empty) linearly lean clause-sets fulfill δ⩾1, where this property has been known before only for minimally unsatisfiable clause-sets