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 is a 4-tuple
(A, E, F, D), where
- A is the set of
- E is the set of
existential variables, with A ∩ E = ∅,
- F is a
clause-setover A ∪ E (i.e., var(F) ⊆ A ∪ E),
- D is the
dependency-mapwith 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.