引入DQCNF的自足赋值
计算机科学中的逻辑
2019-07-30 v1
摘要
SAT的自足赋值（autarkies）可用于理论研究、预处理与处理中化简。它们通过允许留下某些子句“未触及”（不赋值变量）而推广了满足赋值。我们引入对DQCNF（依赖量化布尔CNF）的自然推广，并着眼于特殊情形的SAT翻译。为DQCNF寻找自足赋值与寻找满足赋值同样困难。幸运的是存在（许多）自然的自足赋值系统，它们将自足赋值的范围限制到更可行的域，同时仍保持任意自足赋值良好的通用性质。我们讨论了看似最基本的自足赋值系统，以及相关的化简如何由SAT求解器求得。
引用
@article{arxiv.1907.12156,
title = {Introducing Autarkies for DQCNF},
author = {Oliver Kullmann and Ankit Shukla},
journal= {arXiv preprint arXiv:1907.12156},
year = {2019}
}
备注
5 pages