Paolo Liberatore

Title: Paolo Liberatore

Main Research Question: How efficient are the popular methods DPLL and resolution for solving the problem of propositional satisfiability, and how hard is it to make the optimal choices during execution?

Methodology: The study uses mathematical analysis and computational complexity theory to investigate the efficiency of DPLL and resolution algorithms. It compares the complexity of making optimal choices in these algorithms, such as choosing the best literal to branch on in DPLL or selecting the right pair of clauses to resolve in resolution.

Results: The study proves that choosing the optimal literal to branch on in DPLL is ∆p[logn]-hard and becomes NPPP-hard if branching is only allowed on a subset of variables. Optimal choice in resolution is both NP-hard and coNP-hard. The problem of determining the size of the optimal proofs is also analyzed, and previous hardness results are enhanced.

Implications: These results suggest that making optimal choices in DPLL and resolution can be computationally challenging, potentially leading to increased computational complexity and time. This could have implications for the practical implementation and efficiency of these algorithms. The study also contributes to the ongoing discussion about the automatizability of these methods, providing insights into their potential limitations.

Link to Article: https://arxiv.org/abs/0209032v1 Authors: arXiv ID: 0209032v1