Abstract
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.
| Original language | English |
|---|---|
| Title of host publication | International Workshop on Quantified Boolean Formulas and Beyond |
| Number of pages | 5 |
| Publication status | Published - Jul 2019 |
Fields of science
- 102 Computer Sciences
- 102001 Artificial intelligence
- 102011 Formal languages
- 102022 Software development
- 102031 Theoretical computer science
- 603109 Logic
- 202006 Computer hardware