# 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:

- An
**Ak- autarky**for F is an autarky such that all boolean functions assigned depend essentially on at most k variables. - 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**.