Oliver Kullmann, Ankit Shukla,
"Introducing Autarkies for DQCNF"
: International Workshop on Quantified Boolean Formulas and Beyond, 7-2019
Introducing Autarkies for DQCNF
Sprache des Titels:
International Workshop on Quantified Boolean Formulas and Beyond
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.