关于DPLL的复杂性结果及其解决
Complexity Results on DPLL and Resolution
摘要：
DPLL和归结是解决命题可满足性问题的两种常用方法。它们不是算法，而是算法家族，因为它们的行为取决于它们在执行过程中面临的一些选择：DPLL取决于要分支的字面量的选择;解析取决于每一步要解析的子句对的选择。本文分析了最优选择的复杂性。扩展以前的结果，我们证明了在DPLL中选择最佳的文字分支是Delta[log]^2-hard的，如果分支只允许在变量的子集上，则成为NP^PP-hard。规则分解中的最优选择问题是NP难问题和CoNP难问题。我们还分析了确定最优证明的大小的问题：对于DPLL，它是CoNP困难的，如果我们的猜想是正确的，它是Delta[log]^2困难的。这个问题对于常规的解决方案来说是CoNP困难的。
英文摘要：
DPLL and resolution are two popular methods for solving the problem of propositional satisfiability. Rather than algorithms, they are families of algorithms, as their behavior depend on some choices they face during execution: DPLL depends on the choice of the literal to branch on; resolution depends on the choice of the pair of clauses to resolve at each step. The complexity of making the optimal choice is analyzed in this paper. Extending previous results, we prove that choosing the optimal literal to branch on in DPLL is Delta[log]^2-hard, and becomes NP^PP-hard if branching is only allowed on a subset of variables. Optimal choice in regular resolution is both NP-hard and CoNP-hard. The problem of determining the size of the optimal proofs is also analyzed: it is CoNP-hard for DPLL, and Delta[log]^2-hard if a conjecture we make is true. This problem is CoNP-hard for regular resolution.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
