困难的 SAT 相关推理任务在 Krom 片段中是否变得更易?
计算机科学中的逻辑
2023-06-22 v3
摘要
许多推理问题基于可满足性(SAT)问题。虽然 SAT 本身在以一种特定方式限制公式结构时变得容易,但对于更复杂的决策问题,情况则更不明朗。我们在此考虑 CardMinSat 问题,其询问:给定命题公式 与原子 , 是否在 的某个基数极小模型中为真。该问题在 Horn 片段中是容易的,但正如我们将在本文中展示的,在 Krom 片段(由子句至多含两个文字的 CNF 公式给出)中仍为 -完全(从而是 -难的)。我们将利用这一事实研究信念修正与基于逻辑的溯因中推理任务的复杂性,并表明虽然在某些情况下限制为 Krom 公式会导致复杂性下降,但在其他情况下则不会。因此我们也就 Krom 公式的附加限制考察了 CardMinSat 问题,以更好地理解此类问题的易处理性边界。
引用
@article{arxiv.1711.07786,
title = {Do Hard SAT-Related Reasoning Tasks Become Easier in the Krom Fragment?},
author = {Nadia Creignou and Reinhard Pichler and Stefan Woltran},
journal= {arXiv preprint arXiv:1711.07786},
year = {2023}
}