Introducing Autarkies for DQCNF
Autarkies
for SAT can be used for theoretical studies, preprocessing
and inprocessing
.
They generalise satisfying assignments by allowing to leave some clauses untouched (no variable assigned).
We introduce the natural generalisation to DQCNF (dependency-quantified
boolean CNF), with the perspective of SAT translations for special cases.
Finding an autarky for DQCNF is as hard as finding a satisfying assignment.
Fortunately there are (many) natural autarky-systems
, which
allow restricting the range of autarkies to a more feasible domain, while
still maintaining the good general properties of arbitrary autarkies. We
discuss what seems the most fundamental autarky systems, and how the
related reductions can be found by SAT solvers.