Looking for an Autarky?

---------------------
 Autarkies for SAT are partial assignments for boolean CNF, 
 which either satisfy a clause or leave it untouched.
--------------
        \   ^__^
         \  (oo)\_______
            (__)\       )\/\
                ||----w |
                ||     ||

DQCNF

A DQCNF is a 4-tuple (A, E, F, D), where

• A is the set of universal variables,
• E is the set of existential variables, with A ∩ E = ∅,
• F is a clause-set over A ∪ E (i.e., var(F) ⊆ A ∪ E),
• D is the dependency-map with dom(D) = E, mapping v ∈ E → D(v) ⊆ A, the variables on which v depends.

A- and E-systems

Consider a DQCNF F and k ≥ 0:

1. An Ak- autarky for F is an autarky such that all boolean functions assigned depend essentially on at most k variables.
2. An Ek- autarky is an autarky assigns at most k (existential) variables.

  A0 and A1 allow the boolean functions to essentially 
  depend on 0 resp. 1 universal variable.

  E1 only uses one existential variable.

We have considered three Autarky Systems A1, E1, A1 + E1.