PC 与 URC 公式大小的界
计算机科学中的逻辑
2021-01-06 v3 人工智能
摘要
本文研究 CNF 公式，对这类公式而言，若公式连同变量的部分赋值不可满足（单元归结完全或 URC 公式），则单元传播足以推导出矛盾；或者若公式可满足则还能推导出所有被蕴涵的文字（传播完全或 PC 公式）。若公式利用存在量化的辅助变量表示一个函数，则称之为该函数的编码。我们证明了关于 PC 与 URC 公式及编码大小的若干结果。其中之一是不同类型公式大小之间的分离。具体而言，我们证明了 URC 公式与 PC 公式大小的指数级分离，以及使用辅助变量的 PC 编码与 URC 公式大小的分离。此外，我们证明同一函数的任意两个无冗余 PC 公式的大小至多相差一个关于变量数的多项式因子，并给出一个函数示例表明对 URC 公式类似结论不成立。上述分离之一意味着一个 q-Horn 公式可能需要指数级数量的附加子句才能成为 URC 公式。另一方面，对每个 q-Horn 公式，我们给出使用辅助变量的该函数的多项式大小 URC 编码。此编码一般不是 q-Horn 的。
引用
@article{arxiv.2001.00819,
title = {Bounds on the size of PC and URC formulas},
author = {Petr Kučera and Petr Savický},
journal= {arXiv preprint arXiv:2001.00819},
year = {2021}
}
备注
24 pages, minor corrections and improvements of the text