# Introducing Autarkies for DQCNF

## TL;DR

This paper extends the concept of autarkies from SAT to DQCNF, exploring their theoretical properties, computational complexity, and practical systems for finding autarkies using SAT solvers.

## Contribution

It introduces the first generalization of autarkies to DQCNF, analyzes their complexity, and discusses autarky-systems and reduction techniques for practical computation.

## Key findings

- Autarkies for DQCNF are as hard to find as satisfying assignments.
- Natural autarky-systems can restrict autarkies to feasible domains.
- SAT solvers can be used to find reductions related to autarkies.

## Abstract

Autarkies for SAT can be used for theoretical studies, pre-processing 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.