一句话：证明CardMinSat在Krom片段仍为Θ₂-完全，并刻画其对信念修正与溯因推理复杂度的影响。
本文研究SAT相关推理问题在限制公式结构后是否变易，重点考察CardMinSat：给定命题公式φ与原子x，判断x是否在某些基数最小模型中为真。已知该问题在Horn片段易解，作者证明其在Krom片段（CNF子句至多两个文字）仍为Θ₂-完全，因而NP难。基于此，文章分析信念修正与基于逻辑的溯因等推理任务：限制到Krom公式有时降低复杂度，有时不降低。作者还考察Krom公式的额外限制，以更精确刻画这些问题的可处理性边界。
Many reasoning problems are based on the problem of satisfiability (SAT). While SAT itself becomes easy when restricting the structure of the formulas in a certain way, the situation is more opaque for more involved decision problems. We consider here the CardMinSat problem which asks, given a propositional formula $\phi$ and an atom $x$, whether $x$ is true in some cardinality-minimal model of $\phi$. This problem is easy for the Horn fragment, but, as we will show in this paper, remains $\Theta_2$-complete (and thus $\mathrm{NP}$-hard) for the Krom fragment (which is given by formulas in CNF where clauses have at most two literals). We will make use of this fact to study the complexity of reasoning tasks in belief revision and logic-based abduction and show that, while in some cases the restriction to Krom formulas leads to a decrease of complexity, in others it does not. We thus also consider the CardMinSat problem with respect to additional restrictions to Krom formulas towards a better understanding of the tractability frontier of such problems.
@article{paperbot360,
title = {Do Hard SAT-Related Reasoning Tasks Become Easier in the Krom Fragment?},
author = {Nadia Creignou and Reinhard Pichler and Stefan Woltran},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 4},
year = {2018},
doi = {10.23638/lmcs-14(4:10)2018}
}