Since their introduction by Atserias, Kolaitis, and Vardi in 2004, proof systems where each line is represented by an ordered binary decision diagram (OBDD) have been intensively studied as they allow to compactly represent Boolean functions. We extend this line of work by considering representation formats that can be even more succinct than OBDDs and have gained a lot of attention in the area of knowledge compilation: sentential decision diagrams (SDDs) and deterministic structured DNNF circuits (d-SDNNFs). We show that both variants can provide strictly smaller refutations of unsatisfiable CNFs than their OBDD counterparts. Furthermore, we investigate the relative strength of these systems depending on which of the three fundamental derivation rules join, reordering, and weakening are allowed. Here we obtain several separations and identify interesting open problems. To streamline our proofs we establish a sat-to-unsat lifting theorem that might be of independent interest: it turns satisfiable CNFs that are hard to represent by SDDs and d-SDNNFs into unsatisfiable CNFs that are hard to refute in the corresponding proof system.

翻译：自Atserias、Kolaitis和Vardi于2004年提出以来，以有序二叉决策图(OBDD)表示每一行的证明系统因其能紧凑表示布尔函数而受到深入研究。我们将此工作线扩展至考虑比OBDD更简洁且已在知识编译领域备受关注的表示格式：句子决策图(SDD)和确定性结构化DNNF电路(d-SDNNF)。我们证明这两个变体对不可满足CNF公式提供的反驳均严格小于OBDD对应系统。此外，我们研究了这些系统在允许联结、重排和弱化这三种基本推演规则时的相对强度，获得了若干分离结果并识别出有趣的开放问题。为精简证明，我们建立了一个可能具有独立意义的可满足到不可满足的提升定理：该定理将难以被SDD和d-SDNNF表示的可满足CNF公式转化为在对应证明系统中难以反驳的不可满足CNF公式。