Computer Science – Logic in Computer Science
Scientific paper
2002-09-27
Computer Science
Logic in Computer Science
Scientific paper
10.1145/1119439.1119442
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.
No associations
LandOfFree
Complexity Results on DPLL and Resolution does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Complexity Results on DPLL and Resolution, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Complexity Results on DPLL and Resolution will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-433720